Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  hsmexlem5 Structured version   Visualization version   GIF version

Theorem hsmexlem5 9841
 Description: Lemma for hsmex 9843. Combining the above constraints, along with itunitc 9832 and tcrank 9301, gives an effective constraint on the rank of 𝑆. (Contributed by Stefan O'Rear, 14-Feb-2015.)
Hypotheses
Ref Expression
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
Ref Expression
hsmexlem5 (𝑑𝑆 → (rank‘𝑑) ∈ (har‘𝒫 (ω × ran 𝐻)))
Distinct variable groups:   𝑎,𝑐,𝑑,𝐻   𝑆,𝑐,𝑑   𝑈,𝑐,𝑑   𝑎,𝑏,𝑧,𝑋   𝑥,𝑎,𝑦   𝑏,𝑐,𝑑,𝑥,𝑦,𝑧
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑧,𝑎,𝑏)   𝑈(𝑥,𝑦,𝑧,𝑎,𝑏)   𝐻(𝑥,𝑦,𝑧,𝑏)   𝑂(𝑥,𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝑋(𝑥,𝑦,𝑐,𝑑)

Proof of Theorem hsmexlem5
StepHypRef Expression
1 hsmexlem4.s . . . . . . . 8 𝑆 = {𝑎 (𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏𝑋}
21ssrab3 4032 . . . . . . 7 𝑆 (𝑅1 “ On)
32sseli 3938 . . . . . 6 (𝑑𝑆𝑑 (𝑅1 “ On))
4 tcrank 9301 . . . . . 6 (𝑑 (𝑅1 “ On) → (rank‘𝑑) = (rank “ (TC‘𝑑)))
53, 4syl 17 . . . . 5 (𝑑𝑆 → (rank‘𝑑) = (rank “ (TC‘𝑑)))
6 hsmexlem4.u . . . . . . . . 9 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ 𝑦), 𝑥) ↾ ω))
76itunifn 9828 . . . . . . . 8 (𝑑𝑆 → (𝑈𝑑) Fn ω)
8 fniunfv 6989 . . . . . . . 8 ((𝑈𝑑) Fn ω → 𝑐 ∈ ω ((𝑈𝑑)‘𝑐) = ran (𝑈𝑑))
97, 8syl 17 . . . . . . 7 (𝑑𝑆 𝑐 ∈ ω ((𝑈𝑑)‘𝑐) = ran (𝑈𝑑))
106itunitc 9832 . . . . . . 7 (TC‘𝑑) = ran (𝑈𝑑)
119, 10syl6reqr 2876 . . . . . 6 (𝑑𝑆 → (TC‘𝑑) = 𝑐 ∈ ω ((𝑈𝑑)‘𝑐))
1211imaeq2d 5907 . . . . 5 (𝑑𝑆 → (rank “ (TC‘𝑑)) = (rank “ 𝑐 ∈ ω ((𝑈𝑑)‘𝑐)))
13 imaiun 6987 . . . . . 6 (rank “ 𝑐 ∈ ω ((𝑈𝑑)‘𝑐)) = 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))
1413a1i 11 . . . . 5 (𝑑𝑆 → (rank “ 𝑐 ∈ ω ((𝑈𝑑)‘𝑐)) = 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐)))
155, 12, 143eqtrd 2861 . . . 4 (𝑑𝑆 → (rank‘𝑑) = 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐)))
16 dmresi 5899 . . . 4 dom ( I ↾ 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))) = 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))
1715, 16eqtr4di 2875 . . 3 (𝑑𝑆 → (rank‘𝑑) = dom ( I ↾ 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))))
18 rankon 9212 . . . . . 6 (rank‘𝑑) ∈ On
1915, 18eqeltrrdi 2923 . . . . 5 (𝑑𝑆 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐)) ∈ On)
20 eloni 6179 . . . . 5 ( 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐)) ∈ On → Ord 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐)))
21 oiid 8993 . . . . 5 (Ord 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐)) → OrdIso( E , 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))) = ( I ↾ 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))))
2219, 20, 213syl 18 . . . 4 (𝑑𝑆 → OrdIso( E , 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))) = ( I ↾ 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))))
2322dmeqd 5751 . . 3 (𝑑𝑆 → dom OrdIso( E , 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))) = dom ( I ↾ 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))))
2417, 23eqtr4d 2860 . 2 (𝑑𝑆 → (rank‘𝑑) = dom OrdIso( E , 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))))
25 omex 9094 . . . 4 ω ∈ V
26 wdomref 9024 . . . 4 (ω ∈ V → ω ≼* ω)
2725, 26mp1i 13 . . 3 (𝑑𝑆 → ω ≼* ω)
28 frfnom 8057 . . . . . . 7 (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) Fn ω
29 hsmexlem4.h . . . . . . . 8 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω)
3029fneq1i 6429 . . . . . . 7 (𝐻 Fn ω ↔ (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω) Fn ω)
3128, 30mpbir 234 . . . . . 6 𝐻 Fn ω
32 fniunfv 6989 . . . . . 6 (𝐻 Fn ω → 𝑎 ∈ ω (𝐻𝑎) = ran 𝐻)
3331, 32ax-mp 5 . . . . 5 𝑎 ∈ ω (𝐻𝑎) = ran 𝐻
34 iunon 7963 . . . . . . 7 ((ω ∈ V ∧ ∀𝑎 ∈ ω (𝐻𝑎) ∈ On) → 𝑎 ∈ ω (𝐻𝑎) ∈ On)
3525, 34mpan 689 . . . . . 6 (∀𝑎 ∈ ω (𝐻𝑎) ∈ On → 𝑎 ∈ ω (𝐻𝑎) ∈ On)
3629hsmexlem9 9836 . . . . . 6 (𝑎 ∈ ω → (𝐻𝑎) ∈ On)
3735, 36mprg 3144 . . . . 5 𝑎 ∈ ω (𝐻𝑎) ∈ On
3833, 37eqeltrri 2911 . . . 4 ran 𝐻 ∈ On
3938a1i 11 . . 3 (𝑑𝑆 ran 𝐻 ∈ On)
40 fvssunirn 6681 . . . . . 6 (𝐻𝑐) ⊆ ran 𝐻
41 hsmexlem4.x . . . . . . . 8 𝑋 ∈ V
42 eqid 2822 . . . . . . . 8 OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐)))
4341, 29, 6, 1, 42hsmexlem4 9840 . . . . . . 7 ((𝑐 ∈ ω ∧ 𝑑𝑆) → dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) ∈ (𝐻𝑐))
4443ancoms 462 . . . . . 6 ((𝑑𝑆𝑐 ∈ ω) → dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) ∈ (𝐻𝑐))
4540, 44sseldi 3940 . . . . 5 ((𝑑𝑆𝑐 ∈ ω) → dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) ∈ ran 𝐻)
46 imassrn 5918 . . . . . . 7 (rank “ ((𝑈𝑑)‘𝑐)) ⊆ ran rank
47 rankf 9211 . . . . . . . 8 rank: (𝑅1 “ On)⟶On
48 frn 6500 . . . . . . . 8 (rank: (𝑅1 “ On)⟶On → ran rank ⊆ On)
4947, 48ax-mp 5 . . . . . . 7 ran rank ⊆ On
5046, 49sstri 3951 . . . . . 6 (rank “ ((𝑈𝑑)‘𝑐)) ⊆ On
51 ffun 6497 . . . . . . . 8 (rank: (𝑅1 “ On)⟶On → Fun rank)
52 fvex 6665 . . . . . . . . 9 ((𝑈𝑑)‘𝑐) ∈ V
5352funimaex 6420 . . . . . . . 8 (Fun rank → (rank “ ((𝑈𝑑)‘𝑐)) ∈ V)
5447, 51, 53mp2b 10 . . . . . . 7 (rank “ ((𝑈𝑑)‘𝑐)) ∈ V
5554elpw 4515 . . . . . 6 ((rank “ ((𝑈𝑑)‘𝑐)) ∈ 𝒫 On ↔ (rank “ ((𝑈𝑑)‘𝑐)) ⊆ On)
5650, 55mpbir 234 . . . . 5 (rank “ ((𝑈𝑑)‘𝑐)) ∈ 𝒫 On
5745, 56jctil 523 . . . 4 ((𝑑𝑆𝑐 ∈ ω) → ((rank “ ((𝑈𝑑)‘𝑐)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) ∈ ran 𝐻))
5857ralrimiva 3174 . . 3 (𝑑𝑆 → ∀𝑐 ∈ ω ((rank “ ((𝑈𝑑)‘𝑐)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) ∈ ran 𝐻))
59 eqid 2822 . . . 4 OrdIso( E , 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐)))
6042, 59hsmexlem3 9839 . . 3 (((ω ≼* ω ∧ ran 𝐻 ∈ On) ∧ ∀𝑐 ∈ ω ((rank “ ((𝑈𝑑)‘𝑐)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) ∈ ran 𝐻)) → dom OrdIso( E , 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))) ∈ (har‘𝒫 (ω × ran 𝐻)))
6127, 39, 58, 60syl21anc 836 . 2 (𝑑𝑆 → dom OrdIso( E , 𝑐 ∈ ω (rank “ ((𝑈𝑑)‘𝑐))) ∈ (har‘𝒫 (ω × ran 𝐻)))
6224, 61eqeltrd 2914 1 (𝑑𝑆 → (rank‘𝑑) ∈ (har‘𝒫 (ω × ran 𝐻)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2114  ∀wral 3130  {crab 3134  Vcvv 3469   ⊆ wss 3908  𝒫 cpw 4511  {csn 4539  ∪ cuni 4813  ∪ ciun 4894   class class class wbr 5042   ↦ cmpt 5122   I cid 5436   E cep 5441   × cxp 5530  dom cdm 5532  ran crn 5533   ↾ cres 5534   “ cima 5535  Ord word 6168  Oncon0 6169  Fun wfun 6328   Fn wfn 6329  ⟶wf 6330  ‘cfv 6334  ωcom 7565  reccrdg 8032   ≼ cdom 8494  OrdIsocoi 8961  harchar 9008   ≼* cwdom 9016  TCctc 9166  𝑅1cr1 9179  rankcrnk 9180 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-inf2 9092 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-iin 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-se 5492  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-isom 6343  df-riota 7098  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-smo 7970  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-oi 8962  df-har 9009  df-wdom 9017  df-tc 9167  df-r1 9181  df-rank 9182 This theorem is referenced by:  hsmexlem6  9842
 Copyright terms: Public domain W3C validator