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

Theorem cantnf 9687
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 9671, 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 9676 . 2 (๐œ‘ โ†’ ๐‘‡ Or ๐‘†)
6 oecl 8536 . . . . 5 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
72, 3, 6syl2anc 584 . . . 4 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
8 eloni 6374 . . . 4 ((๐ด โ†‘o ๐ต) โˆˆ On โ†’ Ord (๐ด โ†‘o ๐ต))
97, 8syl 17 . . 3 (๐œ‘ โ†’ Ord (๐ด โ†‘o ๐ต))
10 ordwe 6377 . . 3 (Ord (๐ด โ†‘o ๐ต) โ†’ E We (๐ด โ†‘o ๐ต))
11 weso 5667 . . 3 ( E We (๐ด โ†‘o ๐ต) โ†’ E Or (๐ด โ†‘o ๐ต))
12 sopo 5607 . . 3 ( E Or (๐ด โ†‘o ๐ต) โ†’ E Po (๐ด โ†‘o ๐ต))
139, 10, 11, 124syl 19 . 2 (๐œ‘ โ†’ E Po (๐ด โ†‘o ๐ต))
141, 2, 3cantnff 9668 . . 3 (๐œ‘ โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
1514frnd 6725 . . . 4 (๐œ‘ โ†’ ran (๐ด CNF ๐ต) โŠ† (๐ด โ†‘o ๐ต))
16 onss 7771 . . . . . . . 8 ((๐ด โ†‘o ๐ต) โˆˆ On โ†’ (๐ด โ†‘o ๐ต) โŠ† On)
177, 16syl 17 . . . . . . 7 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โŠ† On)
1817sseld 3981 . . . . . 6 (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ On))
19 eleq1w 2816 . . . . . . . . . 10 (๐‘ก = ๐‘ฆ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†” ๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต)))
20 eleq1w 2816 . . . . . . . . . 10 (๐‘ก = ๐‘ฆ โ†’ (๐‘ก โˆˆ ran (๐ด CNF ๐ต) โ†” ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))
2119, 20imbi12d 344 . . . . . . . . 9 (๐‘ก = ๐‘ฆ โ†’ ((๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)) โ†” (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))))
2221imbi2d 340 . . . . . . . 8 (๐‘ก = ๐‘ฆ โ†’ ((๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))) โ†” (๐œ‘ โ†’ (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))))
23 r19.21v 3179 . . . . . . . . 9 (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐œ‘ โ†’ (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))) โ†” (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))))
24 ordelss 6380 . . . . . . . . . . . . . . . . . . 19 ((Ord (๐ด โ†‘o ๐ต) โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ๐‘ก โŠ† (๐ด โ†‘o ๐ต))
259, 24sylan 580 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ๐‘ก โŠ† (๐ด โ†‘o ๐ต))
2625sselda 3982 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โˆง ๐‘ฆ โˆˆ ๐‘ก) โ†’ ๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต))
27 pm5.5 361 . . . . . . . . . . . . . . . . 17 (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ((๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†” ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))
2826, 27syl 17 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โˆง ๐‘ฆ โˆˆ ๐‘ก) โ†’ ((๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†” ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))
2928ralbidva 3175 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†” โˆ€๐‘ฆ โˆˆ ๐‘ก ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)))
30 dfss3 3970 . . . . . . . . . . . . . . 15 (๐‘ก โŠ† ran (๐ด CNF ๐ต) โ†” โˆ€๐‘ฆ โˆˆ ๐‘ก ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต))
3129, 30bitr4di 288 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†” ๐‘ก โŠ† ran (๐ด CNF ๐ต)))
32 eleq1 2821 . . . . . . . . . . . . . . . 16 (๐‘ก = โˆ… โ†’ (๐‘ก โˆˆ ran (๐ด CNF ๐ต) โ†” โˆ… โˆˆ ran (๐ด CNF ๐ต)))
332adantr 481 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐ด โˆˆ On)
3433adantr 481 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐ด โˆˆ On)
353adantr 481 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐ต โˆˆ On)
3635adantr 481 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐ต โˆˆ On)
37 simplrl 775 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐‘ก โˆˆ (๐ด โ†‘o ๐ต))
38 simplrr 776 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐‘ก โŠ† ran (๐ด CNF ๐ต))
397adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
40 simprl 769 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐‘ก โˆˆ (๐ด โ†‘o ๐ต))
41 onelon 6389 . . . . . . . . . . . . . . . . . . . 20 (((๐ด โ†‘o ๐ต) โˆˆ On โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ๐‘ก โˆˆ On)
4239, 40, 41syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐‘ก โˆˆ On)
43 on0eln0 6420 . . . . . . . . . . . . . . . . . . 19 (๐‘ก โˆˆ On โ†’ (โˆ… โˆˆ ๐‘ก โ†” ๐‘ก โ‰  โˆ…))
4442, 43syl 17 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (โˆ… โˆˆ ๐‘ก โ†” ๐‘ก โ‰  โˆ…))
4544biimpar 478 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ โˆ… โˆˆ ๐‘ก)
46 eqid 2732 . . . . . . . . . . . . . . . . 17 โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)} = โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}
47 eqid 2732 . . . . . . . . . . . . . . . . 17 (โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก)) = (โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก))
48 eqid 2732 . . . . . . . . . . . . . . . . 17 (1st โ€˜(โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก))) = (1st โ€˜(โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)})(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐‘ก โˆˆ (๐ด โ†‘o ๐‘)}) ยทo ๐‘Ž) +o ๐‘) = ๐‘ก)))
49 eqid 2732 . . . . . . . . . . . . . . . . 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 9686 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ก โ‰  โˆ…) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))
51 fczsupp0 8177 . . . . . . . . . . . . . . . . . . . . 21 ((๐ต ร— {โˆ…}) supp โˆ…) = โˆ…
5251eqcomi 2741 . . . . . . . . . . . . . . . . . . . 20 โˆ… = ((๐ต ร— {โˆ…}) supp โˆ…)
53 oieq2 9507 . . . . . . . . . . . . . . . . . . . 20 (โˆ… = ((๐ต ร— {โˆ…}) supp โˆ…) โ†’ OrdIso( E , โˆ…) = OrdIso( E , ((๐ต ร— {โˆ…}) supp โˆ…)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . . . . 19 OrdIso( E , โˆ…) = OrdIso( E , ((๐ต ร— {โˆ…}) supp โˆ…))
55 ne0i 4334 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ (๐ด โ†‘o ๐ต) โ‰  โˆ…)
5655ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด โ†‘o ๐ต) โ‰  โˆ…)
57 oveq1 7415 . . . . . . . . . . . . . . . . . . . . . . . . . 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 6420 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†” ๐ต โ‰  โˆ…))
62 oe0m1 8520 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐ต โˆˆ On โ†’ (โˆ… โˆˆ ๐ต โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
6361, 62bitr3d 280 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ต โˆˆ On โ†’ (๐ต โ‰  โˆ… โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
6435, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต โ‰  โˆ… โ†” (โˆ… โ†‘o ๐ต) = โˆ…))
65 on0eln0 6420 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐ด โˆˆ On โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
6633, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
6760, 64, 663imtr4d 293 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต โ‰  โˆ… โ†’ โˆ… โˆˆ ๐ด))
68 ne0i 4334 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ ๐ต โ†’ ๐ต โ‰  โˆ…)
6967, 68impel 506 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โˆง ๐‘ฆ โˆˆ ๐ต) โ†’ โˆ… โˆˆ ๐ด)
70 fconstmpt 5738 . . . . . . . . . . . . . . . . . . . . 21 (๐ต ร— {โˆ…}) = (๐‘ฆ โˆˆ ๐ต โ†ฆ โˆ…)
7169, 70fmptd 7113 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต ร— {โˆ…}):๐ตโŸถ๐ด)
72 0ex 5307 . . . . . . . . . . . . . . . . . . . . . . 23 โˆ… โˆˆ V
7372a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ โˆ… โˆˆ V)
743, 73fczfsuppd 9380 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐ต ร— {โˆ…}) finSupp โˆ…)
7574adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต ร— {โˆ…}) finSupp โˆ…)
761, 2, 3cantnfs 9660 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((๐ต ร— {โˆ…}) โˆˆ ๐‘† โ†” ((๐ต ร— {โˆ…}):๐ตโŸถ๐ด โˆง (๐ต ร— {โˆ…}) finSupp โˆ…)))
7776adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((๐ต ร— {โˆ…}) โˆˆ ๐‘† โ†” ((๐ต ร— {โˆ…}):๐ตโŸถ๐ด โˆง (๐ต ร— {โˆ…}) finSupp โˆ…)))
7871, 75, 77mpbir2and 711 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ต ร— {โˆ…}) โˆˆ ๐‘†)
79 eqid 2732 . . . . . . . . . . . . . . . . . . 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 9662 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((๐ด CNF ๐ต)โ€˜(๐ต ร— {โˆ…})) = (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom OrdIso( E , โˆ…)))
81 we0 5671 . . . . . . . . . . . . . . . . . . . . . 22 E We โˆ…
82 eqid 2732 . . . . . . . . . . . . . . . . . . . . . . 23 OrdIso( E , โˆ…) = OrdIso( E , โˆ…)
8382oien 9532 . . . . . . . . . . . . . . . . . . . . . 22 ((โˆ… โˆˆ V โˆง E We โˆ…) โ†’ dom OrdIso( E , โˆ…) โ‰ˆ โˆ…)
8472, 81, 83mp2an 690 . . . . . . . . . . . . . . . . . . . . 21 dom OrdIso( E , โˆ…) โ‰ˆ โˆ…
85 en0 9012 . . . . . . . . . . . . . . . . . . . . 21 (dom OrdIso( E , โˆ…) โ‰ˆ โˆ… โ†” dom OrdIso( E , โˆ…) = โˆ…)
8684, 85mpbi 229 . . . . . . . . . . . . . . . . . . . 20 dom OrdIso( E , โˆ…) = โˆ…
8786fveq2i 6894 . . . . . . . . . . . . . . . . . . 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 8455 . . . . . . . . . . . . . . . . . . . 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 2760 . . . . . . . . . . . . . . . . . 18 (seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , โˆ…)โ€˜๐‘˜)) ยทo ((๐ต ร— {โˆ…})โ€˜(OrdIso( E , โˆ…)โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)โ€˜dom OrdIso( E , โˆ…)) = โˆ…
9180, 90eqtrdi 2788 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((๐ด CNF ๐ต)โ€˜(๐ต ร— {โˆ…})) = โˆ…)
9214adantr 481 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
9392ffnd 6718 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ (๐ด CNF ๐ต) Fn ๐‘†)
94 fnfvelrn 7082 . . . . . . . . . . . . . . . . . 18 (((๐ด CNF ๐ต) Fn ๐‘† โˆง (๐ต ร— {โˆ…}) โˆˆ ๐‘†) โ†’ ((๐ด CNF ๐ต)โ€˜(๐ต ร— {โˆ…})) โˆˆ ran (๐ด CNF ๐ต))
9593, 78, 94syl2anc 584 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ((๐ด CNF ๐ต)โ€˜(๐ต ร— {โˆ…})) โˆˆ ran (๐ด CNF ๐ต))
9691, 95eqeltrrd 2834 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ โˆ… โˆˆ ran (๐ด CNF ๐ต))
9732, 50, 96pm2.61ne 3027 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โˆง ๐‘ก โŠ† ran (๐ด CNF ๐ต))) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))
9897expr 457 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (๐‘ก โŠ† ran (๐ด CNF ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)))
9931, 98sylbid 239 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ก โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (โˆ€๐‘ฆ โˆˆ ๐‘ก (๐‘ฆ โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ฆ โˆˆ ran (๐ด CNF ๐ต)) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)))
10099ex 413 . . . . . . . . . . . 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 7845 . . . . . . 7 (๐‘ก โˆˆ On โ†’ (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))))
106105com3l 89 . . . . . 6 (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ (๐‘ก โˆˆ On โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต))))
10718, 106mpdd 43 . . . . 5 (๐œ‘ โ†’ (๐‘ก โˆˆ (๐ด โ†‘o ๐ต) โ†’ ๐‘ก โˆˆ ran (๐ด CNF ๐ต)))
108107ssrdv 3988 . . . 4 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โŠ† ran (๐ด CNF ๐ต))
10915, 108eqssd 3999 . . 3 (๐œ‘ โ†’ ran (๐ด CNF ๐ต) = (๐ด โ†‘o ๐ต))
110 dffo2 6809 . . 3 ((๐ด CNF ๐ต):๐‘†โ€“ontoโ†’(๐ด โ†‘o ๐ต) โ†” ((๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต) โˆง ran (๐ด CNF ๐ต) = (๐ด โ†‘o ๐ต)))
11114, 109, 110sylanbrc 583 . 2 (๐œ‘ โ†’ (๐ด CNF ๐ต):๐‘†โ€“ontoโ†’(๐ด โ†‘o ๐ต))
1122adantr 481 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐ด โˆˆ On)
1133adantr 481 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐ต โˆˆ On)
114 fveq2 6891 . . . . . . . . . . . 12 (๐‘ง = ๐‘ก โ†’ (๐‘ฅโ€˜๐‘ง) = (๐‘ฅโ€˜๐‘ก))
115 fveq2 6891 . . . . . . . . . . . 12 (๐‘ง = ๐‘ก โ†’ (๐‘ฆโ€˜๐‘ง) = (๐‘ฆโ€˜๐‘ก))
116114, 115eleq12d 2827 . . . . . . . . . . 11 (๐‘ง = ๐‘ก โ†’ ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โ†” (๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก)))
117 eleq1w 2816 . . . . . . . . . . . . 13 (๐‘ง = ๐‘ก โ†’ (๐‘ง โˆˆ ๐‘ค โ†” ๐‘ก โˆˆ ๐‘ค))
118117imbi1d 341 . . . . . . . . . . . 12 (๐‘ง = ๐‘ก โ†’ ((๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))))
119118ralbidv 3177 . . . . . . . . . . 11 (๐‘ง = ๐‘ก โ†’ (โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))))
120116, 119anbi12d 631 . . . . . . . . . 10 (๐‘ง = ๐‘ก โ†’ (((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))))
121120cbvrexvw 3235 . . . . . . . . 9 (โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))))
122 fveq1 6890 . . . . . . . . . . . 12 (๐‘ฅ = ๐‘ข โ†’ (๐‘ฅโ€˜๐‘ก) = (๐‘ขโ€˜๐‘ก))
123 fveq1 6890 . . . . . . . . . . . 12 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘ฆโ€˜๐‘ก) = (๐‘ฃโ€˜๐‘ก))
124 eleq12 2823 . . . . . . . . . . . 12 (((๐‘ฅโ€˜๐‘ก) = (๐‘ขโ€˜๐‘ก) โˆง (๐‘ฆโ€˜๐‘ก) = (๐‘ฃโ€˜๐‘ก)) โ†’ ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โ†” (๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก)))
125122, 123, 124syl2an 596 . . . . . . . . . . 11 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โ†” (๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก)))
126 fveq1 6890 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ข โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ขโ€˜๐‘ค))
127 fveq1 6890 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘ฆโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค))
128126, 127eqeqan12d 2746 . . . . . . . . . . . . 13 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ ((๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค) โ†” (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))
129128imbi2d 340 . . . . . . . . . . . 12 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ ((๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค))))
130129ralbidv 3177 . . . . . . . . . . 11 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)) โ†” โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค))))
131125, 130anbi12d 631 . . . . . . . . . 10 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))))
132131rexbidv 3178 . . . . . . . . 9 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ก) โˆˆ (๐‘ฆโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))))
133121, 132bitrid 282 . . . . . . . 8 ((๐‘ฅ = ๐‘ข โˆง ๐‘ฆ = ๐‘ฃ) โ†’ (โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค))) โ†” โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))))
134133cbvopabv 5221 . . . . . . 7 {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))} = {โŸจ๐‘ข, ๐‘ฃโŸฉ โˆฃ โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))}
1354, 134eqtri 2760 . . . . . 6 ๐‘‡ = {โŸจ๐‘ข, ๐‘ฃโŸฉ โˆฃ โˆƒ๐‘ก โˆˆ ๐ต ((๐‘ขโ€˜๐‘ก) โˆˆ (๐‘ฃโ€˜๐‘ก) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ก โˆˆ ๐‘ค โ†’ (๐‘ขโ€˜๐‘ค) = (๐‘ฃโ€˜๐‘ค)))}
136 simprll 777 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐‘“ โˆˆ ๐‘†)
137 simprlr 778 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐‘” โˆˆ ๐‘†)
138 simprr 771 . . . . . 6 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ๐‘“๐‘‡๐‘”)
139 eqid 2732 . . . . . 6 โˆช {๐‘ โˆˆ ๐ต โˆฃ (๐‘“โ€˜๐‘) โˆˆ (๐‘”โ€˜๐‘)} = โˆช {๐‘ โˆˆ ๐ต โˆฃ (๐‘“โ€˜๐‘) โˆˆ (๐‘”โ€˜๐‘)}
140 eqid 2732 . . . . . 6 OrdIso( E , (๐‘” supp โˆ…)) = OrdIso( E , (๐‘” supp โˆ…))
141 eqid 2732 . . . . . 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 9683 . . . . 5 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) โˆˆ ((๐ด CNF ๐ต)โ€˜๐‘”))
143 fvex 6904 . . . . . 6 ((๐ด CNF ๐ต)โ€˜๐‘”) โˆˆ V
144143epeli 5582 . . . . 5 (((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”) โ†” ((๐ด CNF ๐ต)โ€˜๐‘“) โˆˆ ((๐ด CNF ๐ต)โ€˜๐‘”))
145142, 144sylibr 233 . . . 4 ((๐œ‘ โˆง ((๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†) โˆง ๐‘“๐‘‡๐‘”)) โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”))
146145expr 457 . . 3 ((๐œ‘ โˆง (๐‘“ โˆˆ ๐‘† โˆง ๐‘” โˆˆ ๐‘†)) โ†’ (๐‘“๐‘‡๐‘” โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”)))
147146ralrimivva 3200 . 2 (๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐‘† โˆ€๐‘” โˆˆ ๐‘† (๐‘“๐‘‡๐‘” โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”)))
148 soisoi 7324 . 2 (((๐‘‡ Or ๐‘† โˆง E Po (๐ด โ†‘o ๐ต)) โˆง ((๐ด CNF ๐ต):๐‘†โ€“ontoโ†’(๐ด โ†‘o ๐ต) โˆง โˆ€๐‘“ โˆˆ ๐‘† โˆ€๐‘” โˆˆ ๐‘† (๐‘“๐‘‡๐‘” โ†’ ((๐ด CNF ๐ต)โ€˜๐‘“) E ((๐ด CNF ๐ต)โ€˜๐‘”)))) โ†’ (๐ด CNF ๐ต) Isom ๐‘‡, E (๐‘†, (๐ด โ†‘o ๐ต)))
1495, 13, 111, 147, 148syl22anc 837 1 (๐œ‘ โ†’ (๐ด CNF ๐ต) Isom ๐‘‡, E (๐‘†, (๐ด โ†‘o ๐ต)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070  {crab 3432  Vcvv 3474   โŠ† wss 3948  โˆ…c0 4322  {csn 4628  โŸจcop 4634  โˆช cuni 4908  โˆฉ cint 4950   class class class wbr 5148  {copab 5210   E cep 5579   Po wpo 5586   Or wor 5587   We wwe 5630   ร— cxp 5674  dom cdm 5676  ran crn 5677  Ord word 6363  Oncon0 6364  โ„ฉcio 6493   Fn wfn 6538  โŸถwf 6539  โ€“ontoโ†’wfo 6541  โ€˜cfv 6543   Isom wiso 6544  (class class class)co 7408   โˆˆ cmpo 7410  1st c1st 7972  2nd c2nd 7973   supp csupp 8145  seqฯ‰cseqom 8446   +o coa 8462   ยทo comu 8463   โ†‘o coe 8464   โ‰ˆ cen 8935   finSupp cfsupp 9360  OrdIsocoi 9503   CNF ccnf 9655
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-supp 8146  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-seqom 8447  df-1o 8465  df-2o 8466  df-oadd 8469  df-omul 8470  df-oexp 8471  df-er 8702  df-map 8821  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-oi 9504  df-cnf 9656
This theorem is referenced by:  oemapwe  9688  cantnffval2  9689  cantnff1o  9690  cantnfresb  42064
  Copyright terms: Public domain W3C validator