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

Theorem hsmexlem4 10424
Description: Lemma for hsmex 10427. The core induction, establishing bounds on the order types of iterated unions of the initial set. (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
hsmexlem4 ((𝑐 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆) β†’ dom 𝑂 ∈ (π»β€˜π‘))
Distinct variable groups:   π‘Ž,𝑐,𝑑,𝐻   𝑆,𝑐,𝑑   π‘ˆ,𝑐,𝑑   π‘Ž,𝑏,𝑧,𝑋   π‘₯,π‘Ž,𝑦   𝑏,𝑐,𝑑,π‘₯,𝑦,𝑧
Allowed substitution hints:   𝑆(π‘₯,𝑦,𝑧,π‘Ž,𝑏)   π‘ˆ(π‘₯,𝑦,𝑧,π‘Ž,𝑏)   𝐻(π‘₯,𝑦,𝑧,𝑏)   𝑂(π‘₯,𝑦,𝑧,π‘Ž,𝑏,𝑐,𝑑)   𝑋(π‘₯,𝑦,𝑐,𝑑)

Proof of Theorem hsmexlem4
Dummy variables 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hsmexlem4.o . . . . . . 7 𝑂 = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)))
2 fveq2 6892 . . . . . . . . 9 (𝑐 = βˆ… β†’ ((π‘ˆβ€˜π‘‘)β€˜π‘) = ((π‘ˆβ€˜π‘‘)β€˜βˆ…))
32imaeq2d 6060 . . . . . . . 8 (𝑐 = βˆ… β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)))
4 oieq2 9508 . . . . . . . 8 ((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))))
53, 4syl 17 . . . . . . 7 (𝑐 = βˆ… β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))))
61, 5eqtrid 2785 . . . . . 6 (𝑐 = βˆ… β†’ 𝑂 = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))))
76dmeqd 5906 . . . . 5 (𝑐 = βˆ… β†’ dom 𝑂 = dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))))
8 fveq2 6892 . . . . 5 (𝑐 = βˆ… β†’ (π»β€˜π‘) = (π»β€˜βˆ…))
97, 8eleq12d 2828 . . . 4 (𝑐 = βˆ… β†’ (dom 𝑂 ∈ (π»β€˜π‘) ↔ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (π»β€˜βˆ…)))
109ralbidv 3178 . . 3 (𝑐 = βˆ… β†’ (βˆ€π‘‘ ∈ 𝑆 dom 𝑂 ∈ (π»β€˜π‘) ↔ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (π»β€˜βˆ…)))
11 fveq2 6892 . . . . . . . . 9 (𝑐 = 𝑒 β†’ ((π‘ˆβ€˜π‘‘)β€˜π‘) = ((π‘ˆβ€˜π‘‘)β€˜π‘’))
1211imaeq2d 6060 . . . . . . . 8 (𝑐 = 𝑒 β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’)))
13 oieq2 9508 . . . . . . . 8 ((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’)) β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))))
1412, 13syl 17 . . . . . . 7 (𝑐 = 𝑒 β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))))
151, 14eqtrid 2785 . . . . . 6 (𝑐 = 𝑒 β†’ 𝑂 = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))))
1615dmeqd 5906 . . . . 5 (𝑐 = 𝑒 β†’ dom 𝑂 = dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))))
17 fveq2 6892 . . . . 5 (𝑐 = 𝑒 β†’ (π»β€˜π‘) = (π»β€˜π‘’))
1816, 17eleq12d 2828 . . . 4 (𝑐 = 𝑒 β†’ (dom 𝑂 ∈ (π»β€˜π‘) ↔ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’)))
1918ralbidv 3178 . . 3 (𝑐 = 𝑒 β†’ (βˆ€π‘‘ ∈ 𝑆 dom 𝑂 ∈ (π»β€˜π‘) ↔ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’)))
20 fveq2 6892 . . . . . . . . 9 (𝑐 = suc 𝑒 β†’ ((π‘ˆβ€˜π‘‘)β€˜π‘) = ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))
2120imaeq2d 6060 . . . . . . . 8 (𝑐 = suc 𝑒 β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒)))
22 oieq2 9508 . . . . . . . 8 ((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒)) β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))))
2321, 22syl 17 . . . . . . 7 (𝑐 = suc 𝑒 β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))))
241, 23eqtrid 2785 . . . . . 6 (𝑐 = suc 𝑒 β†’ 𝑂 = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))))
2524dmeqd 5906 . . . . 5 (𝑐 = suc 𝑒 β†’ dom 𝑂 = dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))))
26 fveq2 6892 . . . . 5 (𝑐 = suc 𝑒 β†’ (π»β€˜π‘) = (π»β€˜suc 𝑒))
2725, 26eleq12d 2828 . . . 4 (𝑐 = suc 𝑒 β†’ (dom 𝑂 ∈ (π»β€˜π‘) ↔ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (π»β€˜suc 𝑒)))
2827ralbidv 3178 . . 3 (𝑐 = suc 𝑒 β†’ (βˆ€π‘‘ ∈ 𝑆 dom 𝑂 ∈ (π»β€˜π‘) ↔ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (π»β€˜suc 𝑒)))
29 imassrn 6071 . . . . . . 7 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) βŠ† ran rank
30 rankf 9789 . . . . . . . 8 rank:βˆͺ (𝑅1 β€œ On)⟢On
31 frn 6725 . . . . . . . 8 (rank:βˆͺ (𝑅1 β€œ On)⟢On β†’ ran rank βŠ† On)
3230, 31ax-mp 5 . . . . . . 7 ran rank βŠ† On
3329, 32sstri 3992 . . . . . 6 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) βŠ† On
34 hsmexlem4.u . . . . . . . . . 10 π‘ˆ = (π‘₯ ∈ V ↦ (rec((𝑦 ∈ V ↦ βˆͺ 𝑦), π‘₯) β†Ύ Ο‰))
3534ituni0 10413 . . . . . . . . 9 (𝑑 ∈ V β†’ ((π‘ˆβ€˜π‘‘)β€˜βˆ…) = 𝑑)
3635elv 3481 . . . . . . . 8 ((π‘ˆβ€˜π‘‘)β€˜βˆ…) = 𝑑
3736imaeq2i 6058 . . . . . . 7 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) = (rank β€œ 𝑑)
38 ffun 6721 . . . . . . . . . 10 (rank:βˆͺ (𝑅1 β€œ On)⟢On β†’ Fun rank)
3930, 38ax-mp 5 . . . . . . . . 9 Fun rank
40 vex 3479 . . . . . . . . 9 𝑑 ∈ V
41 wdomimag 9582 . . . . . . . . 9 ((Fun rank ∧ 𝑑 ∈ V) β†’ (rank β€œ 𝑑) β‰Ό* 𝑑)
4239, 40, 41mp2an 691 . . . . . . . 8 (rank β€œ 𝑑) β‰Ό* 𝑑
43 sneq 4639 . . . . . . . . . . . . 13 (π‘Ž = 𝑑 β†’ {π‘Ž} = {𝑑})
4443fveq2d 6896 . . . . . . . . . . . 12 (π‘Ž = 𝑑 β†’ (TCβ€˜{π‘Ž}) = (TCβ€˜{𝑑}))
4544raleqdv 3326 . . . . . . . . . . 11 (π‘Ž = 𝑑 β†’ (βˆ€π‘ ∈ (TCβ€˜{π‘Ž})𝑏 β‰Ό 𝑋 ↔ βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋))
46 hsmexlem4.s . . . . . . . . . . 11 𝑆 = {π‘Ž ∈ βˆͺ (𝑅1 β€œ On) ∣ βˆ€π‘ ∈ (TCβ€˜{π‘Ž})𝑏 β‰Ό 𝑋}
4745, 46elrab2 3687 . . . . . . . . . 10 (𝑑 ∈ 𝑆 ↔ (𝑑 ∈ βˆͺ (𝑅1 β€œ On) ∧ βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋))
4847simprbi 498 . . . . . . . . 9 (𝑑 ∈ 𝑆 β†’ βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋)
49 vsnex 5430 . . . . . . . . . . . 12 {𝑑} ∈ V
50 tcid 9734 . . . . . . . . . . . 12 ({𝑑} ∈ V β†’ {𝑑} βŠ† (TCβ€˜{𝑑}))
5149, 50ax-mp 5 . . . . . . . . . . 11 {𝑑} βŠ† (TCβ€˜{𝑑})
52 vsnid 4666 . . . . . . . . . . 11 𝑑 ∈ {𝑑}
5351, 52sselii 3980 . . . . . . . . . 10 𝑑 ∈ (TCβ€˜{𝑑})
54 breq1 5152 . . . . . . . . . . 11 (𝑏 = 𝑑 β†’ (𝑏 β‰Ό 𝑋 ↔ 𝑑 β‰Ό 𝑋))
5554rspcv 3609 . . . . . . . . . 10 (𝑑 ∈ (TCβ€˜{𝑑}) β†’ (βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋 β†’ 𝑑 β‰Ό 𝑋))
5653, 55ax-mp 5 . . . . . . . . 9 (βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋 β†’ 𝑑 β‰Ό 𝑋)
57 domwdom 9569 . . . . . . . . 9 (𝑑 β‰Ό 𝑋 β†’ 𝑑 β‰Ό* 𝑋)
5848, 56, 573syl 18 . . . . . . . 8 (𝑑 ∈ 𝑆 β†’ 𝑑 β‰Ό* 𝑋)
59 wdomtr 9570 . . . . . . . 8 (((rank β€œ 𝑑) β‰Ό* 𝑑 ∧ 𝑑 β‰Ό* 𝑋) β†’ (rank β€œ 𝑑) β‰Ό* 𝑋)
6042, 58, 59sylancr 588 . . . . . . 7 (𝑑 ∈ 𝑆 β†’ (rank β€œ 𝑑) β‰Ό* 𝑋)
6137, 60eqbrtrid 5184 . . . . . 6 (𝑑 ∈ 𝑆 β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) β‰Ό* 𝑋)
62 eqid 2733 . . . . . . 7 OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)))
6362hsmexlem1 10421 . . . . . 6 (((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) βŠ† On ∧ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) β‰Ό* 𝑋) β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (harβ€˜π’« 𝑋))
6433, 61, 63sylancr 588 . . . . 5 (𝑑 ∈ 𝑆 β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (harβ€˜π’« 𝑋))
65 hsmexlem4.h . . . . . 6 𝐻 = (rec((𝑧 ∈ V ↦ (harβ€˜π’« (𝑋 Γ— 𝑧))), (harβ€˜π’« 𝑋)) β†Ύ Ο‰)
6665hsmexlem7 10418 . . . . 5 (π»β€˜βˆ…) = (harβ€˜π’« 𝑋)
6764, 66eleqtrrdi 2845 . . . 4 (𝑑 ∈ 𝑆 β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (π»β€˜βˆ…))
6867rgen 3064 . . 3 βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (π»β€˜βˆ…)
69 nfra1 3282 . . . . . 6 β„²π‘‘βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’)
70 nfv 1918 . . . . . 6 Ⅎ𝑑 𝑒 ∈ Ο‰
7169, 70nfan 1903 . . . . 5 Ⅎ𝑑(βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ 𝑒 ∈ Ο‰)
7234ituniiun 10417 . . . . . . . . . . . . 13 (𝑑 ∈ V β†’ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒) = βˆͺ 𝑓 ∈ 𝑑 ((π‘ˆβ€˜π‘“)β€˜π‘’))
7372elv 3481 . . . . . . . . . . . 12 ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒) = βˆͺ 𝑓 ∈ 𝑑 ((π‘ˆβ€˜π‘“)β€˜π‘’)
7473imaeq2i 6058 . . . . . . . . . . 11 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒)) = (rank β€œ βˆͺ 𝑓 ∈ 𝑑 ((π‘ˆβ€˜π‘“)β€˜π‘’))
75 imaiun 7244 . . . . . . . . . . 11 (rank β€œ βˆͺ 𝑓 ∈ 𝑑 ((π‘ˆβ€˜π‘“)β€˜π‘’)) = βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))
7674, 75eqtri 2761 . . . . . . . . . 10 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒)) = βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))
77 oieq2 9508 . . . . . . . . . 10 ((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒)) = βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) = OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))))
7876, 77ax-mp 5 . . . . . . . . 9 OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) = OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
7978dmeqi 5905 . . . . . . . 8 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) = dom OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
8058ad2antll 728 . . . . . . . . 9 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ 𝑑 β‰Ό* 𝑋)
8165hsmexlem9 10420 . . . . . . . . . 10 (𝑒 ∈ Ο‰ β†’ (π»β€˜π‘’) ∈ On)
8281ad2antrl 727 . . . . . . . . 9 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ (π»β€˜π‘’) ∈ On)
83 fveq2 6892 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑓 β†’ (π‘ˆβ€˜π‘‘) = (π‘ˆβ€˜π‘“))
8483fveq1d 6894 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑓 β†’ ((π‘ˆβ€˜π‘‘)β€˜π‘’) = ((π‘ˆβ€˜π‘“)β€˜π‘’))
8584imaeq2d 6060 . . . . . . . . . . . . . . 15 (𝑑 = 𝑓 β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’)) = (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
86 oieq2 9508 . . . . . . . . . . . . . . 15 ((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’)) = (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))))
8785, 86syl 17 . . . . . . . . . . . . . 14 (𝑑 = 𝑓 β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))))
8887dmeqd 5906 . . . . . . . . . . . . 13 (𝑑 = 𝑓 β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) = dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))))
8988eleq1d 2819 . . . . . . . . . . . 12 (𝑑 = 𝑓 β†’ (dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ↔ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (π»β€˜π‘’)))
90 simpll 766 . . . . . . . . . . . 12 (((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) β†’ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’))
9146ssrab3 4081 . . . . . . . . . . . . . . . . . 18 𝑆 βŠ† βˆͺ (𝑅1 β€œ On)
9291sseli 3979 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ 𝑆 β†’ 𝑑 ∈ βˆͺ (𝑅1 β€œ On))
93 r1elssi 9800 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝑑 βŠ† βˆͺ (𝑅1 β€œ On))
9492, 93syl 17 . . . . . . . . . . . . . . . 16 (𝑑 ∈ 𝑆 β†’ 𝑑 βŠ† βˆͺ (𝑅1 β€œ On))
9594sselda 3983 . . . . . . . . . . . . . . 15 ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) β†’ 𝑓 ∈ βˆͺ (𝑅1 β€œ On))
96 snssi 4812 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ 𝑑 β†’ {𝑓} βŠ† 𝑑)
9740tcss 9739 . . . . . . . . . . . . . . . . . . 19 ({𝑓} βŠ† 𝑑 β†’ (TCβ€˜{𝑓}) βŠ† (TCβ€˜π‘‘))
9896, 97syl 17 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ 𝑑 β†’ (TCβ€˜{𝑓}) βŠ† (TCβ€˜π‘‘))
9949tcel 9740 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ {𝑑} β†’ (TCβ€˜π‘‘) βŠ† (TCβ€˜{𝑑}))
10052, 99mp1i 13 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ 𝑑 β†’ (TCβ€˜π‘‘) βŠ† (TCβ€˜{𝑑}))
10198, 100sstrd 3993 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ 𝑑 β†’ (TCβ€˜{𝑓}) βŠ† (TCβ€˜{𝑑}))
102 ssralv 4051 . . . . . . . . . . . . . . . . 17 ((TCβ€˜{𝑓}) βŠ† (TCβ€˜{𝑑}) β†’ (βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋 β†’ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋))
103101, 102syl 17 . . . . . . . . . . . . . . . 16 (𝑓 ∈ 𝑑 β†’ (βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋 β†’ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋))
10448, 103mpan9 508 . . . . . . . . . . . . . . 15 ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) β†’ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋)
105 sneq 4639 . . . . . . . . . . . . . . . . . 18 (π‘Ž = 𝑓 β†’ {π‘Ž} = {𝑓})
106105fveq2d 6896 . . . . . . . . . . . . . . . . 17 (π‘Ž = 𝑓 β†’ (TCβ€˜{π‘Ž}) = (TCβ€˜{𝑓}))
107106raleqdv 3326 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑓 β†’ (βˆ€π‘ ∈ (TCβ€˜{π‘Ž})𝑏 β‰Ό 𝑋 ↔ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋))
108107, 46elrab2 3687 . . . . . . . . . . . . . . 15 (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ βˆͺ (𝑅1 β€œ On) ∧ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋))
10995, 104, 108sylanbrc 584 . . . . . . . . . . . . . 14 ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) β†’ 𝑓 ∈ 𝑆)
110109adantll 713 . . . . . . . . . . . . 13 (((𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆) ∧ 𝑓 ∈ 𝑑) β†’ 𝑓 ∈ 𝑆)
111110adantll 713 . . . . . . . . . . . 12 (((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) β†’ 𝑓 ∈ 𝑆)
11289, 90, 111rspcdva 3614 . . . . . . . . . . 11 (((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (π»β€˜π‘’))
113 imassrn 6071 . . . . . . . . . . . . 13 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) βŠ† ran rank
114113, 32sstri 3992 . . . . . . . . . . . 12 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) βŠ† On
115 fvex 6905 . . . . . . . . . . . . . . 15 ((π‘ˆβ€˜π‘“)β€˜π‘’) ∈ V
116115funimaex 6637 . . . . . . . . . . . . . 14 (Fun rank β†’ (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ V)
11739, 116ax-mp 5 . . . . . . . . . . . . 13 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ V
118117elpw 4607 . . . . . . . . . . . 12 ((rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ 𝒫 On ↔ (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) βŠ† On)
119114, 118mpbir 230 . . . . . . . . . . 11 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ 𝒫 On
120112, 119jctil 521 . . . . . . . . . 10 (((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) β†’ ((rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (π»β€˜π‘’)))
121120ralrimiva 3147 . . . . . . . . 9 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ βˆ€π‘“ ∈ 𝑑 ((rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (π»β€˜π‘’)))
122 eqid 2733 . . . . . . . . . 10 OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
123 eqid 2733 . . . . . . . . . 10 OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) = OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
124122, 123hsmexlem3 10423 . . . . . . . . 9 (((𝑑 β‰Ό* 𝑋 ∧ (π»β€˜π‘’) ∈ On) ∧ βˆ€π‘“ ∈ 𝑑 ((rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (π»β€˜π‘’))) β†’ dom OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
12580, 82, 121, 124syl21anc 837 . . . . . . . 8 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ dom OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
12679, 125eqeltrid 2838 . . . . . . 7 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
12765hsmexlem8 10419 . . . . . . . 8 (𝑒 ∈ Ο‰ β†’ (π»β€˜suc 𝑒) = (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
128127ad2antrl 727 . . . . . . 7 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ (π»β€˜suc 𝑒) = (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
129126, 128eleqtrrd 2837 . . . . . 6 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (π»β€˜suc 𝑒))
130129expr 458 . . . . 5 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ 𝑒 ∈ Ο‰) β†’ (𝑑 ∈ 𝑆 β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (π»β€˜suc 𝑒)))
13171, 130ralrimi 3255 . . . 4 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ 𝑒 ∈ Ο‰) β†’ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (π»β€˜suc 𝑒))
132131expcom 415 . . 3 (𝑒 ∈ Ο‰ β†’ (βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) β†’ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (π»β€˜suc 𝑒)))
13310, 19, 28, 68, 132finds1 7892 . 2 (𝑐 ∈ Ο‰ β†’ βˆ€π‘‘ ∈ 𝑆 dom 𝑂 ∈ (π»β€˜π‘))
134133r19.21bi 3249 1 ((𝑐 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆) β†’ dom 𝑂 ∈ (π»β€˜π‘))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  {crab 3433  Vcvv 3475   βŠ† wss 3949  βˆ…c0 4323  π’« cpw 4603  {csn 4629  βˆͺ cuni 4909  βˆͺ ciun 4998   class class class wbr 5149   ↦ cmpt 5232   E cep 5580   Γ— cxp 5675  dom cdm 5677  ran crn 5678   β†Ύ cres 5679   β€œ cima 5680  Oncon0 6365  suc csuc 6367  Fun wfun 6538  βŸΆwf 6540  β€˜cfv 6544  Ο‰com 7855  reccrdg 8409   β‰Ό cdom 8937  OrdIsocoi 9504  harchar 9551   β‰Ό* cwdom 9559  TCctc 9731  π‘…1cr1 9757  rankcrnk 9758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-smo 8346  df-recs 8371  df-rdg 8410  df-en 8940  df-dom 8941  df-sdom 8942  df-oi 9505  df-har 9552  df-wdom 9560  df-tc 9732  df-r1 9759  df-rank 9760
This theorem is referenced by:  hsmexlem5  10425
  Copyright terms: Public domain W3C validator