Proof of Theorem hsmexlem5
Step | Hyp | Ref
| Expression |
1 | | hsmexlem4.s |
. . . . . . . 8
⊢ 𝑆 = {𝑎 ∈ ∪
(𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋} |
2 | | ssrab2 3687 |
. . . . . . . 8
⊢ {𝑎 ∈ ∪ (𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏 ≼ 𝑋} ⊆ ∪
(𝑅1 “ On) |
3 | 1, 2 | eqsstri 3635 |
. . . . . . 7
⊢ 𝑆 ⊆ ∪ (𝑅1 “ On) |
4 | 3 | sseli 3599 |
. . . . . 6
⊢ (𝑑 ∈ 𝑆 → 𝑑 ∈ ∪
(𝑅1 “ On)) |
5 | | tcrank 8747 |
. . . . . 6
⊢ (𝑑 ∈ ∪ (𝑅1 “ On) →
(rank‘𝑑) = (rank
“ (TC‘𝑑))) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) = (rank “ (TC‘𝑑))) |
7 | | hsmexlem4.u |
. . . . . . . . 9
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
8 | 7 | itunifn 9239 |
. . . . . . . 8
⊢ (𝑑 ∈ 𝑆 → (𝑈‘𝑑) Fn ω) |
9 | | fniunfv 6505 |
. . . . . . . 8
⊢ ((𝑈‘𝑑) Fn ω → ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐) = ∪ ran (𝑈‘𝑑)) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝑑 ∈ 𝑆 → ∪
𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐) = ∪ ran (𝑈‘𝑑)) |
11 | 7 | itunitc 9243 |
. . . . . . 7
⊢
(TC‘𝑑) = ∪ ran (𝑈‘𝑑) |
12 | 10, 11 | syl6reqr 2675 |
. . . . . 6
⊢ (𝑑 ∈ 𝑆 → (TC‘𝑑) = ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐)) |
13 | 12 | imaeq2d 5466 |
. . . . 5
⊢ (𝑑 ∈ 𝑆 → (rank “ (TC‘𝑑)) = (rank “ ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐))) |
14 | | imaiun 6503 |
. . . . . 6
⊢ (rank
“ ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐)) = ∪
𝑐 ∈ ω (rank
“ ((𝑈‘𝑑)‘𝑐)) |
15 | 14 | a1i 11 |
. . . . 5
⊢ (𝑑 ∈ 𝑆 → (rank “ ∪ 𝑐 ∈ ω ((𝑈‘𝑑)‘𝑐)) = ∪
𝑐 ∈ ω (rank
“ ((𝑈‘𝑑)‘𝑐))) |
16 | 6, 13, 15 | 3eqtrd 2660 |
. . . 4
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) = ∪ 𝑐 ∈ ω (rank “
((𝑈‘𝑑)‘𝑐))) |
17 | | dmresi 5457 |
. . . 4
⊢ dom ( I
↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = ∪
𝑐 ∈ ω (rank
“ ((𝑈‘𝑑)‘𝑐)) |
18 | 16, 17 | syl6eqr 2674 |
. . 3
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) = dom ( I ↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
19 | | rankon 8658 |
. . . . . 6
⊢
(rank‘𝑑)
∈ On |
20 | 16, 19 | syl6eqelr 2710 |
. . . . 5
⊢ (𝑑 ∈ 𝑆 → ∪
𝑐 ∈ ω (rank
“ ((𝑈‘𝑑)‘𝑐)) ∈ On) |
21 | | eloni 5733 |
. . . . 5
⊢ (∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)) ∈ On → Ord ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) |
22 | | oiid 8446 |
. . . . 5
⊢ (Ord
∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)) → OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = ( I ↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
23 | 20, 21, 22 | 3syl 18 |
. . . 4
⊢ (𝑑 ∈ 𝑆 → OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = ( I ↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
24 | 23 | dmeqd 5326 |
. . 3
⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = dom ( I ↾ ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
25 | 18, 24 | eqtr4d 2659 |
. 2
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) = dom OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐)))) |
26 | | omex 8540 |
. . . 4
⊢ ω
∈ V |
27 | | wdomref 8477 |
. . . 4
⊢ (ω
∈ V → ω ≼* ω) |
28 | 26, 27 | mp1i 13 |
. . 3
⊢ (𝑑 ∈ 𝑆 → ω ≼*
ω) |
29 | | frfnom 7530 |
. . . . . . 7
⊢
(rec((𝑧 ∈ V
↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) Fn
ω |
30 | | hsmexlem4.h |
. . . . . . . 8
⊢ 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) |
31 | 30 | fneq1i 5985 |
. . . . . . 7
⊢ (𝐻 Fn ω ↔ (rec((𝑧 ∈ V ↦
(har‘𝒫 (𝑋
× 𝑧))),
(har‘𝒫 𝑋))
↾ ω) Fn ω) |
32 | 29, 31 | mpbir 221 |
. . . . . 6
⊢ 𝐻 Fn ω |
33 | | fniunfv 6505 |
. . . . . 6
⊢ (𝐻 Fn ω → ∪ 𝑎 ∈ ω (𝐻‘𝑎) = ∪ ran 𝐻) |
34 | 32, 33 | ax-mp 5 |
. . . . 5
⊢ ∪ 𝑎 ∈ ω (𝐻‘𝑎) = ∪ ran 𝐻 |
35 | | iunon 7436 |
. . . . . . 7
⊢ ((ω
∈ V ∧ ∀𝑎
∈ ω (𝐻‘𝑎) ∈ On) → ∪ 𝑎 ∈ ω (𝐻‘𝑎) ∈ On) |
36 | 26, 35 | mpan 706 |
. . . . . 6
⊢
(∀𝑎 ∈
ω (𝐻‘𝑎) ∈ On → ∪ 𝑎 ∈ ω (𝐻‘𝑎) ∈ On) |
37 | 30 | hsmexlem9 9247 |
. . . . . 6
⊢ (𝑎 ∈ ω → (𝐻‘𝑎) ∈ On) |
38 | 36, 37 | mprg 2926 |
. . . . 5
⊢ ∪ 𝑎 ∈ ω (𝐻‘𝑎) ∈ On |
39 | 34, 38 | eqeltrri 2698 |
. . . 4
⊢ ∪ ran 𝐻 ∈ On |
40 | 39 | a1i 11 |
. . 3
⊢ (𝑑 ∈ 𝑆 → ∪ ran
𝐻 ∈
On) |
41 | | fvssunirn 6217 |
. . . . . 6
⊢ (𝐻‘𝑐) ⊆ ∪ ran
𝐻 |
42 | | hsmexlem4.x |
. . . . . . . 8
⊢ 𝑋 ∈ V |
43 | | eqid 2622 |
. . . . . . . 8
⊢ OrdIso( E
, (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈‘𝑑)‘𝑐))) |
44 | 42, 30, 7, 1, 43 | hsmexlem4 9251 |
. . . . . . 7
⊢ ((𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆) → dom OrdIso( E , (rank “
((𝑈‘𝑑)‘𝑐))) ∈ (𝐻‘𝑐)) |
45 | 44 | ancoms 469 |
. . . . . 6
⊢ ((𝑑 ∈ 𝑆 ∧ 𝑐 ∈ ω) → dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑐))) ∈ (𝐻‘𝑐)) |
46 | 41, 45 | sseldi 3601 |
. . . . 5
⊢ ((𝑑 ∈ 𝑆 ∧ 𝑐 ∈ ω) → dom OrdIso( E , (rank
“ ((𝑈‘𝑑)‘𝑐))) ∈ ∪ ran
𝐻) |
47 | | imassrn 5477 |
. . . . . . 7
⊢ (rank
“ ((𝑈‘𝑑)‘𝑐)) ⊆ ran rank |
48 | | rankf 8657 |
. . . . . . . 8
⊢
rank:∪ (𝑅1 “
On)⟶On |
49 | | frn 6053 |
. . . . . . . 8
⊢
(rank:∪ (𝑅1 “
On)⟶On → ran rank ⊆ On) |
50 | 48, 49 | ax-mp 5 |
. . . . . . 7
⊢ ran rank
⊆ On |
51 | 47, 50 | sstri 3612 |
. . . . . 6
⊢ (rank
“ ((𝑈‘𝑑)‘𝑐)) ⊆ On |
52 | | ffun 6048 |
. . . . . . . 8
⊢
(rank:∪ (𝑅1 “
On)⟶On → Fun rank) |
53 | | fvex 6201 |
. . . . . . . . 9
⊢ ((𝑈‘𝑑)‘𝑐) ∈ V |
54 | 53 | funimaex 5976 |
. . . . . . . 8
⊢ (Fun rank
→ (rank “ ((𝑈‘𝑑)‘𝑐)) ∈ V) |
55 | 48, 52, 54 | mp2b 10 |
. . . . . . 7
⊢ (rank
“ ((𝑈‘𝑑)‘𝑐)) ∈ V |
56 | 55 | elpw 4164 |
. . . . . 6
⊢ ((rank
“ ((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On ↔ (rank “
((𝑈‘𝑑)‘𝑐)) ⊆ On) |
57 | 51, 56 | mpbir 221 |
. . . . 5
⊢ (rank
“ ((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On |
58 | 46, 57 | jctil 560 |
. . . 4
⊢ ((𝑑 ∈ 𝑆 ∧ 𝑐 ∈ ω) → ((rank “
((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On ∧ dom OrdIso( E ,
(rank “ ((𝑈‘𝑑)‘𝑐))) ∈ ∪ ran
𝐻)) |
59 | 58 | ralrimiva 2966 |
. . 3
⊢ (𝑑 ∈ 𝑆 → ∀𝑐 ∈ ω ((rank “ ((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On ∧ dom OrdIso( E ,
(rank “ ((𝑈‘𝑑)‘𝑐))) ∈ ∪ ran
𝐻)) |
60 | | eqid 2622 |
. . . 4
⊢ OrdIso( E
, ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) = OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) |
61 | 43, 60 | hsmexlem3 9250 |
. . 3
⊢
(((ω ≼* ω ∧ ∪ ran 𝐻 ∈ On) ∧ ∀𝑐 ∈ ω ((rank “ ((𝑈‘𝑑)‘𝑐)) ∈ 𝒫 On ∧ dom OrdIso( E ,
(rank “ ((𝑈‘𝑑)‘𝑐))) ∈ ∪ ran
𝐻)) → dom OrdIso( E ,
∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) ∈ (har‘𝒫 (ω
× ∪ ran 𝐻))) |
62 | 28, 40, 59, 61 | syl21anc 1325 |
. 2
⊢ (𝑑 ∈ 𝑆 → dom OrdIso( E , ∪ 𝑐 ∈ ω (rank “ ((𝑈‘𝑑)‘𝑐))) ∈ (har‘𝒫 (ω
× ∪ ran 𝐻))) |
63 | 25, 62 | eqeltrd 2701 |
1
⊢ (𝑑 ∈ 𝑆 → (rank‘𝑑) ∈ (har‘𝒫 (ω
× ∪ ran 𝐻))) |