Step | Hyp | Ref
| Expression |
1 | | ordtypelem.1 |
. . 3
⊢ 𝐹 = recs(𝐺) |
2 | | ordtypelem.2 |
. . 3
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} |
3 | | ordtypelem.3 |
. . 3
⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) |
4 | | ordtypelem.5 |
. . 3
⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} |
5 | | ordtypelem.6 |
. . 3
⊢ 𝑂 = OrdIso(𝑅, 𝐴) |
6 | | ordtypelem.7 |
. . 3
⊢ (𝜑 → 𝑅 We 𝐴) |
7 | | ordtypelem.8 |
. . 3
⊢ (𝜑 → 𝑅 Se 𝐴) |
8 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem8 8430 |
. 2
⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂)) |
9 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem4 8426 |
. . . . 5
⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) |
10 | | frn 6053 |
. . . . 5
⊢ (𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴 → ran 𝑂 ⊆ 𝐴) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑂 ⊆ 𝐴) |
12 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem2 8424 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Ord 𝑇) |
13 | | ordirr 5741 |
. . . . . . . . . . . . 13
⊢ (Ord
𝑇 → ¬ 𝑇 ∈ 𝑇) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑇 ∈ 𝑇) |
15 | 1 | tfr1a 7490 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝐹 ∧ Lim dom 𝐹) |
16 | 15 | simpri 478 |
. . . . . . . . . . . . . . 15
⊢ Lim dom
𝐹 |
17 | | limord 5784 |
. . . . . . . . . . . . . . 15
⊢ (Lim dom
𝐹 → Ord dom 𝐹) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ Ord dom
𝐹 |
19 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem1 8423 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) |
20 | | ordtypelem9.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑂 ∈ V) |
21 | 19, 20 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 ↾ 𝑇) ∈ V) |
22 | 1 | tfr2b 7492 |
. . . . . . . . . . . . . . . 16
⊢ (Ord
𝑇 → (𝑇 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝑇) ∈ V)) |
23 | 12, 22 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝑇) ∈ V)) |
24 | 21, 23 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ dom 𝐹) |
25 | | ordelon 5747 |
. . . . . . . . . . . . . 14
⊢ ((Ord dom
𝐹 ∧ 𝑇 ∈ dom 𝐹) → 𝑇 ∈ On) |
26 | 18, 24, 25 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ On) |
27 | | imaeq2 5462 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑇 → (𝐹 “ 𝑎) = (𝐹 “ 𝑇)) |
28 | 27 | raleqdv 3144 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑇 → (∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏 ↔ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
29 | 28 | rexbidv 3052 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑇 → (∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
30 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑐 → (𝑧𝑅𝑡 ↔ 𝑐𝑅𝑡)) |
31 | 30 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑧 ∈
(𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑡) |
32 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = 𝑏 → (𝑐𝑅𝑡 ↔ 𝑐𝑅𝑏)) |
33 | 32 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑏 → (∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑡 ↔ ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏)) |
34 | 31, 33 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑏 → (∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏)) |
35 | 34 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑡 ∈
𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏) |
36 | | imaeq2 5462 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑎 → (𝐹 “ 𝑥) = (𝐹 “ 𝑎)) |
37 | 36 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏 ↔ ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏)) |
38 | 37 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → (∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏)) |
39 | 35, 38 | syl5bb 272 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏)) |
40 | 39 | cbvrabv 3199 |
. . . . . . . . . . . . . . . 16
⊢ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} = {𝑎 ∈ On ∣ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏} |
41 | 4, 40 | eqtri 2644 |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = {𝑎 ∈ On ∣ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏} |
42 | 29, 41 | elrab2 3366 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ 𝑇 ↔ (𝑇 ∈ On ∧ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
43 | 42 | baib 944 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ On → (𝑇 ∈ 𝑇 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
44 | 26, 43 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑇 ∈ 𝑇 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
45 | 14, 44 | mtbid 314 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏) |
46 | | ralnex 2992 |
. . . . . . . . . . 11
⊢
(∀𝑏 ∈
𝐴 ¬ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏 ↔ ¬ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏) |
47 | 45, 46 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 ¬ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏) |
48 | 47 | r19.21bi 2932 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → ¬ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏) |
49 | 19 | rneqd 5353 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑂 = ran (𝐹 ↾ 𝑇)) |
50 | | df-ima 5127 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ 𝑇) = ran (𝐹 ↾ 𝑇) |
51 | 49, 50 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑂 = (𝐹 “ 𝑇)) |
52 | 51 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → ran 𝑂 = (𝐹 “ 𝑇)) |
53 | 52 | raleqdv 3144 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (∀𝑐 ∈ ran 𝑂 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
54 | | ffun 6048 |
. . . . . . . . . . . . . 14
⊢ (𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴 → Fun 𝑂) |
55 | 9, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝑂) |
56 | | funfn 5918 |
. . . . . . . . . . . . 13
⊢ (Fun
𝑂 ↔ 𝑂 Fn dom 𝑂) |
57 | 55, 56 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑂 Fn dom 𝑂) |
58 | 57 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑂 Fn dom 𝑂) |
59 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑐 = (𝑂‘𝑚) → (𝑐𝑅𝑏 ↔ (𝑂‘𝑚)𝑅𝑏)) |
60 | 59 | ralrn 6362 |
. . . . . . . . . . 11
⊢ (𝑂 Fn dom 𝑂 → (∀𝑐 ∈ ran 𝑂 𝑐𝑅𝑏 ↔ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏)) |
61 | 58, 60 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (∀𝑐 ∈ ran 𝑂 𝑐𝑅𝑏 ↔ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏)) |
62 | 53, 61 | bitr3d 270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏 ↔ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏)) |
63 | 48, 62 | mtbid 314 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → ¬ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏) |
64 | | rexnal 2995 |
. . . . . . . 8
⊢
(∃𝑚 ∈ dom
𝑂 ¬ (𝑂‘𝑚)𝑅𝑏 ↔ ¬ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏) |
65 | 63, 64 | sylibr 224 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → ∃𝑚 ∈ dom 𝑂 ¬ (𝑂‘𝑚)𝑅𝑏) |
66 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem7 8429 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑚 ∈ dom 𝑂) → ((𝑂‘𝑚)𝑅𝑏 ∨ 𝑏 ∈ ran 𝑂)) |
67 | 66 | ord 392 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑚 ∈ dom 𝑂) → (¬ (𝑂‘𝑚)𝑅𝑏 → 𝑏 ∈ ran 𝑂)) |
68 | 67 | rexlimdva 3031 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (∃𝑚 ∈ dom 𝑂 ¬ (𝑂‘𝑚)𝑅𝑏 → 𝑏 ∈ ran 𝑂)) |
69 | 65, 68 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ran 𝑂) |
70 | 69 | ex 450 |
. . . . 5
⊢ (𝜑 → (𝑏 ∈ 𝐴 → 𝑏 ∈ ran 𝑂)) |
71 | 70 | ssrdv 3609 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ran 𝑂) |
72 | 11, 71 | eqssd 3620 |
. . 3
⊢ (𝜑 → ran 𝑂 = 𝐴) |
73 | | isoeq5 6571 |
. . 3
⊢ (ran
𝑂 = 𝐴 → (𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂) ↔ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))) |
74 | 72, 73 | syl 17 |
. 2
⊢ (𝜑 → (𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂) ↔ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))) |
75 | 8, 74 | mpbid 222 |
1
⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) |