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

Theorem cantnf 9637
Description: The Cantor Normal Form theorem. The function (๐ด CNF ๐ต), which maps a finitely supported function from ๐ต to ๐ด to the sum ((๐ด โ†‘o ๐‘“(๐‘Ž1)) โˆ˜ ๐‘Ž1) +o ((๐ด โ†‘o ๐‘“(๐‘Ž2)) โˆ˜ ๐‘Ž2) +o ... over all indices ๐‘Ž < ๐ต such that ๐‘“(๐‘Ž) is nonzero, is an order isomorphism from the ordering ๐‘‡ of finitely supported functions to the set (๐ด โ†‘o ๐ต) under the natural order. Setting ๐ด = ฯ‰ and letting ๐ต be arbitrarily large, the surjectivity of this function implies that every ordinal has a Cantor normal form (and injectivity, together with coherence cantnfres 9621, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.s ๐‘† = dom (๐ด CNF ๐ต)
cantnfs.a (๐œ‘ โ†’ ๐ด โˆˆ On)
cantnfs.b (๐œ‘ โ†’ ๐ต โˆˆ On)
oemapval.t ๐‘‡ = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))}
Assertion
Ref Expression
cantnf (๐œ‘ โ†’ (๐ด CNF ๐ต) Isom ๐‘‡, E (๐‘†, (๐ด โ†‘o ๐ต)))
Distinct variable groups:   ๐‘ฅ,๐‘ค,๐‘ฆ,๐‘ง,๐ต   ๐‘ค,๐ด,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘ฅ,๐‘†,๐‘ฆ,๐‘ง   ๐œ‘,๐‘ฅ,๐‘ฆ,๐‘ง
Allowed substitution hints:   ๐œ‘(๐‘ค)   ๐‘†(๐‘ค)   ๐‘‡(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)

Proof of Theorem cantnf
Dummy variables ๐‘“ ๐‘ ๐‘” ๐‘˜ ๐‘ก ๐‘ข ๐‘ฃ ๐‘Ž ๐‘ ๐‘‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfs.s . . 3 ๐‘† = dom (๐ด CNF ๐ต)
2 cantnfs.a . . 3 (๐œ‘ โ†’ ๐ด โˆˆ On)
3 cantnfs.b . . 3 (๐œ‘ โ†’ ๐ต โˆˆ On)
4 oemapval.t . . 3 ๐‘‡ = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))}
51, 2, 3, 4oemapso 9626 . 2 (๐œ‘ โ†’ ๐‘‡ Or ๐‘†)
6 oecl 8487 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
72, 3, 6syl2anc 585 . . . 4 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
8 eloni 6331 . . . 4 ((๐ด โ†‘o ๐ต) โˆˆ On โ†’ Ord (๐ด โ†‘o ๐ต))
97, 8syl 17 . . 3 (๐œ‘ โ†’ Ord (๐ด โ†‘o ๐ต))
10 ordwe 6334 . . 3 (Ord (๐ด โ†‘o ๐ต) โ†’ E We (๐ด โ†‘o ๐ต))
11 weso 5628 . . 3 ( E We (๐ด โ†‘o ๐ต) โ†’ E Or (๐ด โ†‘o ๐ต))
12 sopo 5568 . . 3 ( E Or (๐ด โ†‘o ๐ต) โ†’ E Po (๐ด โ†‘o ๐ต))
139, 10, 11, 124syl 19 . 2 (๐œ‘ โ†’ E Po (๐ด โ†‘o ๐ต))
141, 2, 3cantnff 9618 . . 3 (๐œ‘ โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
1514frnd 6680 . . . 4 (๐œ‘ โ†’ ran (๐ด CNF ๐ต) โŠ† (๐ด โ†‘o ๐ต))
16 onss 7723 . . . . . . . 8 ((๐ด โ†‘o ๐ต) โˆˆ On โ†’ (๐ด โ†‘o ๐ต) โŠ† On)
177, 16syl 17 . . . . . . 7 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โŠ† On)
1817sseld 3947 . . . . . 6 (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ On))
19 eleq1w 2817 . . . . . . . . . 10 (๐‘ก = ๐‘ฆ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†” ๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต)))
20 eleq1w 2817 . . . . . . . . . 10 (๐‘ก = ๐‘ฆ โ†’ (๐‘ก โˆˆ ran (๐ด CNF ๐ต) โ†” ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))
2119, 20imbi12d 345 . . . . . . . . 9 (๐‘ก = ๐‘ฆ โ†’ ((๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)) โ†” (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))))
2221imbi2d 341 . . . . . . . 8 (๐‘ก = ๐‘ฆ โ†’ ((๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))) โ†” (๐œ‘ โ†’ (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))))
23 r19.21v 3173 . . . . . . . . 9 (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐œ‘ โ†’ (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))) โ†” (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))))
24 ordelss 6337 . . . . . . . . . . . . . . . . . . 19 ((Ord (๐ด โ†‘o ๐ต) โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ๐‘ก โŠ† (๐ด โ†‘o ๐ต))
259, 24sylan 581 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ๐‘ก โŠ† (๐ด โ†‘o ๐ต))
2625sselda 3948 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โˆง ๐‘ฆ โˆˆ ๐‘ก) โ†’ ๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต))
27 pm5.5 362 . . . . . . . . . . . . . . . . 17 (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ((๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†” ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))
2826, 27syl 17 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โˆง ๐‘ฆ โˆˆ ๐‘ก) โ†’ ((๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†” ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))
2928ralbidva 3169 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†” โˆ€๐‘ฆ โˆˆ ๐‘ก ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))
30 dfss3 3936 . . . . . . . . . . . . . . 15 (๐‘ก โŠ† ran (๐ด CNF ๐ต) โ†” โˆ€๐‘ฆ โˆˆ ๐‘ก ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))
3129, 30bitr4di 289 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†” ๐‘ก โŠ† ran (๐ด CNF ๐ต)))
32 eleq1 2822 . . . . . . . . . . . . . . . 16 (๐‘ก = โˆ… โ†’ (๐‘ก โˆˆ ran (๐ด CNF ๐ต) โ†” โˆ… โˆˆ ran (๐ด CNF ๐ต)))
332adantr 482 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐ด โˆˆ On)
3433adantr 482 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐ด โˆˆ On)
353adantr 482 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐ต โˆˆ On)
3635adantr 482 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐ต โˆˆ On)
37 simplrl 776 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐‘ก โˆˆ (๐ด โ†‘o ๐ต))
38 simplrr 777 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐‘ก โŠ† ran (๐ด CNF ๐ต))
397adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
40 simprl 770 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐‘ก โˆˆ (๐ด โ†‘o ๐ต))
41 onelon 6346 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โ†‘o ๐ต) โˆˆ On โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ๐‘ก โˆˆ On)
4239, 40, 41syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐‘ก โˆˆ On)
43 on0eln0 6377 . . . . . . . . . . . . . . . . . . 19 (๐‘ก โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ก โ†” ๐‘ก โ‰  โˆ…))
4442, 43syl 17 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (โˆ… โˆˆ ๐‘ก โ†” ๐‘ก โ‰  โˆ…))
4544biimpar 479 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ โˆ… โˆˆ ๐‘ก)
46 eqid 2733 . . . . . . . . . . . . . . . . 17 โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)} = โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}
47 eqid 2733 . . . . . . . . . . . . . . . . 17 (โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก)) = (โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก))
48 eqid 2733 . . . . . . . . . . . . . . . . 17 (1st โ€˜(โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก))) = (1st โ€˜(โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก)))
49 eqid 2733 . . . . . . . . . . . . . . . . 17 (2nd โ€˜(โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก))) = (2nd โ€˜(โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก)))
501, 34, 36, 4, 37, 38, 45, 46, 47, 48, 49cantnflem4 9636 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))
51 fczsupp0 8128 . . . . . . . . . . . . . . . . . . . . 21 ((๐ต ร— {โˆ…}) supp โˆ…) = โˆ…
5251eqcomi 2742 . . . . . . . . . . . . . . . . . . . 20 โˆ… = ((๐ต ร— {โˆ…}) supp โˆ…)
53 oieq2 9457 . . . . . . . . . . . . . . . . . . . 20 (โˆ… = ((๐ต ร— {โˆ…}) supp โˆ…) โ†’ OrdIso( E , โˆ…) = OrdIso( E , ((๐ต ร— {โˆ…}) supp โˆ…)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . . . . 19 OrdIso( E , โˆ…) = OrdIso( E , ((๐ต ร— {โˆ…}) supp โˆ…))
55 ne0i 4298 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ (๐ด โ†‘o ๐ต) โ‰  โˆ…)
5655ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด โ†‘o ๐ต) โ‰  โˆ…)
57 oveq1 7368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐ด = โˆ… โ†’ (๐ด โ†‘o ๐ต) = (โˆ… โ†‘o ๐ต))
5857neeq1d 3000 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ด = โˆ… โ†’ ((๐ด โ†‘o ๐ต) โ‰  โˆ… โ†” (โˆ… โ†‘o ๐ต) โ‰  โˆ…))
5956, 58syl5ibcom 244 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด = โˆ… โ†’ (โˆ… โ†‘o ๐ต) โ‰  โˆ…))
6059necon2d 2963 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((โˆ… โ†‘o ๐ต) = โˆ… โ†’ ๐ด โ‰  โˆ…))
61 on0eln0 6377 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†” ๐ต โ‰  โˆ…))
62 oe0m1 8471 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
6361, 62bitr3d 281 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ต โˆˆ On โ†’ (๐ต โ‰  โˆ… โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
6435, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต โ‰  โˆ… โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
65 on0eln0 6377 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ด โˆˆ On โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
6633, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
6760, 64, 663imtr4d 294 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต โ‰  โˆ… โ†’ โˆ… โˆˆ ๐ด))
68 ne0i 4298 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ ๐ต โ†’ ๐ต โ‰  โˆ…)
6967, 68impel 507 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ฆ โˆˆ ๐ต) โ†’ โˆ… โˆˆ ๐ด)
70 fconstmpt 5698 . . . . . . . . . . . . . . . . . . . . 21 (๐ต ร— {โˆ…}) = (๐‘ฆ โˆˆ ๐ต โ†ฆ โˆ…)
7169, 70fmptd 7066 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต ร— {โˆ…}):๐ตโŸถ๐ด)
72 0ex 5268 . . . . . . . . . . . . . . . . . . . . . . 23 โˆ… โˆˆ V
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ โˆ… โˆˆ V)
743, 73fczfsuppd 9331 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐ต ร— {โˆ…}) finSupp โˆ…)
7574adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต ร— {โˆ…}) finSupp โˆ…)
761, 2, 3cantnfs 9610 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((๐ต ร— {โˆ…}) โˆˆ ๐‘† โ†” ((๐ต ร— {โˆ…}):๐ตโŸถ๐ด โˆง (๐ต ร— {โˆ…}) finSupp โˆ…)))
7776adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((๐ต ร— {โˆ…}) โˆˆ ๐‘† โ†” ((๐ต ร— {โˆ…}):๐ตโŸถ๐ด โˆง (๐ต ร— {โˆ…}) finSupp โˆ…)))
7871, 75, 77mpbir2and 712 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต ร— {โˆ…}) โˆˆ ๐‘†)
79 eqid 2733 . . . . . . . . . . . . . . . . . . 19 seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…) = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
801, 33, 35, 54, 78, 79cantnfval 9612 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((๐ด CNF ๐ต)โ€˜(๐ต ร— {โˆ…})) = (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom OrdIso( E , โˆ…)))
81 we0 5632 . . . . . . . . . . . . . . . . . . . . . 22 E We โˆ…
82 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso( E , โˆ…) = OrdIso( E , โˆ…)
8382oien 9482 . . . . . . . . . . . . . . . . . . . . . 22 ((โˆ… โˆˆ V โˆง E We โˆ…) โ†’ dom OrdIso( E , โˆ…) โ‰ˆ โˆ…)
8472, 81, 83mp2an 691 . . . . . . . . . . . . . . . . . . . . 21 dom OrdIso( E , โˆ…) โ‰ˆ โˆ…
85 en0 8963 . . . . . . . . . . . . . . . . . . . . 21 (dom OrdIso( E , โˆ…) โ‰ˆ โˆ… โ†” dom OrdIso( E , โˆ…) = โˆ…)
8684, 85mpbi 229 . . . . . . . . . . . . . . . . . . . 20 dom OrdIso( E , โˆ…) = โˆ…
8786fveq2i 6849 . . . . . . . . . . . . . . . . . . 19 (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom OrdIso( E , โˆ…)) = (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜โˆ…)
8879seqom0g 8406 . . . . . . . . . . . . . . . . . . . 20 (โˆ… โˆˆ V โ†’ (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜โˆ…) = โˆ…)
8972, 88ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜โˆ…) = โˆ…
9087, 89eqtri 2761 . . . . . . . . . . . . . . . . . 18 (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom OrdIso( E , โˆ…)) = โˆ…
9180, 90eqtrdi 2789 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((๐ด CNF ๐ต)โ€˜(๐ต ร— {โˆ…})) = โˆ…)
9214adantr 482 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
9392ffnd 6673 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด CNF ๐ต) Fn ๐‘†)
94 fnfvelrn 7035 . . . . . . . . . . . . . . . . . 18 (((๐ด CNF ๐ต) Fn ๐‘† โˆง (๐ต ร— {โˆ…}) โˆˆ ๐‘†) โ†’ ((๐ด CNF ๐ต)โ€˜(๐ต ร— {โˆ…})) โˆˆ ran (๐ด CNF ๐ต))
9593, 78, 94syl2anc 585 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((๐ด CNF ๐ต)โ€˜(๐ต ร— {โˆ…})) โˆˆ ran (๐ด CNF ๐ต))
9691, 95eqeltrrd 2835 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ โˆ… โˆˆ ran (๐ด CNF ๐ต))
9732, 50, 96pm2.61ne 3027 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))
9897expr 458 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (๐‘ก โŠ† ran (๐ด CNF ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)))
9931, 98sylbid 239 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)))
10099ex 414 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))))
101100com23 86 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))))
102101a2i 14 . . . . . . . . . 10 ((๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))) โ†’ (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))))
103102a1i 11 . . . . . . . . 9 (๐‘ก โˆˆ On โ†’ ((๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))) โ†’ (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)))))
10423, 103biimtrid 241 . . . . . . . 8 (๐‘ก โˆˆ On โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐œ‘ โ†’ (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))) โ†’ (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)))))
10522, 104tfis2 7797 . . . . . . 7 (๐‘ก โˆˆ On โ†’ (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))))
106105com3l 89 . . . . . 6 (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ (๐‘ก โˆˆ On โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))))
10718, 106mpdd 43 . . . . 5 (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)))
108107ssrdv 3954 . . . 4 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โŠ† ran (๐ด CNF ๐ต))
10915, 108eqssd 3965 . . 3 (๐œ‘ โ†’ ran (๐ด CNF ๐ต) = (๐ด โ†‘o ๐ต))
110 dffo2 6764 . . 3 ((๐ด CNF ๐ต):๐‘†โ€“ontoโ†’(๐ด โ†‘o ๐ต) โ†” ((๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต) โˆง ran (๐ด CNF ๐ต) = (๐ด โ†‘o ๐ต)))
11114, 109, 110sylanbrc 584 . 2 (๐œ‘ โ†’ (๐ด CNF ๐ต):๐‘†โ€“ontoโ†’(๐ด โ†‘o ๐ต))
1122adantr 482 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐ด โˆˆ On)
1133adantr 482 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐ต โˆˆ On)
114 fveq2 6846 . . . . . . . . . . . 12 (๐‘ง = ๐‘ก โ†’ (๐‘ฅโ€˜๐‘ง) = (๐‘ฅโ€˜๐‘ก))
115 fveq2 6846 . . . . . . . . . . . 12 (๐‘ง = ๐‘ก โ†’ (๐‘ฆโ€˜๐‘ง) = (๐‘ฆโ€˜๐‘ก))
116114, 115eleq12d 2828 . . . . . . . . . . 11 (๐‘ง = ๐‘ก โ†’ ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โ†” (๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก)))
117 eleq1w 2817 . . . . . . . . . . . . 13 (๐‘ง = ๐‘ก โ†’ (๐‘ง โˆˆ ๐‘ค โ†” ๐‘ก โˆˆ ๐‘ค))
118117imbi1d 342 . . . . . . . . . . . 12 (๐‘ง = ๐‘ก โ†’ ((๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))))
119118ralbidv 3171 . . . . . . . . . . 11 (๐‘ง = ๐‘ก โ†’ (โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))))
120116, 119anbi12d 632 . . . . . . . . . 10 (๐‘ง = ๐‘ก โ†’ (((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))))
121120cbvrexvw 3225 . . . . . . . . 9 (โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))))
122 fveq1 6845 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ข โ†’ (๐‘ฅโ€˜๐‘ก) = (๐‘ขโ€˜๐‘ก))
123 fveq1 6845 . . . . . . . . . . . 12 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘ฆโ€˜๐‘ก) = (๐‘ฃโ€˜๐‘ก))
124 eleq12 2824 . . . . . . . . . . . 12 (((๐‘ฅโ€˜๐‘ก) = (๐‘ขโ€˜๐‘ก) โˆง (๐‘ฆโ€˜๐‘ก) = (๐‘ฃโ€˜๐‘ก)) โ†’ ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โ†” (๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก)))
125122, 123, 124syl2an 597 . . . . . . . . . . 11 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โ†” (๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก)))
126 fveq1 6845 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ข โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ขโ€˜๐‘ค))
127 fveq1 6845 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘ฆโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค))
128126, 127eqeqan12d 2747 . . . . . . . . . . . . 13 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ ((๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค) โ†” (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))
129128imbi2d 341 . . . . . . . . . . . 12 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ ((๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค))))
130129ralbidv 3171 . . . . . . . . . . 11 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค))))
131125, 130anbi12d 632 . . . . . . . . . 10 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))))
132131rexbidv 3172 . . . . . . . . 9 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))))
133121, 132bitrid 283 . . . . . . . 8 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))))
134133cbvopabv 5182 . . . . . . 7 {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))} = {โŸจ๐‘ข, ๐‘ฃโŸฉ โˆฃ โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))}
1354, 134eqtri 2761 . . . . . 6 ๐‘‡ = {โŸจ๐‘ข, ๐‘ฃโŸฉ โˆฃ โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))}
136 simprll 778 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐‘“ โˆˆ ๐‘†)
137 simprlr 779 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐‘” โˆˆ ๐‘†)
138 simprr 772 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐‘“๐‘‡๐‘”)
139 eqid 2733 . . . . . 6 โˆช {๐‘ โˆˆ ๐ต โˆฃ (๐‘“โ€˜๐‘) โˆˆ (๐‘”โ€˜๐‘)} = โˆช {๐‘ โˆˆ ๐ต โˆฃ (๐‘“โ€˜๐‘) โˆˆ (๐‘”โ€˜๐‘)}
140 eqid 2733 . . . . . 6 OrdIso( E , (๐‘” supp โˆ…)) = OrdIso( E , (๐‘” supp โˆ…))
141 eqid 2733 . . . . . 6 seqฯ‰((๐‘˜ โˆˆ V, ๐‘ก โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , (๐‘” supp โˆ…))โ€˜๐‘˜)) ยทo (๐‘”โ€˜(OrdIso( E , (๐‘” supp โˆ…))โ€˜๐‘˜))) +o ๐‘ก)), โˆ…) = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ก โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , (๐‘” supp โˆ…))โ€˜๐‘˜)) ยทo (๐‘”โ€˜(OrdIso( E , (๐‘” supp โˆ…))โ€˜๐‘˜))) +o ๐‘ก)), โˆ…)
1421, 112, 113, 135, 136, 137, 138, 139, 140, 141cantnflem1 9633 . . . . 5 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) โˆˆ ((๐ด CNF ๐ต)โ€˜๐‘”))
143 fvex 6859 . . . . . 6 ((๐ด CNF ๐ต)โ€˜๐‘”) โˆˆ V
144143epeli 5543 . . . . 5 (((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”) โ†” ((๐ด CNF ๐ต)โ€˜๐‘“) โˆˆ ((๐ด CNF ๐ต)โ€˜๐‘”))
145142, 144sylibr 233 . . . 4 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”))
146145expr 458 . . 3 ((๐œ‘ โˆง (๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†)) โ†’ (๐‘“๐‘‡๐‘” โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”)))
147146ralrimivva 3194 . 2 (๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐‘† โˆ€๐‘” โˆˆ ๐‘† (๐‘“๐‘‡๐‘” โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”)))
148 soisoi 7277 . 2 (((๐‘‡ Or ๐‘† โˆง E Po (๐ด โ†‘o ๐ต)) โˆง ((๐ด CNF ๐ต):๐‘†โ€“ontoโ†’(๐ด โ†‘o ๐ต) โˆง โˆ€๐‘“ โˆˆ ๐‘† โˆ€๐‘” โˆˆ ๐‘† (๐‘“๐‘‡๐‘” โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”)))) โ†’ (๐ด CNF ๐ต) Isom ๐‘‡, E (๐‘†, (๐ด โ†‘o ๐ต)))
1495, 13, 111, 147, 148syl22anc 838 1 (๐œ‘ โ†’ (๐ด CNF ๐ต) Isom ๐‘‡, E (๐‘†, (๐ด โ†‘o ๐ต)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070  {crab 3406  Vcvv 3447   โŠ† wss 3914  โˆ…c0 4286  {csn 4590  โŸจcop 4596  โˆช cuni 4869  โˆฉ cint 4911   class class class wbr 5109  {copab 5171   E cep 5540   Po wpo 5547   Or wor 5548   We wwe 5591   ร— cxp 5635  dom cdm 5637  ran crn 5638  Ord word 6320  Oncon0 6321  โ„ฉcio 6450   Fn wfn 6495  โŸถwf 6496  โ€“ontoโ†’wfo 6498  โ€˜cfv 6500   Isom wiso 6501  (class class class)co 7361   โˆˆ cmpo 7363  1st c1st 7923  2nd c2nd 7924   supp csupp 8096  seqฯ‰cseqom 8397   +o coa 8413   ยทo comu 8414   โ†‘o coe 8415   โ‰ˆ cen 8886   finSupp cfsupp 9311  OrdIsocoi 9453   CNF ccnf 9605
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 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
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 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-supp 8097  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-seqom 8398  df-1o 8416  df-2o 8417  df-oadd 8420  df-omul 8421  df-oexp 8422  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fsupp 9312  df-oi 9454  df-cnf 9606
This theorem is referenced by:  oemapwe  9638  cantnffval2  9639  cantnff1o  9640  cantnfresb  41706
  Copyright terms: Public domain W3C validator