Step | Hyp | Ref
| Expression |
1 | | hsmexlem4.o |
. . . . . . 7
⊢ 𝑂 = OrdIso( E , (rank “
((𝑈‘𝑑)‘𝑐))) |
2 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑐 = ∅ → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘∅)) |
3 | 2 | imaeq2d 5385 |
. . . . . . . 8
⊢ (𝑐 = ∅ → (rank “
((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘∅))) |
4 | | oieq2 8301 |
. . . . . . . 8
⊢ ((rank
“ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘∅)) → OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅)))) |
5 | 3, 4 | syl 17 |
. . . . . . 7
⊢ (𝑐 = ∅ → OrdIso( E ,
(rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅)))) |
6 | 1, 5 | syl5eq 2656 |
. . . . . 6
⊢ (𝑐 = ∅ → 𝑂 = OrdIso( E , (rank “
((𝑈‘𝑑)‘∅)))) |
7 | 6 | dmeqd 5248 |
. . . . 5
⊢ (𝑐 = ∅ → dom 𝑂 = dom OrdIso( E , (rank “
((𝑈‘𝑑)‘∅)))) |
8 | | fveq2 6103 |
. . . . 5
⊢ (𝑐 = ∅ → (𝐻‘𝑐) = (𝐻‘∅)) |
9 | 7, 8 | eleq12d 2682 |
. . . 4
⊢ (𝑐 = ∅ → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “
((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅))) |
10 | 9 | ralbidv 2969 |
. . 3
⊢ (𝑐 = ∅ → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅))) |
11 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑐 = 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘𝑒)) |
12 | 11 | imaeq2d 5385 |
. . . . . . . 8
⊢ (𝑐 = 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘𝑒))) |
13 | | oieq2 8301 |
. . . . . . . 8
⊢ ((rank
“ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒)))) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝑐 = 𝑒 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒)))) |
15 | 1, 14 | syl5eq 2656 |
. . . . . 6
⊢ (𝑐 = 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒)))) |
16 | 15 | dmeqd 5248 |
. . . . 5
⊢ (𝑐 = 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒)))) |
17 | | fveq2 6103 |
. . . . 5
⊢ (𝑐 = 𝑒 → (𝐻‘𝑐) = (𝐻‘𝑒)) |
18 | 16, 17 | eleq12d 2682 |
. . . 4
⊢ (𝑐 = 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “
((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒))) |
19 | 18 | ralbidv 2969 |
. . 3
⊢ (𝑐 = 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒))) |
20 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑐 = suc 𝑒 → ((𝑈‘𝑑)‘𝑐) = ((𝑈‘𝑑)‘suc 𝑒)) |
21 | 20 | imaeq2d 5385 |
. . . . . . . 8
⊢ (𝑐 = suc 𝑒 → (rank “ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘suc 𝑒))) |
22 | | oieq2 8301 |
. . . . . . . 8
⊢ ((rank
“ ((𝑈‘𝑑)‘𝑐)) = (rank “ ((𝑈‘𝑑)‘suc 𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒)))) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ (𝑐 = suc 𝑒 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒)))) |
24 | 1, 23 | syl5eq 2656 |
. . . . . 6
⊢ (𝑐 = suc 𝑒 → 𝑂 = OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒)))) |
25 | 24 | dmeqd 5248 |
. . . . 5
⊢ (𝑐 = suc 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒)))) |
26 | | fveq2 6103 |
. . . . 5
⊢ (𝑐 = suc 𝑒 → (𝐻‘𝑐) = (𝐻‘suc 𝑒)) |
27 | 25, 26 | eleq12d 2682 |
. . . 4
⊢ (𝑐 = suc 𝑒 → (dom 𝑂 ∈ (𝐻‘𝑐) ↔ dom OrdIso( E , (rank “
((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))) |
28 | 27 | ralbidv 2969 |
. . 3
⊢ (𝑐 = suc 𝑒 → (∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐) ↔ ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))) |
29 | | imassrn 5396 |
. . . . . . 7
⊢ (rank
“ ((𝑈‘𝑑)‘∅)) ⊆ ran
rank |
30 | | rankf 8540 |
. . . . . . . 8
⊢
rank:∪ (𝑅1 “
On)⟶On |
31 | | frn 5966 |
. . . . . . . 8
⊢
(rank:∪ (𝑅1 “
On)⟶On → ran rank ⊆ On) |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
⊢ ran rank
⊆ On |
33 | 29, 32 | sstri 3577 |
. . . . . 6
⊢ (rank
“ ((𝑈‘𝑑)‘∅)) ⊆
On |
34 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
35 | | hsmexlem4.u |
. . . . . . . . . 10
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
36 | 35 | ituni0 9123 |
. . . . . . . . 9
⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘∅) = 𝑑) |
37 | 34, 36 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑈‘𝑑)‘∅) = 𝑑 |
38 | 37 | imaeq2i 5383 |
. . . . . . 7
⊢ (rank
“ ((𝑈‘𝑑)‘∅)) = (rank
“ 𝑑) |
39 | | ffun 5961 |
. . . . . . . . . 10
⊢
(rank:∪ (𝑅1 “
On)⟶On → Fun rank) |
40 | 30, 39 | ax-mp 5 |
. . . . . . . . 9
⊢ Fun
rank |
41 | | wdomimag 8375 |
. . . . . . . . 9
⊢ ((Fun
rank ∧ 𝑑 ∈ V)
→ (rank “ 𝑑)
≼* 𝑑) |
42 | 40, 34, 41 | mp2an 704 |
. . . . . . . 8
⊢ (rank
“ 𝑑)
≼* 𝑑 |
43 | | sneq 4135 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑}) |
44 | 43 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑑 → (TC‘{𝑎}) = (TC‘{𝑑})) |
45 | 44 | raleqdv 3121 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑑 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋)) |
46 | | hsmexlem4.s |
. . . . . . . . . . 11
⊢ 𝑆 = {𝑎 ∈ ∪
(𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋} |
47 | 45, 46 | elrab2 3333 |
. . . . . . . . . 10
⊢ (𝑑 ∈ 𝑆 ↔ (𝑑 ∈ ∪
(𝑅1 “ On) ∧ ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋)) |
48 | 47 | simprbi 479 |
. . . . . . . . 9
⊢ (𝑑 ∈ 𝑆 → ∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋) |
49 | | snex 4835 |
. . . . . . . . . . . 12
⊢ {𝑑} ∈ V |
50 | | tcid 8498 |
. . . . . . . . . . . 12
⊢ ({𝑑} ∈ V → {𝑑} ⊆ (TC‘{𝑑})) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢ {𝑑} ⊆ (TC‘{𝑑}) |
52 | | vsnid 4156 |
. . . . . . . . . . 11
⊢ 𝑑 ∈ {𝑑} |
53 | 51, 52 | sselii 3565 |
. . . . . . . . . 10
⊢ 𝑑 ∈ (TC‘{𝑑}) |
54 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (𝑏 ≼ 𝑋 ↔ 𝑑 ≼ 𝑋)) |
55 | 54 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝑑 ∈ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋)) |
56 | 53, 55 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑏 ∈
(TC‘{𝑑})𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋) |
57 | | domwdom 8362 |
. . . . . . . . 9
⊢ (𝑑 ≼ 𝑋 → 𝑑 ≼* 𝑋) |
58 | 48, 56, 57 | 3syl 18 |
. . . . . . . 8
⊢ (𝑑 ∈ 𝑆 → 𝑑 ≼* 𝑋) |
59 | | wdomtr 8363 |
. . . . . . . 8
⊢ (((rank
“ 𝑑)
≼* 𝑑 ∧
𝑑 ≼* 𝑋) → (rank “ 𝑑) ≼* 𝑋) |
60 | 42, 58, 59 | sylancr 694 |
. . . . . . 7
⊢ (𝑑 ∈ 𝑆 → (rank “ 𝑑) ≼* 𝑋) |
61 | 38, 60 | syl5eqbr 4618 |
. . . . . 6
⊢ (𝑑 ∈ 𝑆 → (rank “ ((𝑈‘𝑑)‘∅)) ≼* 𝑋) |
62 | | eqid 2610 |
. . . . . . 7
⊢ OrdIso( E
, (rank “ ((𝑈‘𝑑)‘∅))) = OrdIso( E , (rank
“ ((𝑈‘𝑑)‘∅))) |
63 | 62 | hsmexlem1 9131 |
. . . . . 6
⊢ (((rank
“ ((𝑈‘𝑑)‘∅)) ⊆ On
∧ (rank “ ((𝑈‘𝑑)‘∅)) ≼* 𝑋) → dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘∅))) ∈
(har‘𝒫 𝑋)) |
64 | 33, 61, 63 | sylancr 694 |
. . . . 5
⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “
((𝑈‘𝑑)‘∅))) ∈
(har‘𝒫 𝑋)) |
65 | | hsmexlem4.h |
. . . . . 6
⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) |
66 | 65 | hsmexlem7 9128 |
. . . . 5
⊢ (𝐻‘∅) =
(har‘𝒫 𝑋) |
67 | 64, 66 | syl6eleqr 2699 |
. . . 4
⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “
((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅)) |
68 | 67 | rgen 2906 |
. . 3
⊢
∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘∅))) ∈ (𝐻‘∅) |
69 | | nfra1 2925 |
. . . . . 6
⊢
Ⅎ𝑑∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) |
70 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑑 𝑒 ∈ ω |
71 | 69, 70 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑑(∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω) |
72 | 35 | ituniiun 9127 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ V → ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)) |
73 | 34, 72 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑈‘𝑑)‘suc 𝑒) = ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒) |
74 | 73 | imaeq2i 5383 |
. . . . . . . . . . 11
⊢ (rank
“ ((𝑈‘𝑑)‘suc 𝑒)) = (rank “ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)) |
75 | | imaiun 6407 |
. . . . . . . . . . 11
⊢ (rank
“ ∪ 𝑓 ∈ 𝑑 ((𝑈‘𝑓)‘𝑒)) = ∪
𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)) |
76 | 74, 75 | eqtri 2632 |
. . . . . . . . . 10
⊢ (rank
“ ((𝑈‘𝑑)‘suc 𝑒)) = ∪
𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)) |
77 | | oieq2 8301 |
. . . . . . . . . 10
⊢ ((rank
“ ((𝑈‘𝑑)‘suc 𝑒)) = ∪
𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒)))) |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . 9
⊢ OrdIso( E
, (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) |
79 | 78 | dmeqi 5247 |
. . . . . . . 8
⊢ dom
OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) = dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) |
80 | 58 | ad2antll 761 |
. . . . . . . . 9
⊢
((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → 𝑑 ≼* 𝑋) |
81 | 65 | hsmexlem9 9130 |
. . . . . . . . . 10
⊢ (𝑒 ∈ ω → (𝐻‘𝑒) ∈ On) |
82 | 81 | ad2antrl 760 |
. . . . . . . . 9
⊢
((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘𝑒) ∈ On) |
83 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑎 ∈ ∪ (𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋} ⊆ ∪
(𝑅1 “ On) |
84 | 46, 83 | eqsstri 3598 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑆 ⊆ ∪ (𝑅1 “ On) |
85 | 84 | sseli 3564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ 𝑆 → 𝑑 ∈ ∪
(𝑅1 “ On)) |
86 | | r1elssi 8551 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ ∪ (𝑅1 “ On) → 𝑑 ⊆ ∪ (𝑅1 “ On)) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ 𝑆 → 𝑑 ⊆ ∪
(𝑅1 “ On)) |
88 | 87 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ ∪
(𝑅1 “ On)) |
89 | | snssi 4280 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ 𝑑 → {𝑓} ⊆ 𝑑) |
90 | 34 | tcss 8503 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑓} ⊆ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑)) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑)) |
92 | 49 | tcel 8504 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 ∈ {𝑑} → (TC‘𝑑) ⊆ (TC‘{𝑑})) |
93 | 52, 92 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ 𝑑 → (TC‘𝑑) ⊆ (TC‘{𝑑})) |
94 | 91, 93 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘{𝑑})) |
95 | | ssralv 3629 |
. . . . . . . . . . . . . . . . 17
⊢
((TC‘{𝑓})
⊆ (TC‘{𝑑})
→ (∀𝑏 ∈
(TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋)) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ 𝑑 → (∀𝑏 ∈ (TC‘{𝑑})𝑏 ≼ 𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋)) |
97 | 48, 96 | mpan9 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋) |
98 | | sneq 4135 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑓 → {𝑎} = {𝑓}) |
99 | 98 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑓 → (TC‘{𝑎}) = (TC‘{𝑓})) |
100 | 99 | raleqdv 3121 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑓 → (∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋)) |
101 | 100, 46 | elrab2 3333 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ ∪
(𝑅1 “ On) ∧ ∀𝑏 ∈ (TC‘{𝑓})𝑏 ≼ 𝑋)) |
102 | 88, 97, 101 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆) |
103 | 102 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆) |
104 | 103 | adantll 746 |
. . . . . . . . . . . 12
⊢
(((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → 𝑓 ∈ 𝑆) |
105 | | simpll 786 |
. . . . . . . . . . . 12
⊢
(((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒)) |
106 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑓 → (𝑈‘𝑑) = (𝑈‘𝑓)) |
107 | 106 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑓 → ((𝑈‘𝑑)‘𝑒) = ((𝑈‘𝑓)‘𝑒)) |
108 | 107 | imaeq2d 5385 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑓 → (rank “ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒))) |
109 | | oieq2 8301 |
. . . . . . . . . . . . . . . 16
⊢ ((rank
“ ((𝑈‘𝑑)‘𝑒)) = (rank “ ((𝑈‘𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒)))) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑓 → OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒)))) |
111 | 110 | dmeqd 5248 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑓 → dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) = dom OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒)))) |
112 | 111 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑓 → (dom OrdIso( E , (rank “
((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ↔ dom OrdIso( E , (rank “
((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))) |
113 | 112 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝑆 → (∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) → dom OrdIso( E , (rank “
((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))) |
114 | 104, 105,
113 | sylc 63 |
. . . . . . . . . . 11
⊢
(((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → dom OrdIso( E , (rank “
((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒)) |
115 | | imassrn 5396 |
. . . . . . . . . . . . 13
⊢ (rank
“ ((𝑈‘𝑓)‘𝑒)) ⊆ ran rank |
116 | 115, 32 | sstri 3577 |
. . . . . . . . . . . 12
⊢ (rank
“ ((𝑈‘𝑓)‘𝑒)) ⊆ On |
117 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈‘𝑓)‘𝑒) ∈ V |
118 | 117 | funimaex 5890 |
. . . . . . . . . . . . . 14
⊢ (Fun rank
→ (rank “ ((𝑈‘𝑓)‘𝑒)) ∈ V) |
119 | 40, 118 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (rank
“ ((𝑈‘𝑓)‘𝑒)) ∈ V |
120 | 119 | elpw 4114 |
. . . . . . . . . . . 12
⊢ ((rank
“ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ↔ (rank “
((𝑈‘𝑓)‘𝑒)) ⊆ On) |
121 | 116, 120 | mpbir 220 |
. . . . . . . . . . 11
⊢ (rank
“ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On |
122 | 114, 121 | jctil 558 |
. . . . . . . . . 10
⊢
(((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) → ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E ,
(rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))) |
123 | 122 | ralrimiva 2949 |
. . . . . . . . 9
⊢
((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E ,
(rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))) |
124 | | eqid 2610 |
. . . . . . . . . 10
⊢ OrdIso( E
, (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , (rank “ ((𝑈‘𝑓)‘𝑒))) |
125 | | eqid 2610 |
. . . . . . . . . 10
⊢ OrdIso( E
, ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) = OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) |
126 | 124, 125 | hsmexlem3 9133 |
. . . . . . . . 9
⊢ (((𝑑 ≼* 𝑋 ∧ (𝐻‘𝑒) ∈ On) ∧ ∀𝑓 ∈ 𝑑 ((rank “ ((𝑈‘𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E ,
(rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (𝐻‘𝑒))) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒)))) |
127 | 80, 82, 123, 126 | syl21anc 1317 |
. . . . . . . 8
⊢
((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , ∪ 𝑓 ∈ 𝑑 (rank “ ((𝑈‘𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒)))) |
128 | 79, 127 | syl5eqel 2692 |
. . . . . . 7
⊢
((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , (rank “
((𝑈‘𝑑)‘suc 𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻‘𝑒)))) |
129 | 65 | hsmexlem8 9129 |
. . . . . . . 8
⊢ (𝑒 ∈ ω → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒)))) |
130 | 129 | ad2antrl 760 |
. . . . . . 7
⊢
((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻‘𝑒)))) |
131 | 128, 130 | eleqtrrd 2691 |
. . . . . 6
⊢
((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆)) → dom OrdIso( E , (rank “
((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)) |
132 | 131 | expr 641 |
. . . . 5
⊢
((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω) → (𝑑 ∈ 𝑆 → dom OrdIso( E , (rank “
((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))) |
133 | 71, 132 | ralrimi 2940 |
. . . 4
⊢
((∀𝑑 ∈
𝑆 dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) ∧ 𝑒 ∈ ω) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)) |
134 | 133 | expcom 450 |
. . 3
⊢ (𝑒 ∈ ω →
(∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “
((𝑈‘𝑑)‘𝑒))) ∈ (𝐻‘𝑒) → ∀𝑑 ∈ 𝑆 dom OrdIso( E , (rank “ ((𝑈‘𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))) |
135 | 10, 19, 28, 68, 134 | finds1 6987 |
. 2
⊢ (𝑐 ∈ ω →
∀𝑑 ∈ 𝑆 dom 𝑂 ∈ (𝐻‘𝑐)) |
136 | 135 | r19.21bi 2916 |
1
⊢ ((𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆) → dom 𝑂 ∈ (𝐻‘𝑐)) |