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

Theorem cantnf 9688
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 9672, 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 9677 . 2 (๐œ‘ โ†’ ๐‘‡ Or ๐‘†)
6 oecl 8537 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
72, 3, 6syl2anc 585 . . . 4 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
8 eloni 6375 . . . 4 ((๐ด โ†‘o ๐ต) โˆˆ On โ†’ Ord (๐ด โ†‘o ๐ต))
97, 8syl 17 . . 3 (๐œ‘ โ†’ Ord (๐ด โ†‘o ๐ต))
10 ordwe 6378 . . 3 (Ord (๐ด โ†‘o ๐ต) โ†’ E We (๐ด โ†‘o ๐ต))
11 weso 5668 . . 3 ( E We (๐ด โ†‘o ๐ต) โ†’ E Or (๐ด โ†‘o ๐ต))
12 sopo 5608 . . 3 ( E Or (๐ด โ†‘o ๐ต) โ†’ E Po (๐ด โ†‘o ๐ต))
139, 10, 11, 124syl 19 . 2 (๐œ‘ โ†’ E Po (๐ด โ†‘o ๐ต))
141, 2, 3cantnff 9669 . . 3 (๐œ‘ โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
1514frnd 6726 . . . 4 (๐œ‘ โ†’ ran (๐ด CNF ๐ต) โŠ† (๐ด โ†‘o ๐ต))
16 onss 7772 . . . . . . . 8 ((๐ด โ†‘o ๐ต) โˆˆ On โ†’ (๐ด โ†‘o ๐ต) โŠ† On)
177, 16syl 17 . . . . . . 7 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โŠ† On)
1817sseld 3982 . . . . . 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 3180 . . . . . . . . 9 (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐œ‘ โ†’ (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))) โ†” (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))))
24 ordelss 6381 . . . . . . . . . . . . . . . . . . 19 ((Ord (๐ด โ†‘o ๐ต) โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ๐‘ก โŠ† (๐ด โ†‘o ๐ต))
259, 24sylan 581 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ๐‘ก โŠ† (๐ด โ†‘o ๐ต))
2625sselda 3983 . . . . . . . . . . . . . . . . 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 3176 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†” โˆ€๐‘ฆ โˆˆ ๐‘ก ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))
30 dfss3 3971 . . . . . . . . . . . . . . 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 6390 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โ†‘o ๐ต) โˆˆ On โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ๐‘ก โˆˆ On)
4239, 40, 41syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐‘ก โˆˆ On)
43 on0eln0 6421 . . . . . . . . . . . . . . . . . . 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 9687 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))
51 fczsupp0 8178 . . . . . . . . . . . . . . . . . . . . 21 ((๐ต ร— {โˆ…}) supp โˆ…) = โˆ…
5251eqcomi 2742 . . . . . . . . . . . . . . . . . . . 20 โˆ… = ((๐ต ร— {โˆ…}) supp โˆ…)
53 oieq2 9508 . . . . . . . . . . . . . . . . . . . 20 (โˆ… = ((๐ต ร— {โˆ…}) supp โˆ…) โ†’ OrdIso( E , โˆ…) = OrdIso( E , ((๐ต ร— {โˆ…}) supp โˆ…)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . . . . 19 OrdIso( E , โˆ…) = OrdIso( E , ((๐ต ร— {โˆ…}) supp โˆ…))
55 ne0i 4335 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ (๐ด โ†‘o ๐ต) โ‰  โˆ…)
5655ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด โ†‘o ๐ต) โ‰  โˆ…)
57 oveq1 7416 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐ด = โˆ… โ†’ (๐ด โ†‘o ๐ต) = (โˆ… โ†‘o ๐ต))
5857neeq1d 3001 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ด = โˆ… โ†’ ((๐ด โ†‘o ๐ต) โ‰  โˆ… โ†” (โˆ… โ†‘o ๐ต) โ‰  โˆ…))
5956, 58syl5ibcom 244 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด = โˆ… โ†’ (โˆ… โ†‘o ๐ต) โ‰  โˆ…))
6059necon2d 2964 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((โˆ… โ†‘o ๐ต) = โˆ… โ†’ ๐ด โ‰  โˆ…))
61 on0eln0 6421 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†” ๐ต โ‰  โˆ…))
62 oe0m1 8521 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
6361, 62bitr3d 281 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ต โˆˆ On โ†’ (๐ต โ‰  โˆ… โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
6435, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต โ‰  โˆ… โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
65 on0eln0 6421 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ด โˆˆ On โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
6633, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
6760, 64, 663imtr4d 294 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต โ‰  โˆ… โ†’ โˆ… โˆˆ ๐ด))
68 ne0i 4335 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ ๐ต โ†’ ๐ต โ‰  โˆ…)
6967, 68impel 507 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ฆ โˆˆ ๐ต) โ†’ โˆ… โˆˆ ๐ด)
70 fconstmpt 5739 . . . . . . . . . . . . . . . . . . . . 21 (๐ต ร— {โˆ…}) = (๐‘ฆ โˆˆ ๐ต โ†ฆ โˆ…)
7169, 70fmptd 7114 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต ร— {โˆ…}):๐ตโŸถ๐ด)
72 0ex 5308 . . . . . . . . . . . . . . . . . . . . . . 23 โˆ… โˆˆ V
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ โˆ… โˆˆ V)
743, 73fczfsuppd 9381 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐ต ร— {โˆ…}) finSupp โˆ…)
7574adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต ร— {โˆ…}) finSupp โˆ…)
761, 2, 3cantnfs 9661 . . . . . . . . . . . . . . . . . . . . 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 9663 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((๐ด CNF ๐ต)โ€˜(๐ต ร— {โˆ…})) = (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom OrdIso( E , โˆ…)))
81 we0 5672 . . . . . . . . . . . . . . . . . . . . . 22 E We โˆ…
82 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso( E , โˆ…) = OrdIso( E , โˆ…)
8382oien 9533 . . . . . . . . . . . . . . . . . . . . . 22 ((โˆ… โˆˆ V โˆง E We โˆ…) โ†’ dom OrdIso( E , โˆ…) โ‰ˆ โˆ…)
8472, 81, 83mp2an 691 . . . . . . . . . . . . . . . . . . . . 21 dom OrdIso( E , โˆ…) โ‰ˆ โˆ…
85 en0 9013 . . . . . . . . . . . . . . . . . . . . 21 (dom OrdIso( E , โˆ…) โ‰ˆ โˆ… โ†” dom OrdIso( E , โˆ…) = โˆ…)
8684, 85mpbi 229 . . . . . . . . . . . . . . . . . . . 20 dom OrdIso( E , โˆ…) = โˆ…
8786fveq2i 6895 . . . . . . . . . . . . . . . . . . 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 8456 . . . . . . . . . . . . . . . . . . . 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 6719 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด CNF ๐ต) Fn ๐‘†)
94 fnfvelrn 7083 . . . . . . . . . . . . . . . . . 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 3028 . . . . . . . . . . . . . . 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 7846 . . . . . . 7 (๐‘ก โˆˆ On โ†’ (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))))
106105com3l 89 . . . . . 6 (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ (๐‘ก โˆˆ On โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))))
10718, 106mpdd 43 . . . . 5 (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)))
108107ssrdv 3989 . . . 4 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โŠ† ran (๐ด CNF ๐ต))
10915, 108eqssd 4000 . . 3 (๐œ‘ โ†’ ran (๐ด CNF ๐ต) = (๐ด โ†‘o ๐ต))
110 dffo2 6810 . . 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 6892 . . . . . . . . . . . 12 (๐‘ง = ๐‘ก โ†’ (๐‘ฅโ€˜๐‘ง) = (๐‘ฅโ€˜๐‘ก))
115 fveq2 6892 . . . . . . . . . . . 12 (๐‘ง = ๐‘ก โ†’ (๐‘ฆโ€˜๐‘ง) = (๐‘ฆโ€˜๐‘ก))
116114, 115eleq12d 2828 . . . . . . . . . . 11 (๐‘ง = ๐‘ก โ†’ ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โ†” (๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก)))
117 eleq1w 2817 . . . . . . . . . . . . 13 (๐‘ง = ๐‘ก โ†’ (๐‘ง โˆˆ ๐‘ค โ†” ๐‘ก โˆˆ ๐‘ค))
118117imbi1d 342 . . . . . . . . . . . 12 (๐‘ง = ๐‘ก โ†’ ((๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))))
119118ralbidv 3178 . . . . . . . . . . 11 (๐‘ง = ๐‘ก โ†’ (โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))))
120116, 119anbi12d 632 . . . . . . . . . 10 (๐‘ง = ๐‘ก โ†’ (((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))))
121120cbvrexvw 3236 . . . . . . . . 9 (โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))))
122 fveq1 6891 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ข โ†’ (๐‘ฅโ€˜๐‘ก) = (๐‘ขโ€˜๐‘ก))
123 fveq1 6891 . . . . . . . . . . . 12 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘ฆโ€˜๐‘ก) = (๐‘ฃโ€˜๐‘ก))
124 eleq12 2824 . . . . . . . . . . . 12 (((๐‘ฅโ€˜๐‘ก) = (๐‘ขโ€˜๐‘ก) โˆง (๐‘ฆโ€˜๐‘ก) = (๐‘ฃโ€˜๐‘ก)) โ†’ ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โ†” (๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก)))
125122, 123, 124syl2an 597 . . . . . . . . . . 11 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โ†” (๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก)))
126 fveq1 6891 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ข โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ขโ€˜๐‘ค))
127 fveq1 6891 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘ฆโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค))
128126, 127eqeqan12d 2747 . . . . . . . . . . . . 13 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ ((๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค) โ†” (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))
129128imbi2d 341 . . . . . . . . . . . 12 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ ((๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค))))
130129ralbidv 3178 . . . . . . . . . . 11 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค))))
131125, 130anbi12d 632 . . . . . . . . . 10 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))))
132131rexbidv 3179 . . . . . . . . 9 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))))
133121, 132bitrid 283 . . . . . . . 8 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))))
134133cbvopabv 5222 . . . . . . 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 9684 . . . . 5 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) โˆˆ ((๐ด CNF ๐ต)โ€˜๐‘”))
143 fvex 6905 . . . . . 6 ((๐ด CNF ๐ต)โ€˜๐‘”) โˆˆ V
144143epeli 5583 . . . . 5 (((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”) โ†” ((๐ด CNF ๐ต)โ€˜๐‘“) โˆˆ ((๐ด CNF ๐ต)โ€˜๐‘”))
145142, 144sylibr 233 . . . 4 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”))
146145expr 458 . . 3 ((๐œ‘ โˆง (๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†)) โ†’ (๐‘“๐‘‡๐‘” โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”)))
147146ralrimivva 3201 . 2 (๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐‘† โˆ€๐‘” โˆˆ ๐‘† (๐‘“๐‘‡๐‘” โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”)))
148 soisoi 7325 . 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 2941  โˆ€wral 3062  โˆƒwrex 3071  {crab 3433  Vcvv 3475   โŠ† wss 3949  โˆ…c0 4323  {csn 4629  โŸจcop 4635  โˆช cuni 4909  โˆฉ cint 4951   class class class wbr 5149  {copab 5211   E cep 5580   Po wpo 5587   Or wor 5588   We wwe 5631   ร— cxp 5675  dom cdm 5677  ran crn 5678  Ord word 6364  Oncon0 6365  โ„ฉcio 6494   Fn wfn 6539  โŸถwf 6540  โ€“ontoโ†’wfo 6542  โ€˜cfv 6544   Isom wiso 6545  (class class class)co 7409   โˆˆ cmpo 7411  1st c1st 7973  2nd c2nd 7974   supp csupp 8146  seqฯ‰cseqom 8447   +o coa 8463   ยทo comu 8464   โ†‘o coe 8465   โ‰ˆ cen 8936   finSupp cfsupp 9361  OrdIsocoi 9504   CNF ccnf 9656
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
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-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-supp 8147  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-seqom 8448  df-1o 8466  df-2o 8467  df-oadd 8470  df-omul 8471  df-oexp 8472  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9362  df-oi 9505  df-cnf 9657
This theorem is referenced by:  oemapwe  9689  cantnffval2  9690  cantnff1o  9691  cantnfresb  42122
  Copyright terms: Public domain W3C validator