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 8784 |
. 2
⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂)) |
9 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem4 8780 |
. . . . 5
⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) |
10 | 9 | frnd 6351 |
. . . 4
⊢ (𝜑 → ran 𝑂 ⊆ 𝐴) |
11 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem2 8778 |
. . . . . . . . . . 11
⊢ (𝜑 → Ord 𝑇) |
12 | | ordirr 6047 |
. . . . . . . . . . 11
⊢ (Ord
𝑇 → ¬ 𝑇 ∈ 𝑇) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑇 ∈ 𝑇) |
14 | 1 | tfr1a 7834 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 ∧ Lim dom 𝐹) |
15 | 14 | simpri 478 |
. . . . . . . . . . . . 13
⊢ Lim dom
𝐹 |
16 | | limord 6088 |
. . . . . . . . . . . . 13
⊢ (Lim dom
𝐹 → Ord dom 𝐹) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Ord dom
𝐹 |
18 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem1 8777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) |
19 | | ordtypelem9.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑂 ∈ V) |
20 | 18, 19 | eqeltrrd 2867 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ 𝑇) ∈ V) |
21 | 1 | tfr2b 7836 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝑇 → (𝑇 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝑇) ∈ V)) |
22 | 11, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 ∈ dom 𝐹 ↔ (𝐹 ↾ 𝑇) ∈ V)) |
23 | 20, 22 | mpbird 249 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ dom 𝐹) |
24 | | ordelon 6053 |
. . . . . . . . . . . 12
⊢ ((Ord dom
𝐹 ∧ 𝑇 ∈ dom 𝐹) → 𝑇 ∈ On) |
25 | 17, 23, 24 | sylancr 578 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ On) |
26 | | imaeq2 5766 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑇 → (𝐹 “ 𝑎) = (𝐹 “ 𝑇)) |
27 | 26 | raleqdv 3355 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑇 → (∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏 ↔ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
28 | 27 | rexbidv 3242 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑇 → (∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
29 | | breq1 4932 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑐 → (𝑧𝑅𝑡 ↔ 𝑐𝑅𝑡)) |
30 | 29 | cbvralv 3383 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑧 ∈
(𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑡) |
31 | | breq2 4933 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑏 → (𝑐𝑅𝑡 ↔ 𝑐𝑅𝑏)) |
32 | 31 | ralbidv 3147 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑏 → (∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑡 ↔ ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏)) |
33 | 30, 32 | syl5bb 275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑏 → (∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏)) |
34 | 33 | cbvrexv 3384 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑡 ∈
𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏) |
35 | | imaeq2 5766 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → (𝐹 “ 𝑥) = (𝐹 “ 𝑎)) |
36 | 35 | raleqdv 3355 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏 ↔ ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏)) |
37 | 36 | rexbidv 3242 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑥)𝑐𝑅𝑏 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏)) |
38 | 34, 37 | syl5bb 275 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏)) |
39 | 38 | cbvrabv 3412 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} = {𝑎 ∈ On ∣ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏} |
40 | 4, 39 | eqtri 2802 |
. . . . . . . . . . . . 13
⊢ 𝑇 = {𝑎 ∈ On ∣ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑎)𝑐𝑅𝑏} |
41 | 28, 40 | elrab2 3599 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ 𝑇 ↔ (𝑇 ∈ On ∧ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
42 | 41 | baib 528 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ On → (𝑇 ∈ 𝑇 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
43 | 25, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑇 ∈ 𝑇 ↔ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
44 | 13, 43 | mtbid 316 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏) |
45 | | ralnex 3183 |
. . . . . . . . 9
⊢
(∀𝑏 ∈
𝐴 ¬ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏 ↔ ¬ ∃𝑏 ∈ 𝐴 ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏) |
46 | 44, 45 | sylibr 226 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 ¬ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏) |
47 | 46 | r19.21bi 3158 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → ¬ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏) |
48 | 18 | rneqd 5651 |
. . . . . . . . . . 11
⊢ (𝜑 → ran 𝑂 = ran (𝐹 ↾ 𝑇)) |
49 | | df-ima 5420 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑇) = ran (𝐹 ↾ 𝑇) |
50 | 48, 49 | syl6eqr 2832 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑂 = (𝐹 “ 𝑇)) |
51 | 50 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → ran 𝑂 = (𝐹 “ 𝑇)) |
52 | 51 | raleqdv 3355 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (∀𝑐 ∈ ran 𝑂 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏)) |
53 | 9 | ffund 6348 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝑂) |
54 | 53 | funfnd 6219 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑂 Fn dom 𝑂) |
55 | 54 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑂 Fn dom 𝑂) |
56 | | breq1 4932 |
. . . . . . . . . 10
⊢ (𝑐 = (𝑂‘𝑚) → (𝑐𝑅𝑏 ↔ (𝑂‘𝑚)𝑅𝑏)) |
57 | 56 | ralrn 6679 |
. . . . . . . . 9
⊢ (𝑂 Fn dom 𝑂 → (∀𝑐 ∈ ran 𝑂 𝑐𝑅𝑏 ↔ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏)) |
58 | 55, 57 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (∀𝑐 ∈ ran 𝑂 𝑐𝑅𝑏 ↔ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏)) |
59 | 52, 58 | bitr3d 273 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (∀𝑐 ∈ (𝐹 “ 𝑇)𝑐𝑅𝑏 ↔ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏)) |
60 | 47, 59 | mtbid 316 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → ¬ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏) |
61 | | rexnal 3185 |
. . . . . 6
⊢
(∃𝑚 ∈ dom
𝑂 ¬ (𝑂‘𝑚)𝑅𝑏 ↔ ¬ ∀𝑚 ∈ dom 𝑂(𝑂‘𝑚)𝑅𝑏) |
62 | 60, 61 | sylibr 226 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → ∃𝑚 ∈ dom 𝑂 ¬ (𝑂‘𝑚)𝑅𝑏) |
63 | 1, 2, 3, 4, 5, 6, 7 | ordtypelem7 8783 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑚 ∈ dom 𝑂) → ((𝑂‘𝑚)𝑅𝑏 ∨ 𝑏 ∈ ran 𝑂)) |
64 | 63 | ord 850 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐴) ∧ 𝑚 ∈ dom 𝑂) → (¬ (𝑂‘𝑚)𝑅𝑏 → 𝑏 ∈ ran 𝑂)) |
65 | 64 | rexlimdva 3229 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (∃𝑚 ∈ dom 𝑂 ¬ (𝑂‘𝑚)𝑅𝑏 → 𝑏 ∈ ran 𝑂)) |
66 | 62, 65 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ran 𝑂) |
67 | 10, 66 | eqelssd 3878 |
. . 3
⊢ (𝜑 → ran 𝑂 = 𝐴) |
68 | | isoeq5 6897 |
. . 3
⊢ (ran
𝑂 = 𝐴 → (𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂) ↔ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))) |
69 | 67, 68 | syl 17 |
. 2
⊢ (𝜑 → (𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂) ↔ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))) |
70 | 8, 69 | mpbid 224 |
1
⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) |