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 𝐻 ) ) )