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

Theorem cnfcom 9641
Description: Any ordinal ๐ต is equinumerous to the leading term of its Cantor normal form. Here we show that bijection explicitly. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.)
Hypotheses
Ref Expression
cnfcom.s ๐‘† = dom (ฯ‰ CNF ๐ด)
cnfcom.a (๐œ‘ โ†’ ๐ด โˆˆ On)
cnfcom.b (๐œ‘ โ†’ ๐ต โˆˆ (ฯ‰ โ†‘o ๐ด))
cnfcom.f ๐น = (โ—ก(ฯ‰ CNF ๐ด)โ€˜๐ต)
cnfcom.g ๐บ = OrdIso( E , (๐น supp โˆ…))
cnfcom.h ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (๐‘€ +o ๐‘ง)), โˆ…)
cnfcom.t ๐‘‡ = seqฯ‰((๐‘˜ โˆˆ V, ๐‘“ โˆˆ V โ†ฆ ๐พ), โˆ…)
cnfcom.m ๐‘€ = ((ฯ‰ โ†‘o (๐บโ€˜๐‘˜)) ยทo (๐นโ€˜(๐บโ€˜๐‘˜)))
cnfcom.k ๐พ = ((๐‘ฅ โˆˆ ๐‘€ โ†ฆ (dom ๐‘“ +o ๐‘ฅ)) โˆช โ—ก(๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ (๐‘€ +o ๐‘ฅ)))
cnfcom.1 (๐œ‘ โ†’ ๐ผ โˆˆ dom ๐บ)
Assertion
Ref Expression
cnfcom (๐œ‘ โ†’ (๐‘‡โ€˜suc ๐ผ):(๐ปโ€˜suc ๐ผ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐ผ)) ยทo (๐นโ€˜(๐บโ€˜๐ผ))))
Distinct variable groups:   ๐‘ฅ,๐‘˜,๐‘ง,๐ด   ๐‘˜,๐ผ,๐‘ฅ,๐‘ง   ๐‘ฅ,๐‘€   ๐‘“,๐‘˜,๐‘ฅ,๐‘ง,๐น   ๐‘ง,๐‘‡   ๐‘“,๐บ,๐‘˜,๐‘ฅ,๐‘ง   ๐‘“,๐ป,๐‘ฅ   ๐‘†,๐‘˜,๐‘ง
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘ง,๐‘“,๐‘˜)   ๐ด(๐‘“)   ๐ต(๐‘ฅ,๐‘ง,๐‘“,๐‘˜)   ๐‘†(๐‘ฅ,๐‘“)   ๐‘‡(๐‘ฅ,๐‘“,๐‘˜)   ๐ป(๐‘ง,๐‘˜)   ๐ผ(๐‘“)   ๐พ(๐‘ฅ,๐‘ง,๐‘“,๐‘˜)   ๐‘€(๐‘ง,๐‘“,๐‘˜)

Proof of Theorem cnfcom
Dummy variables ๐‘ค ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnfcom.1 . 2 (๐œ‘ โ†’ ๐ผ โˆˆ dom ๐บ)
2 cnfcom.s . . . . . 6 ๐‘† = dom (ฯ‰ CNF ๐ด)
3 omelon 9587 . . . . . . 7 ฯ‰ โˆˆ On
43a1i 11 . . . . . 6 (๐œ‘ โ†’ ฯ‰ โˆˆ On)
5 cnfcom.a . . . . . 6 (๐œ‘ โ†’ ๐ด โˆˆ On)
6 cnfcom.g . . . . . 6 ๐บ = OrdIso( E , (๐น supp โˆ…))
7 cnfcom.f . . . . . . 7 ๐น = (โ—ก(ฯ‰ CNF ๐ด)โ€˜๐ต)
82, 4, 5cantnff1o 9637 . . . . . . . . 9 (๐œ‘ โ†’ (ฯ‰ CNF ๐ด):๐‘†โ€“1-1-ontoโ†’(ฯ‰ โ†‘o ๐ด))
9 f1ocnv 6797 . . . . . . . . 9 ((ฯ‰ CNF ๐ด):๐‘†โ€“1-1-ontoโ†’(ฯ‰ โ†‘o ๐ด) โ†’ โ—ก(ฯ‰ CNF ๐ด):(ฯ‰ โ†‘o ๐ด)โ€“1-1-ontoโ†’๐‘†)
10 f1of 6785 . . . . . . . . 9 (โ—ก(ฯ‰ CNF ๐ด):(ฯ‰ โ†‘o ๐ด)โ€“1-1-ontoโ†’๐‘† โ†’ โ—ก(ฯ‰ CNF ๐ด):(ฯ‰ โ†‘o ๐ด)โŸถ๐‘†)
118, 9, 103syl 18 . . . . . . . 8 (๐œ‘ โ†’ โ—ก(ฯ‰ CNF ๐ด):(ฯ‰ โ†‘o ๐ด)โŸถ๐‘†)
12 cnfcom.b . . . . . . . 8 (๐œ‘ โ†’ ๐ต โˆˆ (ฯ‰ โ†‘o ๐ด))
1311, 12ffvelcdmd 7037 . . . . . . 7 (๐œ‘ โ†’ (โ—ก(ฯ‰ CNF ๐ด)โ€˜๐ต) โˆˆ ๐‘†)
147, 13eqeltrid 2838 . . . . . 6 (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
152, 4, 5, 6, 14cantnfcl 9608 . . . . 5 (๐œ‘ โ†’ ( E We (๐น supp โˆ…) โˆง dom ๐บ โˆˆ ฯ‰))
1615simprd 497 . . . 4 (๐œ‘ โ†’ dom ๐บ โˆˆ ฯ‰)
17 elnn 7814 . . . 4 ((๐ผ โˆˆ dom ๐บ โˆง dom ๐บ โˆˆ ฯ‰) โ†’ ๐ผ โˆˆ ฯ‰)
181, 16, 17syl2anc 585 . . 3 (๐œ‘ โ†’ ๐ผ โˆˆ ฯ‰)
19 eleq1 2822 . . . . . 6 (๐‘ค = ๐ผ โ†’ (๐‘ค โˆˆ dom ๐บ โ†” ๐ผ โˆˆ dom ๐บ))
20 suceq 6384 . . . . . . . 8 (๐‘ค = ๐ผ โ†’ suc ๐‘ค = suc ๐ผ)
2120fveq2d 6847 . . . . . . 7 (๐‘ค = ๐ผ โ†’ (๐‘‡โ€˜suc ๐‘ค) = (๐‘‡โ€˜suc ๐ผ))
2220fveq2d 6847 . . . . . . 7 (๐‘ค = ๐ผ โ†’ (๐ปโ€˜suc ๐‘ค) = (๐ปโ€˜suc ๐ผ))
23 fveq2 6843 . . . . . . . . 9 (๐‘ค = ๐ผ โ†’ (๐บโ€˜๐‘ค) = (๐บโ€˜๐ผ))
2423oveq2d 7374 . . . . . . . 8 (๐‘ค = ๐ผ โ†’ (ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) = (ฯ‰ โ†‘o (๐บโ€˜๐ผ)))
25 2fveq3 6848 . . . . . . . 8 (๐‘ค = ๐ผ โ†’ (๐นโ€˜(๐บโ€˜๐‘ค)) = (๐นโ€˜(๐บโ€˜๐ผ)))
2624, 25oveq12d 7376 . . . . . . 7 (๐‘ค = ๐ผ โ†’ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))) = ((ฯ‰ โ†‘o (๐บโ€˜๐ผ)) ยทo (๐นโ€˜(๐บโ€˜๐ผ))))
2721, 22, 26f1oeq123d 6779 . . . . . 6 (๐‘ค = ๐ผ โ†’ ((๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))) โ†” (๐‘‡โ€˜suc ๐ผ):(๐ปโ€˜suc ๐ผ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐ผ)) ยทo (๐นโ€˜(๐บโ€˜๐ผ)))))
2819, 27imbi12d 345 . . . . 5 (๐‘ค = ๐ผ โ†’ ((๐‘ค โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค)))) โ†” (๐ผ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐ผ):(๐ปโ€˜suc ๐ผ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐ผ)) ยทo (๐นโ€˜(๐บโ€˜๐ผ))))))
2928imbi2d 341 . . . 4 (๐‘ค = ๐ผ โ†’ ((๐œ‘ โ†’ (๐‘ค โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))))) โ†” (๐œ‘ โ†’ (๐ผ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐ผ):(๐ปโ€˜suc ๐ผ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐ผ)) ยทo (๐นโ€˜(๐บโ€˜๐ผ)))))))
30 eleq1 2822 . . . . . 6 (๐‘ค = โˆ… โ†’ (๐‘ค โˆˆ dom ๐บ โ†” โˆ… โˆˆ dom ๐บ))
31 suceq 6384 . . . . . . . 8 (๐‘ค = โˆ… โ†’ suc ๐‘ค = suc โˆ…)
3231fveq2d 6847 . . . . . . 7 (๐‘ค = โˆ… โ†’ (๐‘‡โ€˜suc ๐‘ค) = (๐‘‡โ€˜suc โˆ…))
3331fveq2d 6847 . . . . . . 7 (๐‘ค = โˆ… โ†’ (๐ปโ€˜suc ๐‘ค) = (๐ปโ€˜suc โˆ…))
34 fveq2 6843 . . . . . . . . 9 (๐‘ค = โˆ… โ†’ (๐บโ€˜๐‘ค) = (๐บโ€˜โˆ…))
3534oveq2d 7374 . . . . . . . 8 (๐‘ค = โˆ… โ†’ (ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) = (ฯ‰ โ†‘o (๐บโ€˜โˆ…)))
36 2fveq3 6848 . . . . . . . 8 (๐‘ค = โˆ… โ†’ (๐นโ€˜(๐บโ€˜๐‘ค)) = (๐นโ€˜(๐บโ€˜โˆ…)))
3735, 36oveq12d 7376 . . . . . . 7 (๐‘ค = โˆ… โ†’ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))) = ((ฯ‰ โ†‘o (๐บโ€˜โˆ…)) ยทo (๐นโ€˜(๐บโ€˜โˆ…))))
3832, 33, 37f1oeq123d 6779 . . . . . 6 (๐‘ค = โˆ… โ†’ ((๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))) โ†” (๐‘‡โ€˜suc โˆ…):(๐ปโ€˜suc โˆ…)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜โˆ…)) ยทo (๐นโ€˜(๐บโ€˜โˆ…)))))
3930, 38imbi12d 345 . . . . 5 (๐‘ค = โˆ… โ†’ ((๐‘ค โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค)))) โ†” (โˆ… โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc โˆ…):(๐ปโ€˜suc โˆ…)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜โˆ…)) ยทo (๐นโ€˜(๐บโ€˜โˆ…))))))
40 eleq1 2822 . . . . . 6 (๐‘ค = ๐‘ฆ โ†’ (๐‘ค โˆˆ dom ๐บ โ†” ๐‘ฆ โˆˆ dom ๐บ))
41 suceq 6384 . . . . . . . 8 (๐‘ค = ๐‘ฆ โ†’ suc ๐‘ค = suc ๐‘ฆ)
4241fveq2d 6847 . . . . . . 7 (๐‘ค = ๐‘ฆ โ†’ (๐‘‡โ€˜suc ๐‘ค) = (๐‘‡โ€˜suc ๐‘ฆ))
4341fveq2d 6847 . . . . . . 7 (๐‘ค = ๐‘ฆ โ†’ (๐ปโ€˜suc ๐‘ค) = (๐ปโ€˜suc ๐‘ฆ))
44 fveq2 6843 . . . . . . . . 9 (๐‘ค = ๐‘ฆ โ†’ (๐บโ€˜๐‘ค) = (๐บโ€˜๐‘ฆ))
4544oveq2d 7374 . . . . . . . 8 (๐‘ค = ๐‘ฆ โ†’ (ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) = (ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)))
46 2fveq3 6848 . . . . . . . 8 (๐‘ค = ๐‘ฆ โ†’ (๐นโ€˜(๐บโ€˜๐‘ค)) = (๐นโ€˜(๐บโ€˜๐‘ฆ)))
4745, 46oveq12d 7376 . . . . . . 7 (๐‘ค = ๐‘ฆ โ†’ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))) = ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))
4842, 43, 47f1oeq123d 6779 . . . . . 6 (๐‘ค = ๐‘ฆ โ†’ ((๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))) โ†” (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ)))))
4940, 48imbi12d 345 . . . . 5 (๐‘ค = ๐‘ฆ โ†’ ((๐‘ค โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค)))) โ†” (๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))))
50 eleq1 2822 . . . . . 6 (๐‘ค = suc ๐‘ฆ โ†’ (๐‘ค โˆˆ dom ๐บ โ†” suc ๐‘ฆ โˆˆ dom ๐บ))
51 suceq 6384 . . . . . . . 8 (๐‘ค = suc ๐‘ฆ โ†’ suc ๐‘ค = suc suc ๐‘ฆ)
5251fveq2d 6847 . . . . . . 7 (๐‘ค = suc ๐‘ฆ โ†’ (๐‘‡โ€˜suc ๐‘ค) = (๐‘‡โ€˜suc suc ๐‘ฆ))
5351fveq2d 6847 . . . . . . 7 (๐‘ค = suc ๐‘ฆ โ†’ (๐ปโ€˜suc ๐‘ค) = (๐ปโ€˜suc suc ๐‘ฆ))
54 fveq2 6843 . . . . . . . . 9 (๐‘ค = suc ๐‘ฆ โ†’ (๐บโ€˜๐‘ค) = (๐บโ€˜suc ๐‘ฆ))
5554oveq2d 7374 . . . . . . . 8 (๐‘ค = suc ๐‘ฆ โ†’ (ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) = (ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)))
56 2fveq3 6848 . . . . . . . 8 (๐‘ค = suc ๐‘ฆ โ†’ (๐นโ€˜(๐บโ€˜๐‘ค)) = (๐นโ€˜(๐บโ€˜suc ๐‘ฆ)))
5755, 56oveq12d 7376 . . . . . . 7 (๐‘ค = suc ๐‘ฆ โ†’ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))) = ((ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜suc ๐‘ฆ))))
5852, 53, 57f1oeq123d 6779 . . . . . 6 (๐‘ค = suc ๐‘ฆ โ†’ ((๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))) โ†” (๐‘‡โ€˜suc suc ๐‘ฆ):(๐ปโ€˜suc suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜suc ๐‘ฆ)))))
5950, 58imbi12d 345 . . . . 5 (๐‘ค = suc ๐‘ฆ โ†’ ((๐‘ค โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค)))) โ†” (suc ๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc suc ๐‘ฆ):(๐ปโ€˜suc suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜suc ๐‘ฆ))))))
605adantr 482 . . . . . . 7 ((๐œ‘ โˆง โˆ… โˆˆ dom ๐บ) โ†’ ๐ด โˆˆ On)
6112adantr 482 . . . . . . 7 ((๐œ‘ โˆง โˆ… โˆˆ dom ๐บ) โ†’ ๐ต โˆˆ (ฯ‰ โ†‘o ๐ด))
62 cnfcom.h . . . . . . 7 ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (๐‘€ +o ๐‘ง)), โˆ…)
63 cnfcom.t . . . . . . 7 ๐‘‡ = seqฯ‰((๐‘˜ โˆˆ V, ๐‘“ โˆˆ V โ†ฆ ๐พ), โˆ…)
64 cnfcom.m . . . . . . 7 ๐‘€ = ((ฯ‰ โ†‘o (๐บโ€˜๐‘˜)) ยทo (๐นโ€˜(๐บโ€˜๐‘˜)))
65 cnfcom.k . . . . . . 7 ๐พ = ((๐‘ฅ โˆˆ ๐‘€ โ†ฆ (dom ๐‘“ +o ๐‘ฅ)) โˆช โ—ก(๐‘ฅ โˆˆ dom ๐‘“ โ†ฆ (๐‘€ +o ๐‘ฅ)))
66 simpr 486 . . . . . . 7 ((๐œ‘ โˆง โˆ… โˆˆ dom ๐บ) โ†’ โˆ… โˆˆ dom ๐บ)
673a1i 11 . . . . . . . 8 ((๐œ‘ โˆง โˆ… โˆˆ dom ๐บ) โ†’ ฯ‰ โˆˆ On)
68 suppssdm 8109 . . . . . . . . . . 11 (๐น supp โˆ…) โŠ† dom ๐น
692, 4, 5cantnfs 9607 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐น โˆˆ ๐‘† โ†” (๐น:๐ดโŸถฯ‰ โˆง ๐น finSupp โˆ…)))
7014, 69mpbid 231 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐น:๐ดโŸถฯ‰ โˆง ๐น finSupp โˆ…))
7170simpld 496 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐น:๐ดโŸถฯ‰)
7268, 71fssdm 6689 . . . . . . . . . 10 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ๐ด)
73 onss 7720 . . . . . . . . . . 11 (๐ด โˆˆ On โ†’ ๐ด โŠ† On)
745, 73syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ด โŠ† On)
7572, 74sstrd 3955 . . . . . . . . 9 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† On)
766oif 9471 . . . . . . . . . 10 ๐บ:dom ๐บโŸถ(๐น supp โˆ…)
7776ffvelcdmi 7035 . . . . . . . . 9 (โˆ… โˆˆ dom ๐บ โ†’ (๐บโ€˜โˆ…) โˆˆ (๐น supp โˆ…))
78 ssel2 3940 . . . . . . . . 9 (((๐น supp โˆ…) โŠ† On โˆง (๐บโ€˜โˆ…) โˆˆ (๐น supp โˆ…)) โ†’ (๐บโ€˜โˆ…) โˆˆ On)
7975, 77, 78syl2an 597 . . . . . . . 8 ((๐œ‘ โˆง โˆ… โˆˆ dom ๐บ) โ†’ (๐บโ€˜โˆ…) โˆˆ On)
80 peano1 7826 . . . . . . . . 9 โˆ… โˆˆ ฯ‰
8180a1i 11 . . . . . . . 8 ((๐œ‘ โˆง โˆ… โˆˆ dom ๐บ) โ†’ โˆ… โˆˆ ฯ‰)
82 oen0 8534 . . . . . . . 8 (((ฯ‰ โˆˆ On โˆง (๐บโ€˜โˆ…) โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (๐บโ€˜โˆ…)))
8367, 79, 81, 82syl21anc 837 . . . . . . 7 ((๐œ‘ โˆง โˆ… โˆˆ dom ๐บ) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (๐บโ€˜โˆ…)))
84 0ex 5265 . . . . . . . . 9 โˆ… โˆˆ V
8563seqom0g 8403 . . . . . . . . 9 (โˆ… โˆˆ V โ†’ (๐‘‡โ€˜โˆ…) = โˆ…)
8684, 85ax-mp 5 . . . . . . . 8 (๐‘‡โ€˜โˆ…) = โˆ…
87 f1o0 6822 . . . . . . . . . 10 โˆ…:โˆ…โ€“1-1-ontoโ†’โˆ…
8862seqom0g 8403 . . . . . . . . . . 11 (โˆ… โˆˆ V โ†’ (๐ปโ€˜โˆ…) = โˆ…)
89 f1oeq2 6774 . . . . . . . . . . 11 ((๐ปโ€˜โˆ…) = โˆ… โ†’ (โˆ…:(๐ปโ€˜โˆ…)โ€“1-1-ontoโ†’โˆ… โ†” โˆ…:โˆ…โ€“1-1-ontoโ†’โˆ…))
9084, 88, 89mp2b 10 . . . . . . . . . 10 (โˆ…:(๐ปโ€˜โˆ…)โ€“1-1-ontoโ†’โˆ… โ†” โˆ…:โˆ…โ€“1-1-ontoโ†’โˆ…)
9187, 90mpbir 230 . . . . . . . . 9 โˆ…:(๐ปโ€˜โˆ…)โ€“1-1-ontoโ†’โˆ…
92 f1oeq1 6773 . . . . . . . . 9 ((๐‘‡โ€˜โˆ…) = โˆ… โ†’ ((๐‘‡โ€˜โˆ…):(๐ปโ€˜โˆ…)โ€“1-1-ontoโ†’โˆ… โ†” โˆ…:(๐ปโ€˜โˆ…)โ€“1-1-ontoโ†’โˆ…))
9391, 92mpbiri 258 . . . . . . . 8 ((๐‘‡โ€˜โˆ…) = โˆ… โ†’ (๐‘‡โ€˜โˆ…):(๐ปโ€˜โˆ…)โ€“1-1-ontoโ†’โˆ…)
9486, 93mp1i 13 . . . . . . 7 ((๐œ‘ โˆง โˆ… โˆˆ dom ๐บ) โ†’ (๐‘‡โ€˜โˆ…):(๐ปโ€˜โˆ…)โ€“1-1-ontoโ†’โˆ…)
952, 60, 61, 7, 6, 62, 63, 64, 65, 66, 83, 94cnfcomlem 9640 . . . . . 6 ((๐œ‘ โˆง โˆ… โˆˆ dom ๐บ) โ†’ (๐‘‡โ€˜suc โˆ…):(๐ปโ€˜suc โˆ…)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜โˆ…)) ยทo (๐นโ€˜(๐บโ€˜โˆ…))))
9695ex 414 . . . . 5 (๐œ‘ โ†’ (โˆ… โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc โˆ…):(๐ปโ€˜suc โˆ…)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜โˆ…)) ยทo (๐นโ€˜(๐บโ€˜โˆ…)))))
976oicl 9470 . . . . . . . . . 10 Ord dom ๐บ
98 ordtr 6332 . . . . . . . . . 10 (Ord dom ๐บ โ†’ Tr dom ๐บ)
9997, 98ax-mp 5 . . . . . . . . 9 Tr dom ๐บ
100 trsuc 6405 . . . . . . . . 9 ((Tr dom ๐บ โˆง suc ๐‘ฆ โˆˆ dom ๐บ) โ†’ ๐‘ฆ โˆˆ dom ๐บ)
10199, 100mpan 689 . . . . . . . 8 (suc ๐‘ฆ โˆˆ dom ๐บ โ†’ ๐‘ฆ โˆˆ dom ๐บ)
102101imim1i 63 . . . . . . 7 ((๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ)))) โ†’ (suc ๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ)))))
1035ad2antrr 725 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ๐ด โˆˆ On)
10412ad2antrr 725 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ๐ต โˆˆ (ฯ‰ โ†‘o ๐ด))
105 simprl 770 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ suc ๐‘ฆ โˆˆ dom ๐บ)
10674ad2antrr 725 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ๐ด โŠ† On)
10772ad2antrr 725 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐น supp โˆ…) โŠ† ๐ด)
10876ffvelcdmi 7035 . . . . . . . . . . . . . . . . 17 (suc ๐‘ฆ โˆˆ dom ๐บ โ†’ (๐บโ€˜suc ๐‘ฆ) โˆˆ (๐น supp โˆ…))
109108ad2antrl 727 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐บโ€˜suc ๐‘ฆ) โˆˆ (๐น supp โˆ…))
110107, 109sseldd 3946 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐บโ€˜suc ๐‘ฆ) โˆˆ ๐ด)
111106, 110sseldd 3946 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐บโ€˜suc ๐‘ฆ) โˆˆ On)
112 eloni 6328 . . . . . . . . . . . . . 14 ((๐บโ€˜suc ๐‘ฆ) โˆˆ On โ†’ Ord (๐บโ€˜suc ๐‘ฆ))
113111, 112syl 17 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ Ord (๐บโ€˜suc ๐‘ฆ))
114 vex 3448 . . . . . . . . . . . . . . 15 ๐‘ฆ โˆˆ V
115114sucid 6400 . . . . . . . . . . . . . 14 ๐‘ฆ โˆˆ suc ๐‘ฆ
116 ovexd 7393 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐น supp โˆ…) โˆˆ V)
11715simpld 496 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ E We (๐น supp โˆ…))
1186oiiso 9478 . . . . . . . . . . . . . . . . . 18 (((๐น supp โˆ…) โˆˆ V โˆง E We (๐น supp โˆ…)) โ†’ ๐บ Isom E , E (dom ๐บ, (๐น supp โˆ…)))
119116, 117, 118syl2anc 585 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐บ Isom E , E (dom ๐บ, (๐น supp โˆ…)))
120119ad2antrr 725 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ๐บ Isom E , E (dom ๐บ, (๐น supp โˆ…)))
121101ad2antrl 727 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ๐‘ฆ โˆˆ dom ๐บ)
122 isorel 7272 . . . . . . . . . . . . . . . 16 ((๐บ Isom E , E (dom ๐บ, (๐น supp โˆ…)) โˆง (๐‘ฆ โˆˆ dom ๐บ โˆง suc ๐‘ฆ โˆˆ dom ๐บ)) โ†’ (๐‘ฆ E suc ๐‘ฆ โ†” (๐บโ€˜๐‘ฆ) E (๐บโ€˜suc ๐‘ฆ)))
123120, 121, 105, 122syl12anc 836 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐‘ฆ E suc ๐‘ฆ โ†” (๐บโ€˜๐‘ฆ) E (๐บโ€˜suc ๐‘ฆ)))
124114sucex 7742 . . . . . . . . . . . . . . . 16 suc ๐‘ฆ โˆˆ V
125124epeli 5540 . . . . . . . . . . . . . . 15 (๐‘ฆ E suc ๐‘ฆ โ†” ๐‘ฆ โˆˆ suc ๐‘ฆ)
126 fvex 6856 . . . . . . . . . . . . . . . 16 (๐บโ€˜suc ๐‘ฆ) โˆˆ V
127126epeli 5540 . . . . . . . . . . . . . . 15 ((๐บโ€˜๐‘ฆ) E (๐บโ€˜suc ๐‘ฆ) โ†” (๐บโ€˜๐‘ฆ) โˆˆ (๐บโ€˜suc ๐‘ฆ))
128123, 125, 1273bitr3g 313 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐‘ฆ โˆˆ suc ๐‘ฆ โ†” (๐บโ€˜๐‘ฆ) โˆˆ (๐บโ€˜suc ๐‘ฆ)))
129115, 128mpbii 232 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐บโ€˜๐‘ฆ) โˆˆ (๐บโ€˜suc ๐‘ฆ))
130 ordsucss 7754 . . . . . . . . . . . . 13 (Ord (๐บโ€˜suc ๐‘ฆ) โ†’ ((๐บโ€˜๐‘ฆ) โˆˆ (๐บโ€˜suc ๐‘ฆ) โ†’ suc (๐บโ€˜๐‘ฆ) โŠ† (๐บโ€˜suc ๐‘ฆ)))
131113, 129, 130sylc 65 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ suc (๐บโ€˜๐‘ฆ) โŠ† (๐บโ€˜suc ๐‘ฆ))
13276ffvelcdmi 7035 . . . . . . . . . . . . . . . . 17 (๐‘ฆ โˆˆ dom ๐บ โ†’ (๐บโ€˜๐‘ฆ) โˆˆ (๐น supp โˆ…))
133121, 132syl 17 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐บโ€˜๐‘ฆ) โˆˆ (๐น supp โˆ…))
134107, 133sseldd 3946 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐บโ€˜๐‘ฆ) โˆˆ ๐ด)
135106, 134sseldd 3946 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐บโ€˜๐‘ฆ) โˆˆ On)
136 onsuc 7747 . . . . . . . . . . . . . 14 ((๐บโ€˜๐‘ฆ) โˆˆ On โ†’ suc (๐บโ€˜๐‘ฆ) โˆˆ On)
137135, 136syl 17 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ suc (๐บโ€˜๐‘ฆ) โˆˆ On)
1383a1i 11 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ฯ‰ โˆˆ On)
13980a1i 11 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ โˆ… โˆˆ ฯ‰)
140 oewordi 8539 . . . . . . . . . . . . 13 (((suc (๐บโ€˜๐‘ฆ) โˆˆ On โˆง (๐บโ€˜suc ๐‘ฆ) โˆˆ On โˆง ฯ‰ โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ (suc (๐บโ€˜๐‘ฆ) โŠ† (๐บโ€˜suc ๐‘ฆ) โ†’ (ฯ‰ โ†‘o suc (๐บโ€˜๐‘ฆ)) โŠ† (ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ))))
141137, 111, 138, 139, 140syl31anc 1374 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (suc (๐บโ€˜๐‘ฆ) โŠ† (๐บโ€˜suc ๐‘ฆ) โ†’ (ฯ‰ โ†‘o suc (๐บโ€˜๐‘ฆ)) โŠ† (ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ))))
142131, 141mpd 15 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (ฯ‰ โ†‘o suc (๐บโ€˜๐‘ฆ)) โŠ† (ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)))
14371ad2antrr 725 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ๐น:๐ดโŸถฯ‰)
144143, 134ffvelcdmd 7037 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐นโ€˜(๐บโ€˜๐‘ฆ)) โˆˆ ฯ‰)
145 nnon 7809 . . . . . . . . . . . . . . 15 ((๐นโ€˜(๐บโ€˜๐‘ฆ)) โˆˆ ฯ‰ โ†’ (๐นโ€˜(๐บโ€˜๐‘ฆ)) โˆˆ On)
146144, 145syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐นโ€˜(๐บโ€˜๐‘ฆ)) โˆˆ On)
147 oecl 8484 . . . . . . . . . . . . . . 15 ((ฯ‰ โˆˆ On โˆง (๐บโ€˜๐‘ฆ) โˆˆ On) โ†’ (ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) โˆˆ On)
148138, 135, 147syl2anc 585 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) โˆˆ On)
149 oen0 8534 . . . . . . . . . . . . . . 15 (((ฯ‰ โˆˆ On โˆง (๐บโ€˜๐‘ฆ) โˆˆ On) โˆง โˆ… โˆˆ ฯ‰) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)))
150138, 135, 139, 149syl21anc 837 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ โˆ… โˆˆ (ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)))
151 omord2 8515 . . . . . . . . . . . . . 14 ((((๐นโ€˜(๐บโ€˜๐‘ฆ)) โˆˆ On โˆง ฯ‰ โˆˆ On โˆง (ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) โˆˆ On) โˆง โˆ… โˆˆ (ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ))) โ†’ ((๐นโ€˜(๐บโ€˜๐‘ฆ)) โˆˆ ฯ‰ โ†” ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))) โˆˆ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo ฯ‰)))
152146, 138, 148, 150, 151syl31anc 1374 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ((๐นโ€˜(๐บโ€˜๐‘ฆ)) โˆˆ ฯ‰ โ†” ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))) โˆˆ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo ฯ‰)))
153144, 152mpbid 231 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))) โˆˆ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo ฯ‰))
154 oesuc 8474 . . . . . . . . . . . . 13 ((ฯ‰ โˆˆ On โˆง (๐บโ€˜๐‘ฆ) โˆˆ On) โ†’ (ฯ‰ โ†‘o suc (๐บโ€˜๐‘ฆ)) = ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo ฯ‰))
155138, 135, 154syl2anc 585 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (ฯ‰ โ†‘o suc (๐บโ€˜๐‘ฆ)) = ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo ฯ‰))
156153, 155eleqtrrd 2837 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))) โˆˆ (ฯ‰ โ†‘o suc (๐บโ€˜๐‘ฆ)))
157142, 156sseldd 3946 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ ((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))) โˆˆ (ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)))
158 simprr 772 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))
1592, 103, 104, 7, 6, 62, 63, 64, 65, 105, 157, 158cnfcomlem 9640 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โˆง (suc ๐‘ฆ โˆˆ dom ๐บ โˆง (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))))) โ†’ (๐‘‡โ€˜suc suc ๐‘ฆ):(๐ปโ€˜suc suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜suc ๐‘ฆ))))
160159exp32 422 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (suc ๐‘ฆ โˆˆ dom ๐บ โ†’ ((๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ))) โ†’ (๐‘‡โ€˜suc suc ๐‘ฆ):(๐ปโ€˜suc suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜suc ๐‘ฆ))))))
161160a2d 29 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((suc ๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ)))) โ†’ (suc ๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc suc ๐‘ฆ):(๐ปโ€˜suc suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜suc ๐‘ฆ))))))
162102, 161syl5 34 . . . . . 6 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ ((๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ)))) โ†’ (suc ๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc suc ๐‘ฆ):(๐ปโ€˜suc suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜suc ๐‘ฆ))))))
163162expcom 415 . . . . 5 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐œ‘ โ†’ ((๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ฆ):(๐ปโ€˜suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜๐‘ฆ)))) โ†’ (suc ๐‘ฆ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc suc ๐‘ฆ):(๐ปโ€˜suc suc ๐‘ฆ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜suc ๐‘ฆ)) ยทo (๐นโ€˜(๐บโ€˜suc ๐‘ฆ)))))))
16439, 49, 59, 96, 163finds2 7838 . . . 4 (๐‘ค โˆˆ ฯ‰ โ†’ (๐œ‘ โ†’ (๐‘ค โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐‘ค):(๐ปโ€˜suc ๐‘ค)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐‘ค)) ยทo (๐นโ€˜(๐บโ€˜๐‘ค))))))
16529, 164vtoclga 3533 . . 3 (๐ผ โˆˆ ฯ‰ โ†’ (๐œ‘ โ†’ (๐ผ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐ผ):(๐ปโ€˜suc ๐ผ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐ผ)) ยทo (๐นโ€˜(๐บโ€˜๐ผ))))))
16618, 165mpcom 38 . 2 (๐œ‘ โ†’ (๐ผ โˆˆ dom ๐บ โ†’ (๐‘‡โ€˜suc ๐ผ):(๐ปโ€˜suc ๐ผ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐ผ)) ยทo (๐นโ€˜(๐บโ€˜๐ผ)))))
1671, 166mpd 15 1 (๐œ‘ โ†’ (๐‘‡โ€˜suc ๐ผ):(๐ปโ€˜suc ๐ผ)โ€“1-1-ontoโ†’((ฯ‰ โ†‘o (๐บโ€˜๐ผ)) ยทo (๐นโ€˜(๐บโ€˜๐ผ))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107  Vcvv 3444   โˆช cun 3909   โŠ† wss 3911  โˆ…c0 4283   class class class wbr 5106   โ†ฆ cmpt 5189  Tr wtr 5223   E cep 5537   We wwe 5588  โ—กccnv 5633  dom cdm 5634  Ord word 6317  Oncon0 6318  suc csuc 6320  โŸถwf 6493  โ€“1-1-ontoโ†’wf1o 6496  โ€˜cfv 6497   Isom wiso 6498  (class class class)co 7358   โˆˆ cmpo 7360  ฯ‰com 7803   supp csupp 8093  seqฯ‰cseqom 8394   +o coa 8410   ยทo comu 8411   โ†‘o coe 8412   finSupp cfsupp 9308  OrdIsocoi 9450   CNF ccnf 9602
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 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582
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 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-seqom 8395  df-1o 8413  df-2o 8414  df-oadd 8417  df-omul 8418  df-oexp 8419  df-er 8651  df-map 8770  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-oi 9451  df-cnf 9603
This theorem is referenced by:  cnfcom2  9643
  Copyright terms: Public domain W3C validator