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

Theorem hsmexlem4 10235
Description: Lemma for hsmex 10238. 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 6804 . . . . . . . . 9 (𝑐 = βˆ… β†’ ((π‘ˆβ€˜π‘‘)β€˜π‘) = ((π‘ˆβ€˜π‘‘)β€˜βˆ…))
32imaeq2d 5979 . . . . . . . 8 (𝑐 = βˆ… β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)))
4 oieq2 9320 . . . . . . . 8 ((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))))
53, 4syl 17 . . . . . . 7 (𝑐 = βˆ… β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))))
61, 5eqtrid 2788 . . . . . 6 (𝑐 = βˆ… β†’ 𝑂 = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))))
76dmeqd 5827 . . . . 5 (𝑐 = βˆ… β†’ dom 𝑂 = dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))))
8 fveq2 6804 . . . . 5 (𝑐 = βˆ… β†’ (π»β€˜π‘) = (π»β€˜βˆ…))
97, 8eleq12d 2831 . . . 4 (𝑐 = βˆ… β†’ (dom 𝑂 ∈ (π»β€˜π‘) ↔ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (π»β€˜βˆ…)))
109ralbidv 3171 . . 3 (𝑐 = βˆ… β†’ (βˆ€π‘‘ ∈ 𝑆 dom 𝑂 ∈ (π»β€˜π‘) ↔ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (π»β€˜βˆ…)))
11 fveq2 6804 . . . . . . . . 9 (𝑐 = 𝑒 β†’ ((π‘ˆβ€˜π‘‘)β€˜π‘) = ((π‘ˆβ€˜π‘‘)β€˜π‘’))
1211imaeq2d 5979 . . . . . . . 8 (𝑐 = 𝑒 β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’)))
13 oieq2 9320 . . . . . . . 8 ((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’)) β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))))
1412, 13syl 17 . . . . . . 7 (𝑐 = 𝑒 β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))))
151, 14eqtrid 2788 . . . . . 6 (𝑐 = 𝑒 β†’ 𝑂 = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))))
1615dmeqd 5827 . . . . 5 (𝑐 = 𝑒 β†’ dom 𝑂 = dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))))
17 fveq2 6804 . . . . 5 (𝑐 = 𝑒 β†’ (π»β€˜π‘) = (π»β€˜π‘’))
1816, 17eleq12d 2831 . . . 4 (𝑐 = 𝑒 β†’ (dom 𝑂 ∈ (π»β€˜π‘) ↔ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’)))
1918ralbidv 3171 . . 3 (𝑐 = 𝑒 β†’ (βˆ€π‘‘ ∈ 𝑆 dom 𝑂 ∈ (π»β€˜π‘) ↔ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’)))
20 fveq2 6804 . . . . . . . . 9 (𝑐 = suc 𝑒 β†’ ((π‘ˆβ€˜π‘‘)β€˜π‘) = ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))
2120imaeq2d 5979 . . . . . . . 8 (𝑐 = suc 𝑒 β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘)) = (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒)))
22 oieq2 9320 . . . . . . . 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 2788 . . . . . 6 (𝑐 = suc 𝑒 β†’ 𝑂 = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))))
2524dmeqd 5827 . . . . 5 (𝑐 = suc 𝑒 β†’ dom 𝑂 = dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))))
26 fveq2 6804 . . . . 5 (𝑐 = suc 𝑒 β†’ (π»β€˜π‘) = (π»β€˜suc 𝑒))
2725, 26eleq12d 2831 . . . 4 (𝑐 = suc 𝑒 β†’ (dom 𝑂 ∈ (π»β€˜π‘) ↔ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (π»β€˜suc 𝑒)))
2827ralbidv 3171 . . 3 (𝑐 = suc 𝑒 β†’ (βˆ€π‘‘ ∈ 𝑆 dom 𝑂 ∈ (π»β€˜π‘) ↔ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (π»β€˜suc 𝑒)))
29 imassrn 5990 . . . . . . 7 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) βŠ† ran rank
30 rankf 9600 . . . . . . . 8 rank:βˆͺ (𝑅1 β€œ On)⟢On
31 frn 6637 . . . . . . . 8 (rank:βˆͺ (𝑅1 β€œ On)⟢On β†’ ran rank βŠ† On)
3230, 31ax-mp 5 . . . . . . 7 ran rank βŠ† On
3329, 32sstri 3935 . . . . . 6 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) βŠ† On
34 hsmexlem4.u . . . . . . . . . 10 π‘ˆ = (π‘₯ ∈ V ↦ (rec((𝑦 ∈ V ↦ βˆͺ 𝑦), π‘₯) β†Ύ Ο‰))
3534ituni0 10224 . . . . . . . . 9 (𝑑 ∈ V β†’ ((π‘ˆβ€˜π‘‘)β€˜βˆ…) = 𝑑)
3635elv 3443 . . . . . . . 8 ((π‘ˆβ€˜π‘‘)β€˜βˆ…) = 𝑑
3736imaeq2i 5977 . . . . . . 7 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) = (rank β€œ 𝑑)
38 ffun 6633 . . . . . . . . . 10 (rank:βˆͺ (𝑅1 β€œ On)⟢On β†’ Fun rank)
3930, 38ax-mp 5 . . . . . . . . 9 Fun rank
40 vex 3441 . . . . . . . . 9 𝑑 ∈ V
41 wdomimag 9394 . . . . . . . . 9 ((Fun rank ∧ 𝑑 ∈ V) β†’ (rank β€œ 𝑑) β‰Ό* 𝑑)
4239, 40, 41mp2an 690 . . . . . . . 8 (rank β€œ 𝑑) β‰Ό* 𝑑
43 sneq 4575 . . . . . . . . . . . . 13 (π‘Ž = 𝑑 β†’ {π‘Ž} = {𝑑})
4443fveq2d 6808 . . . . . . . . . . . 12 (π‘Ž = 𝑑 β†’ (TCβ€˜{π‘Ž}) = (TCβ€˜{𝑑}))
4544raleqdv 3367 . . . . . . . . . . 11 (π‘Ž = 𝑑 β†’ (βˆ€π‘ ∈ (TCβ€˜{π‘Ž})𝑏 β‰Ό 𝑋 ↔ βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋))
46 hsmexlem4.s . . . . . . . . . . 11 𝑆 = {π‘Ž ∈ βˆͺ (𝑅1 β€œ On) ∣ βˆ€π‘ ∈ (TCβ€˜{π‘Ž})𝑏 β‰Ό 𝑋}
4745, 46elrab2 3632 . . . . . . . . . 10 (𝑑 ∈ 𝑆 ↔ (𝑑 ∈ βˆͺ (𝑅1 β€œ On) ∧ βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋))
4847simprbi 498 . . . . . . . . 9 (𝑑 ∈ 𝑆 β†’ βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋)
49 snex 5363 . . . . . . . . . . . 12 {𝑑} ∈ V
50 tcid 9545 . . . . . . . . . . . 12 ({𝑑} ∈ V β†’ {𝑑} βŠ† (TCβ€˜{𝑑}))
5149, 50ax-mp 5 . . . . . . . . . . 11 {𝑑} βŠ† (TCβ€˜{𝑑})
52 vsnid 4602 . . . . . . . . . . 11 𝑑 ∈ {𝑑}
5351, 52sselii 3923 . . . . . . . . . 10 𝑑 ∈ (TCβ€˜{𝑑})
54 breq1 5084 . . . . . . . . . . 11 (𝑏 = 𝑑 β†’ (𝑏 β‰Ό 𝑋 ↔ 𝑑 β‰Ό 𝑋))
5554rspcv 3562 . . . . . . . . . 10 (𝑑 ∈ (TCβ€˜{𝑑}) β†’ (βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋 β†’ 𝑑 β‰Ό 𝑋))
5653, 55ax-mp 5 . . . . . . . . 9 (βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋 β†’ 𝑑 β‰Ό 𝑋)
57 domwdom 9381 . . . . . . . . 9 (𝑑 β‰Ό 𝑋 β†’ 𝑑 β‰Ό* 𝑋)
5848, 56, 573syl 18 . . . . . . . 8 (𝑑 ∈ 𝑆 β†’ 𝑑 β‰Ό* 𝑋)
59 wdomtr 9382 . . . . . . . 8 (((rank β€œ 𝑑) β‰Ό* 𝑑 ∧ 𝑑 β‰Ό* 𝑋) β†’ (rank β€œ 𝑑) β‰Ό* 𝑋)
6042, 58, 59sylancr 588 . . . . . . 7 (𝑑 ∈ 𝑆 β†’ (rank β€œ 𝑑) β‰Ό* 𝑋)
6137, 60eqbrtrid 5116 . . . . . 6 (𝑑 ∈ 𝑆 β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)) β‰Ό* 𝑋)
62 eqid 2736 . . . . . . 7 OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…)))
6362hsmexlem1 10232 . . . . . 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 10229 . . . . 5 (π»β€˜βˆ…) = (harβ€˜π’« 𝑋)
6764, 66eleqtrrdi 2848 . . . 4 (𝑑 ∈ 𝑆 β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (π»β€˜βˆ…))
6867rgen 3064 . . 3 βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜βˆ…))) ∈ (π»β€˜βˆ…)
69 nfra1 3264 . . . . . 6 β„²π‘‘βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’)
70 nfv 1915 . . . . . 6 Ⅎ𝑑 𝑒 ∈ Ο‰
7169, 70nfan 1900 . . . . 5 Ⅎ𝑑(βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ 𝑒 ∈ Ο‰)
7234ituniiun 10228 . . . . . . . . . . . . 13 (𝑑 ∈ V β†’ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒) = βˆͺ 𝑓 ∈ 𝑑 ((π‘ˆβ€˜π‘“)β€˜π‘’))
7372elv 3443 . . . . . . . . . . . 12 ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒) = βˆͺ 𝑓 ∈ 𝑑 ((π‘ˆβ€˜π‘“)β€˜π‘’)
7473imaeq2i 5977 . . . . . . . . . . 11 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒)) = (rank β€œ βˆͺ 𝑓 ∈ 𝑑 ((π‘ˆβ€˜π‘“)β€˜π‘’))
75 imaiun 7150 . . . . . . . . . . 11 (rank β€œ βˆͺ 𝑓 ∈ 𝑑 ((π‘ˆβ€˜π‘“)β€˜π‘’)) = βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))
7674, 75eqtri 2764 . . . . . . . . . 10 (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒)) = βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))
77 oieq2 9320 . . . . . . . . . 10 ((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒)) = βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) = OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))))
7876, 77ax-mp 5 . . . . . . . . 9 OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) = OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
7978dmeqi 5826 . . . . . . . 8 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) = dom OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
8058ad2antll 727 . . . . . . . . 9 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ 𝑑 β‰Ό* 𝑋)
8165hsmexlem9 10231 . . . . . . . . . 10 (𝑒 ∈ Ο‰ β†’ (π»β€˜π‘’) ∈ On)
8281ad2antrl 726 . . . . . . . . 9 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ (π»β€˜π‘’) ∈ On)
83 fveq2 6804 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑓 β†’ (π‘ˆβ€˜π‘‘) = (π‘ˆβ€˜π‘“))
8483fveq1d 6806 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑓 β†’ ((π‘ˆβ€˜π‘‘)β€˜π‘’) = ((π‘ˆβ€˜π‘“)β€˜π‘’))
8584imaeq2d 5979 . . . . . . . . . . . . . . 15 (𝑑 = 𝑓 β†’ (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’)) = (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
86 oieq2 9320 . . . . . . . . . . . . . . 15 ((rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’)) = (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))))
8785, 86syl 17 . . . . . . . . . . . . . 14 (𝑑 = 𝑓 β†’ OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))))
8887dmeqd 5827 . . . . . . . . . . . . 13 (𝑑 = 𝑓 β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) = dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))))
8988eleq1d 2821 . . . . . . . . . . . 12 (𝑑 = 𝑓 β†’ (dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ↔ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (π»β€˜π‘’)))
90 simpll 765 . . . . . . . . . . . 12 (((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) β†’ βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’))
9146ssrab3 4021 . . . . . . . . . . . . . . . . . 18 𝑆 βŠ† βˆͺ (𝑅1 β€œ On)
9291sseli 3922 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ 𝑆 β†’ 𝑑 ∈ βˆͺ (𝑅1 β€œ On))
93 r1elssi 9611 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝑑 βŠ† βˆͺ (𝑅1 β€œ On))
9492, 93syl 17 . . . . . . . . . . . . . . . 16 (𝑑 ∈ 𝑆 β†’ 𝑑 βŠ† βˆͺ (𝑅1 β€œ On))
9594sselda 3926 . . . . . . . . . . . . . . 15 ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) β†’ 𝑓 ∈ βˆͺ (𝑅1 β€œ On))
96 snssi 4747 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ 𝑑 β†’ {𝑓} βŠ† 𝑑)
9740tcss 9550 . . . . . . . . . . . . . . . . . . 19 ({𝑓} βŠ† 𝑑 β†’ (TCβ€˜{𝑓}) βŠ† (TCβ€˜π‘‘))
9896, 97syl 17 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ 𝑑 β†’ (TCβ€˜{𝑓}) βŠ† (TCβ€˜π‘‘))
9949tcel 9551 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ {𝑑} β†’ (TCβ€˜π‘‘) βŠ† (TCβ€˜{𝑑}))
10052, 99mp1i 13 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ 𝑑 β†’ (TCβ€˜π‘‘) βŠ† (TCβ€˜{𝑑}))
10198, 100sstrd 3936 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ 𝑑 β†’ (TCβ€˜{𝑓}) βŠ† (TCβ€˜{𝑑}))
102 ssralv 3992 . . . . . . . . . . . . . . . . 17 ((TCβ€˜{𝑓}) βŠ† (TCβ€˜{𝑑}) β†’ (βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋 β†’ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋))
103101, 102syl 17 . . . . . . . . . . . . . . . 16 (𝑓 ∈ 𝑑 β†’ (βˆ€π‘ ∈ (TCβ€˜{𝑑})𝑏 β‰Ό 𝑋 β†’ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋))
10448, 103mpan9 508 . . . . . . . . . . . . . . 15 ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) β†’ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋)
105 sneq 4575 . . . . . . . . . . . . . . . . . 18 (π‘Ž = 𝑓 β†’ {π‘Ž} = {𝑓})
106105fveq2d 6808 . . . . . . . . . . . . . . . . 17 (π‘Ž = 𝑓 β†’ (TCβ€˜{π‘Ž}) = (TCβ€˜{𝑓}))
107106raleqdv 3367 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑓 β†’ (βˆ€π‘ ∈ (TCβ€˜{π‘Ž})𝑏 β‰Ό 𝑋 ↔ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋))
108107, 46elrab2 3632 . . . . . . . . . . . . . . 15 (𝑓 ∈ 𝑆 ↔ (𝑓 ∈ βˆͺ (𝑅1 β€œ On) ∧ βˆ€π‘ ∈ (TCβ€˜{𝑓})𝑏 β‰Ό 𝑋))
10995, 104, 108sylanbrc 584 . . . . . . . . . . . . . 14 ((𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑) β†’ 𝑓 ∈ 𝑆)
110109adantll 712 . . . . . . . . . . . . 13 (((𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆) ∧ 𝑓 ∈ 𝑑) β†’ 𝑓 ∈ 𝑆)
111110adantll 712 . . . . . . . . . . . 12 (((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) β†’ 𝑓 ∈ 𝑆)
11289, 90, 111rspcdva 3567 . . . . . . . . . . 11 (((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) ∧ 𝑓 ∈ 𝑑) β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (π»β€˜π‘’))
113 imassrn 5990 . . . . . . . . . . . . 13 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) βŠ† ran rank
114113, 32sstri 3935 . . . . . . . . . . . 12 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) βŠ† On
115 fvex 6817 . . . . . . . . . . . . . . 15 ((π‘ˆβ€˜π‘“)β€˜π‘’) ∈ V
116115funimaex 6551 . . . . . . . . . . . . . 14 (Fun rank β†’ (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ V)
11739, 116ax-mp 5 . . . . . . . . . . . . 13 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ V
118117elpw 4543 . . . . . . . . . . . 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 3140 . . . . . . . . 9 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ βˆ€π‘“ ∈ 𝑑 ((rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (π»β€˜π‘’)))
122 eqid 2736 . . . . . . . . . 10 OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) = OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
123 eqid 2736 . . . . . . . . . 10 OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) = OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)))
124122, 123hsmexlem3 10234 . . . . . . . . 9 (((𝑑 β‰Ό* 𝑋 ∧ (π»β€˜π‘’) ∈ On) ∧ βˆ€π‘“ ∈ 𝑑 ((rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (π»β€˜π‘’))) β†’ dom OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
12580, 82, 121, 124syl21anc 836 . . . . . . . 8 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ dom OrdIso( E , βˆͺ 𝑓 ∈ 𝑑 (rank β€œ ((π‘ˆβ€˜π‘“)β€˜π‘’))) ∈ (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
12679, 125eqeltrid 2841 . . . . . . 7 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜suc 𝑒))) ∈ (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
12765hsmexlem8 10230 . . . . . . . 8 (𝑒 ∈ Ο‰ β†’ (π»β€˜suc 𝑒) = (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
128127ad2antrl 726 . . . . . . 7 ((βˆ€π‘‘ ∈ 𝑆 dom OrdIso( E , (rank β€œ ((π‘ˆβ€˜π‘‘)β€˜π‘’))) ∈ (π»β€˜π‘’) ∧ (𝑒 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆)) β†’ (π»β€˜suc 𝑒) = (harβ€˜π’« (𝑋 Γ— (π»β€˜π‘’))))
129126, 128eleqtrrd 2840 . . . . . 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 3237 . . . 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 7780 . 2 (𝑐 ∈ Ο‰ β†’ βˆ€π‘‘ ∈ 𝑆 dom 𝑂 ∈ (π»β€˜π‘))
134133r19.21bi 3231 1 ((𝑐 ∈ Ο‰ ∧ 𝑑 ∈ 𝑆) β†’ dom 𝑂 ∈ (π»β€˜π‘))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1539   ∈ wcel 2104  βˆ€wral 3062  {crab 3303  Vcvv 3437   βŠ† wss 3892  βˆ…c0 4262  π’« cpw 4539  {csn 4565  βˆͺ cuni 4844  βˆͺ ciun 4931   class class class wbr 5081   ↦ cmpt 5164   E cep 5505   Γ— cxp 5598  dom cdm 5600  ran crn 5601   β†Ύ cres 5602   β€œ cima 5603  Oncon0 6281  suc csuc 6283  Fun wfun 6452  βŸΆwf 6454  β€˜cfv 6458  Ο‰com 7744  reccrdg 8271   β‰Ό cdom 8762  OrdIsocoi 9316  harchar 9363   β‰Ό* cwdom 9371  TCctc 9542  π‘…1cr1 9568  rankcrnk 9569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-inf2 9447
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3304  df-reu 3305  df-rab 3306  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-se 5556  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-isom 6467  df-riota 7264  df-ov 7310  df-om 7745  df-1st 7863  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-smo 8208  df-recs 8233  df-rdg 8272  df-en 8765  df-dom 8766  df-sdom 8767  df-oi 9317  df-har 9364  df-wdom 9372  df-tc 9543  df-r1 9570  df-rank 9571
This theorem is referenced by:  hsmexlem5  10236
  Copyright terms: Public domain W3C validator