Metamath Proof Explorer

Theorem hsmexlem5

Description: Lemma for hsmex . Combining the above constraints, along with itunitc and tcrank , gives an effective constraint on the rank of S . (Contributed by Stefan O'Rear, 14-Feb-2015)

Ref Expression
Hypotheses hsmexlem4.x ⊢ 𝑋 ∈ V
hsmexlem4.h ⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω )
hsmexlem4.u ⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
hsmexlem4.s ⊢ 𝑆 = { 𝑎 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑏 ∈ ( TC ‘ { 𝑎 } ) 𝑏 ≼ 𝑋 }
hsmexlem4.o ⊢ 𝑂 = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
Assertion hsmexlem5 ( 𝑑 ∈ 𝑆 → ( rank ‘ 𝑑 ) ∈ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 hsmexlem4.x ⊢ 𝑋 ∈ V
2 hsmexlem4.h ⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω )
3 hsmexlem4.u ⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
4 hsmexlem4.s ⊢ 𝑆 = { 𝑎 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑏 ∈ ( TC ‘ { 𝑎 } ) 𝑏 ≼ 𝑋 }
5 hsmexlem4.o ⊢ 𝑂 = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
6 4 ssrab3 ⊢ 𝑆 ⊆ ∪ ( 𝑅1 “ On )
7 6 sseli ⊢ ( 𝑑 ∈ 𝑆 → 𝑑 ∈ ∪ ( 𝑅1 “ On ) )
8 tcrank ⊢ ( 𝑑 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝑑 ) = ( rank “ ( TC ‘ 𝑑 ) ) )
9 7 8 syl ⊢ ( 𝑑 ∈ 𝑆 → ( rank ‘ 𝑑 ) = ( rank “ ( TC ‘ 𝑑 ) ) )
10 3 itunitc ⊢ ( TC ‘ 𝑑 ) = ∪ ran ( 𝑈 ‘ 𝑑 )
11 3 itunifn ⊢ ( 𝑑 ∈ 𝑆 → ( 𝑈 ‘ 𝑑 ) Fn ω )
12 fniunfv ⊢ ( ( 𝑈 ‘ 𝑑 ) Fn ω → ∪ 𝑐 ∈ ω ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) = ∪ ran ( 𝑈 ‘ 𝑑 ) )
13 11 12 syl ⊢ ( 𝑑 ∈ 𝑆 → ∪ 𝑐 ∈ ω ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) = ∪ ran ( 𝑈 ‘ 𝑑 ) )
14 10 13 eqtr4id ⊢ ( 𝑑 ∈ 𝑆 → ( TC ‘ 𝑑 ) = ∪ 𝑐 ∈ ω ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) )
15 14 imaeq2d ⊢ ( 𝑑 ∈ 𝑆 → ( rank “ ( TC ‘ 𝑑 ) ) = ( rank “ ∪ 𝑐 ∈ ω ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
16 imaiun ⊢ ( rank “ ∪ 𝑐 ∈ ω ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) = ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) )
17 16 a1i ⊢ ( 𝑑 ∈ 𝑆 → ( rank “ ∪ 𝑐 ∈ ω ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) = ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
18 9 15 17 3eqtrd ⊢ ( 𝑑 ∈ 𝑆 → ( rank ‘ 𝑑 ) = ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
19 dmresi ⊢ dom ( I ↾ ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) )
20 18 19 eqtr4di ⊢ ( 𝑑 ∈ 𝑆 → ( rank ‘ 𝑑 ) = dom ( I ↾ ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) )
21 rankon ⊢ ( rank ‘ 𝑑 ) ∈ On
22 18 21 eqeltrrdi ⊢ ( 𝑑 ∈ 𝑆 → ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ∈ On )
23 eloni ⊢ ( ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ∈ On → Ord ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
24 oiid ⊢ ( Ord ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) → OrdIso ( E , ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = ( I ↾ ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) )
25 22 23 24 3syl ⊢ ( 𝑑 ∈ 𝑆 → OrdIso ( E , ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = ( I ↾ ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) )
26 25 dmeqd ⊢ ( 𝑑 ∈ 𝑆 → dom OrdIso ( E , ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = dom ( I ↾ ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) )
27 20 26 eqtr4d ⊢ ( 𝑑 ∈ 𝑆 → ( rank ‘ 𝑑 ) = dom OrdIso ( E , ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) )
28 omex ⊢ ω ∈ V
29 wdomref ⊢ ( ω ∈ V → ω ≼* ω )
30 28 29 mp1i ⊢ ( 𝑑 ∈ 𝑆 → ω ≼* ω )
31 frfnom ⊢ ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω ) Fn ω
32 2 fneq1i ⊢ ( 𝐻 Fn ω ↔ ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω ) Fn ω )
33 31 32 mpbir ⊢ 𝐻 Fn ω
34 fniunfv ⊢ ( 𝐻 Fn ω → ∪ 𝑎 ∈ ω ( 𝐻 ‘ 𝑎 ) = ∪ ran 𝐻 )
35 33 34 ax-mp ⊢ ∪ 𝑎 ∈ ω ( 𝐻 ‘ 𝑎 ) = ∪ ran 𝐻
36 iunon ⊢ ( ( ω ∈ V ∧ ∀ 𝑎 ∈ ω ( 𝐻 ‘ 𝑎 ) ∈ On ) → ∪ 𝑎 ∈ ω ( 𝐻 ‘ 𝑎 ) ∈ On )
37 28 36 mpan ⊢ ( ∀ 𝑎 ∈ ω ( 𝐻 ‘ 𝑎 ) ∈ On → ∪ 𝑎 ∈ ω ( 𝐻 ‘ 𝑎 ) ∈ On )
38 2 hsmexlem9 ⊢ ( 𝑎 ∈ ω → ( 𝐻 ‘ 𝑎 ) ∈ On )
39 37 38 mprg ⊢ ∪ 𝑎 ∈ ω ( 𝐻 ‘ 𝑎 ) ∈ On
40 35 39 eqeltrri ⊢ ∪ ran 𝐻 ∈ On
41 40 a1i ⊢ ( 𝑑 ∈ 𝑆 → ∪ ran 𝐻 ∈ On )
42 fvssunirn ⊢ ( 𝐻 ‘ 𝑐 ) ⊆ ∪ ran 𝐻
43 eqid ⊢ OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
44 1 2 3 4 43 hsmexlem4 ⊢ ( ( 𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆 ) → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) ∈ ( 𝐻 ‘ 𝑐 ) )
45 44 ancoms ⊢ ( ( 𝑑 ∈ 𝑆 ∧ 𝑐 ∈ ω ) → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) ∈ ( 𝐻 ‘ 𝑐 ) )
46 42 45 sselid ⊢ ( ( 𝑑 ∈ 𝑆 ∧ 𝑐 ∈ ω ) → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) ∈ ∪ ran 𝐻 )
47 imassrn ⊢ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ⊆ ran rank
48 rankf ⊢ rank : ∪ ( 𝑅1 “ On ) ⟶ On
49 frn ⊢ ( rank : ∪ ( 𝑅1 “ On ) ⟶ On → ran rank ⊆ On )
50 48 49 ax-mp ⊢ ran rank ⊆ On
51 47 50 sstri ⊢ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ⊆ On
52 ffun ⊢ ( rank : ∪ ( 𝑅1 “ On ) ⟶ On → Fun rank )
53 fvex ⊢ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ∈ V
54 53 funimaex ⊢ ( Fun rank → ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ∈ V )
55 48 52 54 mp2b ⊢ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ∈ V
56 55 elpw ⊢ ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ∈ 𝒫 On ↔ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ⊆ On )
57 51 56 mpbir ⊢ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ∈ 𝒫 On
58 46 57 jctil ⊢ ( ( 𝑑 ∈ 𝑆 ∧ 𝑐 ∈ ω ) → ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ∈ 𝒫 On ∧ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) ∈ ∪ ran 𝐻 ) )
59 58 ralrimiva ⊢ ( 𝑑 ∈ 𝑆 → ∀ 𝑐 ∈ ω ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ∈ 𝒫 On ∧ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) ∈ ∪ ran 𝐻 ) )
60 eqid ⊢ OrdIso ( E , ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = OrdIso ( E , ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
61 43 60 hsmexlem3 ⊢ ( ( ( ω ≼* ω ∧ ∪ ran 𝐻 ∈ On ) ∧ ∀ 𝑐 ∈ ω ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ∈ 𝒫 On ∧ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) ∈ ∪ ran 𝐻 ) ) → dom OrdIso ( E , ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) ∈ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) )
62 30 41 59 61 syl21anc ⊢ ( 𝑑 ∈ 𝑆 → dom OrdIso ( E , ∪ 𝑐 ∈ ω ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) ∈ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) )
63 27 62 eqeltrd ⊢ ( 𝑑 ∈ 𝑆 → ( rank ‘ 𝑑 ) ∈ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) )