Proof of Theorem hsmexlem5
| Step | Hyp | Ref
| Expression |
| 1 | | hsmexlem4.s |
. . . . . . . 8
⊢ 𝑆 = {𝑎 ∈ ∪
(𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋} |
| 2 | 1 | ssrab3 4082 |
. . . . . . 7
⊢ 𝑆 ⊆ ∪ (𝑅1 “ On) |
| 3 | 2 | sseli 3979 |
. . . . . 6
⊢ (𝑑 ∈ 𝑆 → 𝑑 ∈ ∪
(𝑅1 “ On)) |
| 4 | | tcrank 9924 |
. . . . . 6
⊢ (𝑑 ∈ ∪ (𝑅1 “ On) →
(rank‘𝑑) = (rank
“ (TC‘𝑑))) |
| 5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) = (rank “ (TC‘𝑑))) |
| 6 | | hsmexlem4.u |
. . . . . . . 8
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
| 7 | 6 | itunitc 10461 |
. . . . . . 7
⊢
(TC‘𝑑) = ∪ ran (𝑈‘𝑑) |
| 8 | 6 | itunifn 10457 |
. . . . . . . 8
⊢ (𝑑 ∈ 𝑆 → (𝑈‘𝑑) Fn ω) |
| 9 | | fniunfv 7267 |
. . . . . . . 8
⊢ ((𝑈‘𝑑) Fn ω → ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐) = ∪ ran (𝑈‘𝑑)) |
| 10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝑑 ∈ 𝑆 → ∪
𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐) = ∪ ran (𝑈‘𝑑)) |
| 11 | 7, 10 | eqtr4id 2796 |
. . . . . 6
⊢ (𝑑 ∈ 𝑆 → (TC‘𝑑) = ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐)) |
| 12 | 11 | imaeq2d 6078 |
. . . . 5
⊢ (𝑑 ∈ 𝑆 → (rank “ (TC‘𝑑)) = (rank “ ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐))) |
| 13 | | imaiun 7265 |
. . . . . 6
⊢ (rank
“ ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐)) = ∪
𝑐 ∈ ω (rank
“ ((𝑈‘𝑑)‘𝑐)) |
| 14 | 13 | a1i 11 |
. . . . 5
⊢ (𝑑 ∈ 𝑆 → (rank “ ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐)) = ∪
𝑐 ∈ ω (rank
“ ((𝑈‘𝑑)‘𝑐))) |
| 15 | 5, 12, 14 | 3eqtrd 2781 |
. . . 4
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) = ∪ 𝑐 ∈ ω (rank “
((𝑈‘𝑑)‘𝑐))) |
| 16 | | dmresi 6070 |
. . . 4
⊢ dom ( I
↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = ∪
𝑐 ∈ ω (rank
“ ((𝑈‘𝑑)‘𝑐)) |
| 17 | 15, 16 | eqtr4di 2795 |
. . 3
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) = dom ( I ↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
| 18 | | rankon 9835 |
. . . . . 6
⊢
(rank‘𝑑)
∈ On |
| 19 | 15, 18 | eqeltrrdi 2850 |
. . . . 5
⊢ (𝑑 ∈ 𝑆 → ∪
𝑐 ∈ ω (rank
“ ((𝑈‘𝑑)‘𝑐)) ∈ On) |
| 20 | | eloni 6394 |
. . . . 5
⊢ (∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)) ∈ On → Ord ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) |
| 21 | | oiid 9581 |
. . . . 5
⊢ (Ord
∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)) → OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = ( I ↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
| 22 | 19, 20, 21 | 3syl 18 |
. . . 4
⊢ (𝑑 ∈ 𝑆 → OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = ( I ↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
| 23 | 22 | dmeqd 5916 |
. . 3
⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = dom ( I ↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
| 24 | 17, 23 | eqtr4d 2780 |
. 2
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) = dom OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
| 25 | | omex 9683 |
. . . 4
⊢ ω
∈ V |
| 26 | | wdomref 9612 |
. . . 4
⊢ (ω
∈ V → ω ≼* ω) |
| 27 | 25, 26 | mp1i 13 |
. . 3
⊢ (𝑑 ∈ 𝑆 → ω ≼*
ω) |
| 28 | | frfnom 8475 |
. . . . . . 7
⊢
(rec((𝑧 ∈ V
↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) Fn
ω |
| 29 | | hsmexlem4.h |
. . . . . . . 8
⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) |
| 30 | 29 | fneq1i 6665 |
. . . . . . 7
⊢ (𝐻 Fn ω ↔ (rec((𝑧 ∈ V ↦
(har‘𝒫 (𝑋
× 𝑧))),
(har‘𝒫 𝑋))
↾ ω) Fn ω) |
| 31 | 28, 30 | mpbir 231 |
. . . . . 6
⊢ 𝐻 Fn ω |
| 32 | | fniunfv 7267 |
. . . . . 6
⊢ (𝐻 Fn ω → ∪ 𝑎 ∈ ω (𝐻‘𝑎) = ∪ ran 𝐻) |
| 33 | 31, 32 | ax-mp 5 |
. . . . 5
⊢ ∪ 𝑎 ∈ ω (𝐻‘𝑎) = ∪ ran 𝐻 |
| 34 | | iunon 8379 |
. . . . . . 7
⊢ ((ω
∈ V ∧ ∀𝑎
∈ ω (𝐻‘𝑎) ∈ On) → ∪ 𝑎 ∈ ω (𝐻‘𝑎) ∈ On) |
| 35 | 25, 34 | mpan 690 |
. . . . . 6
⊢
(∀𝑎 ∈
ω (𝐻‘𝑎) ∈ On → ∪ 𝑎 ∈ ω (𝐻‘𝑎) ∈ On) |
| 36 | 29 | hsmexlem9 10465 |
. . . . . 6
⊢ (𝑎 ∈ ω → (𝐻‘𝑎) ∈ On) |
| 37 | 35, 36 | mprg 3067 |
. . . . 5
⊢ ∪ 𝑎 ∈ ω (𝐻‘𝑎) ∈ On |
| 38 | 33, 37 | eqeltrri 2838 |
. . . 4
⊢ ∪ ran 𝐻 ∈ On |
| 39 | 38 | a1i 11 |
. . 3
⊢ (𝑑 ∈ 𝑆 → ∪ ran
𝐻 ∈
On) |
| 40 | | fvssunirn 6939 |
. . . . . 6
⊢ (𝐻‘𝑐) ⊆ ∪ ran
𝐻 |
| 41 | | hsmexlem4.x |
. . . . . . . 8
⊢ 𝑋 ∈ V |
| 42 | | eqid 2737 |
. . . . . . . 8
⊢ OrdIso( E
, (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) |
| 43 | 41, 29, 6, 1, 42 | hsmexlem4 10469 |
. . . . . . 7
⊢ ((𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆) → dom OrdIso( E , (rank “
((𝑈‘𝑑)‘𝑐))) ∈ (𝐻‘𝑐)) |
| 44 | 43 | ancoms 458 |
. . . . . 6
⊢ ((𝑑 ∈ 𝑆 ∧ 𝑐 ∈ ω) → dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑐))) ∈ (𝐻‘𝑐)) |
| 45 | 40, 44 | sselid 3981 |
. . . . 5
⊢ ((𝑑 ∈ 𝑆 ∧ 𝑐 ∈ ω) → dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑐))) ∈ ∪ ran
𝐻) |
| 46 | | imassrn 6089 |
. . . . . . 7
⊢ (rank
“ ((𝑈‘𝑑)‘𝑐)) ⊆ ran rank |
| 47 | | rankf 9834 |
. . . . . . . 8
⊢
rank:∪ (𝑅1 “
On)⟶On |
| 48 | | frn 6743 |
. . . . . . . 8
⊢
(rank:∪ (𝑅1 “
On)⟶On → ran rank ⊆ On) |
| 49 | 47, 48 | ax-mp 5 |
. . . . . . 7
⊢ ran rank
⊆ On |
| 50 | 46, 49 | sstri 3993 |
. . . . . 6
⊢ (rank
“ ((𝑈‘𝑑)‘𝑐)) ⊆ On |
| 51 | | ffun 6739 |
. . . . . . . 8
⊢
(rank:∪ (𝑅1 “
On)⟶On → Fun rank) |
| 52 | | fvex 6919 |
. . . . . . . . 9
⊢ ((𝑈‘𝑑)‘𝑐) ∈ V |
| 53 | 52 | funimaex 6655 |
. . . . . . . 8
⊢ (Fun rank
→ (rank “ ((𝑈‘𝑑)‘𝑐)) ∈ V) |
| 54 | 47, 51, 53 | mp2b 10 |
. . . . . . 7
⊢ (rank
“ ((𝑈‘𝑑)‘𝑐)) ∈ V |
| 55 | 54 | elpw 4604 |
. . . . . 6
⊢ ((rank
“ ((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On ↔ (rank “
((𝑈‘𝑑)‘𝑐)) ⊆ On) |
| 56 | 50, 55 | mpbir 231 |
. . . . 5
⊢ (rank
“ ((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On |
| 57 | 45, 56 | jctil 519 |
. . . 4
⊢ ((𝑑 ∈ 𝑆 ∧ 𝑐 ∈ ω) → ((rank “
((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On ∧ dom OrdIso( E ,
(rank “ ((𝑈‘𝑑)‘𝑐))) ∈ ∪ ran
𝐻)) |
| 58 | 57 | ralrimiva 3146 |
. . 3
⊢ (𝑑 ∈ 𝑆 → ∀𝑐 ∈ ω ((rank “ ((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On ∧ dom OrdIso( E ,
(rank “ ((𝑈‘𝑑)‘𝑐))) ∈ ∪ ran
𝐻)) |
| 59 | | eqid 2737 |
. . . 4
⊢ OrdIso( E
, ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) |
| 60 | 42, 59 | hsmexlem3 10468 |
. . 3
⊢
(((ω ≼* ω ∧ ∪ ran 𝐻 ∈ On) ∧ ∀𝑐 ∈ ω ((rank “ ((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On ∧ dom OrdIso( E ,
(rank “ ((𝑈‘𝑑)‘𝑐))) ∈ ∪ ran
𝐻)) → dom OrdIso( E ,
∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) ∈ (har‘𝒫 (ω
× ∪ ran 𝐻))) |
| 61 | 27, 39, 58, 60 | syl21anc 838 |
. 2
⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) ∈ (har‘𝒫 (ω
× ∪ ran 𝐻))) |
| 62 | 24, 61 | eqeltrd 2841 |
1
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) ∈ (har‘𝒫 (ω
× ∪ ran 𝐻))) |