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

Theorem cantnflem3 9634
Description: Lemma for cantnf 9636. Here we show existence of Cantor normal forms. Assuming (by transfinite induction) that every number less than ๐ถ has a normal form, we can use oeeu 8555 to factor ๐ถ into the form ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘ where 0 < ๐‘Œ < ๐ด and ๐‘ < (๐ด โ†‘o ๐‘‹) (and a fortiori ๐‘‹ < ๐ต). Then since ๐‘ < (๐ด โ†‘o ๐‘‹) โ‰ค (๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ โ‰ค ๐ถ, ๐‘ has a normal form, and by appending the term (๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ using cantnfp1 9624 we get a normal form for ๐ถ. (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.s ๐‘† = dom (๐ด CNF ๐ต)
cantnfs.a (๐œ‘ โ†’ ๐ด โˆˆ On)
cantnfs.b (๐œ‘ โ†’ ๐ต โˆˆ On)
oemapval.t ๐‘‡ = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))}
cantnf.c (๐œ‘ โ†’ ๐ถ โˆˆ (๐ด โ†‘o ๐ต))
cantnf.s (๐œ‘ โ†’ ๐ถ โŠ† ran (๐ด CNF ๐ต))
cantnf.e (๐œ‘ โ†’ โˆ… โˆˆ ๐ถ)
cantnf.x ๐‘‹ = โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐ถ โˆˆ (๐ด โ†‘o ๐‘)}
cantnf.p ๐‘ƒ = (โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Ž) +o ๐‘) = ๐ถ))
cantnf.y ๐‘Œ = (1st โ€˜๐‘ƒ)
cantnf.z ๐‘ = (2nd โ€˜๐‘ƒ)
cantnf.g (๐œ‘ โ†’ ๐บ โˆˆ ๐‘†)
cantnf.v (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = ๐‘)
cantnf.f ๐น = (๐‘ก โˆˆ ๐ต โ†ฆ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)))
Assertion
Ref Expression
cantnflem3 (๐œ‘ โ†’ ๐ถ โˆˆ ran (๐ด CNF ๐ต))
Distinct variable groups:   ๐‘ก,๐‘,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง,๐ต   ๐‘Ž,๐‘,๐‘,๐‘‘,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง,๐ถ   ๐‘ก,๐‘Ž,๐ด,๐‘,๐‘,๐‘‘,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘‡,๐‘,๐‘ก   ๐‘ค,๐น,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘†,๐‘,๐‘ก,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘ก,๐‘,๐‘ฅ,๐‘ฆ,๐‘ง   ๐บ,๐‘,๐‘ก,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง   ๐œ‘,๐‘ก,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘ก,๐‘Œ,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘‹,๐‘Ž,๐‘,๐‘‘,๐‘ก,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง
Allowed substitution hints:   ๐œ‘(๐‘ค,๐‘Ž,๐‘,๐‘,๐‘‘)   ๐ต(๐‘Ž,๐‘,๐‘‘)   ๐ถ(๐‘ก)   ๐‘ƒ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘ก,๐‘Ž,๐‘,๐‘,๐‘‘)   ๐‘†(๐‘ค,๐‘Ž,๐‘,๐‘‘)   ๐‘‡(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘Ž,๐‘,๐‘‘)   ๐น(๐‘ก,๐‘Ž,๐‘,๐‘,๐‘‘)   ๐บ(๐‘Ž,๐‘,๐‘‘)   ๐‘‹(๐‘)   ๐‘Œ(๐‘Ž,๐‘,๐‘,๐‘‘)   ๐‘(๐‘ค,๐‘Ž,๐‘,๐‘,๐‘‘)

Proof of Theorem cantnflem3
Dummy variable ๐‘˜ is distinct from all other variables.
StepHypRef Expression
1 cantnfs.s . . . . 5 ๐‘† = dom (๐ด CNF ๐ต)
2 cantnfs.a . . . . 5 (๐œ‘ โ†’ ๐ด โˆˆ On)
3 cantnfs.b . . . . 5 (๐œ‘ โ†’ ๐ต โˆˆ On)
4 cantnf.g . . . . 5 (๐œ‘ โ†’ ๐บ โˆˆ ๐‘†)
5 oemapval.t . . . . . . . . . . . . . 14 ๐‘‡ = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))}
6 cantnf.c . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ถ โˆˆ (๐ด โ†‘o ๐ต))
7 cantnf.s . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ถ โŠ† ran (๐ด CNF ๐ต))
8 cantnf.e . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ… โˆˆ ๐ถ)
91, 2, 3, 5, 6, 7, 8cantnflem2 9633 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ด โˆˆ (On โˆ– 2o) โˆง ๐ถ โˆˆ (On โˆ– 1o)))
10 eqid 2737 . . . . . . . . . . . . . . 15 ๐‘‹ = ๐‘‹
11 eqid 2737 . . . . . . . . . . . . . . 15 ๐‘Œ = ๐‘Œ
12 eqid 2737 . . . . . . . . . . . . . . 15 ๐‘ = ๐‘
1310, 11, 123pm3.2i 1340 . . . . . . . . . . . . . 14 (๐‘‹ = ๐‘‹ โˆง ๐‘Œ = ๐‘Œ โˆง ๐‘ = ๐‘)
14 cantnf.x . . . . . . . . . . . . . . 15 ๐‘‹ = โˆช โˆฉ {๐‘ โˆˆ On โˆฃ ๐ถ โˆˆ (๐ด โ†‘o ๐‘)}
15 cantnf.p . . . . . . . . . . . . . . 15 ๐‘ƒ = (โ„ฉ๐‘‘โˆƒ๐‘Ž โˆˆ On โˆƒ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)(๐‘‘ = โŸจ๐‘Ž, ๐‘โŸฉ โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Ž) +o ๐‘) = ๐ถ))
16 cantnf.y . . . . . . . . . . . . . . 15 ๐‘Œ = (1st โ€˜๐‘ƒ)
17 cantnf.z . . . . . . . . . . . . . . 15 ๐‘ = (2nd โ€˜๐‘ƒ)
1814, 15, 16, 17oeeui 8554 . . . . . . . . . . . . . 14 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ถ โˆˆ (On โˆ– 1o)) โ†’ (((๐‘‹ โˆˆ On โˆง ๐‘Œ โˆˆ (๐ด โˆ– 1o) โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘) = ๐ถ) โ†” (๐‘‹ = ๐‘‹ โˆง ๐‘Œ = ๐‘Œ โˆง ๐‘ = ๐‘)))
1913, 18mpbiri 258 . . . . . . . . . . . . 13 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ถ โˆˆ (On โˆ– 1o)) โ†’ ((๐‘‹ โˆˆ On โˆง ๐‘Œ โˆˆ (๐ด โˆ– 1o) โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘) = ๐ถ))
209, 19syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘‹ โˆˆ On โˆง ๐‘Œ โˆˆ (๐ด โˆ– 1o) โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘) = ๐ถ))
2120simpld 496 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‹ โˆˆ On โˆง ๐‘Œ โˆˆ (๐ด โˆ– 1o) โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)))
2221simp1d 1143 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘‹ โˆˆ On)
23 oecl 8488 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘‹ โˆˆ On) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
242, 22, 23syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
2521simp2d 1144 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Œ โˆˆ (๐ด โˆ– 1o))
2625eldifad 3927 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ด)
27 onelon 6347 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘Œ โˆˆ ๐ด) โ†’ ๐‘Œ โˆˆ On)
282, 26, 27syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘Œ โˆˆ On)
29 dif1o 8451 . . . . . . . . . . . 12 (๐‘Œ โˆˆ (๐ด โˆ– 1o) โ†” (๐‘Œ โˆˆ ๐ด โˆง ๐‘Œ โ‰  โˆ…))
3029simprbi 498 . . . . . . . . . . 11 (๐‘Œ โˆˆ (๐ด โˆ– 1o) โ†’ ๐‘Œ โ‰  โˆ…)
3125, 30syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ โ‰  โˆ…)
32 on0eln0 6378 . . . . . . . . . . 11 (๐‘Œ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘Œ โ†” ๐‘Œ โ‰  โˆ…))
3328, 32syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆ… โˆˆ ๐‘Œ โ†” ๐‘Œ โ‰  โˆ…))
3431, 33mpbird 257 . . . . . . . . 9 (๐œ‘ โ†’ โˆ… โˆˆ ๐‘Œ)
35 omword1 8525 . . . . . . . . 9 ((((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐‘Œ โˆˆ On) โˆง โˆ… โˆˆ ๐‘Œ) โ†’ (๐ด โ†‘o ๐‘‹) โŠ† ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ))
3624, 28, 34, 35syl21anc 837 . . . . . . . 8 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โŠ† ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ))
37 omcl 8487 . . . . . . . . . . 11 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐‘Œ โˆˆ On) โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โˆˆ On)
3824, 28, 37syl2anc 585 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โˆˆ On)
3921simp3d 1145 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹))
40 onelon 6347 . . . . . . . . . . 11 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โ†’ ๐‘ โˆˆ On)
4124, 39, 40syl2anc 585 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ On)
42 oaword1 8504 . . . . . . . . . 10 ((((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โˆˆ On โˆง ๐‘ โˆˆ On) โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โŠ† (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘))
4338, 41, 42syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โŠ† (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘))
4420simprd 497 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘) = ๐ถ)
4543, 44sseqtrd 3989 . . . . . . . 8 (๐œ‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โŠ† ๐ถ)
4636, 45sstrd 3959 . . . . . . 7 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โŠ† ๐ถ)
47 oecl 8488 . . . . . . . . 9 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
482, 3, 47syl2anc 585 . . . . . . . 8 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
49 ontr2 6369 . . . . . . . 8 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง (๐ด โ†‘o ๐ต) โˆˆ On) โ†’ (((๐ด โ†‘o ๐‘‹) โŠ† ๐ถ โˆง ๐ถ โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต)))
5024, 48, 49syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ (((๐ด โ†‘o ๐‘‹) โŠ† ๐ถ โˆง ๐ถ โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต)))
5146, 6, 50mp2and 698 . . . . . 6 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต))
529simpld 496 . . . . . . 7 (๐œ‘ โ†’ ๐ด โˆˆ (On โˆ– 2o))
53 oeord 8540 . . . . . . 7 ((๐‘‹ โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โˆˆ (On โˆ– 2o)) โ†’ (๐‘‹ โˆˆ ๐ต โ†” (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต)))
5422, 3, 52, 53syl3anc 1372 . . . . . 6 (๐œ‘ โ†’ (๐‘‹ โˆˆ ๐ต โ†” (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต)))
5551, 54mpbird 257 . . . . 5 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
562adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐ด โˆˆ On)
573adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐ต โˆˆ On)
58 suppssdm 8113 . . . . . . . . . . . . . . 15 (๐บ supp โˆ…) โŠ† dom ๐บ
591, 2, 3cantnfs 9609 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บ โˆˆ ๐‘† โ†” (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…)))
604, 59mpbid 231 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…))
6160simpld 496 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐บ:๐ตโŸถ๐ด)
6258, 61fssdm 6693 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
6362sselda 3949 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ฅ โˆˆ ๐ต)
64 onelon 6347 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
6557, 63, 64syl2anc 585 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ฅ โˆˆ On)
66 oecl 8488 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ On)
6756, 65, 66syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ On)
6861adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐บ:๐ตโŸถ๐ด)
6968, 63ffvelcdmd 7041 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐บโ€˜๐‘ฅ) โˆˆ ๐ด)
70 onelon 6347 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง (๐บโ€˜๐‘ฅ) โˆˆ ๐ด) โ†’ (๐บโ€˜๐‘ฅ) โˆˆ On)
7156, 69, 70syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐บโ€˜๐‘ฅ) โˆˆ On)
7261ffnd 6674 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐บ Fn ๐ต)
738elexd 3468 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ… โˆˆ V)
74 elsuppfn 8107 . . . . . . . . . . . . . 14 ((๐บ Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ (๐‘ฅ โˆˆ (๐บ supp โˆ…) โ†” (๐‘ฅ โˆˆ ๐ต โˆง (๐บโ€˜๐‘ฅ) โ‰  โˆ…)))
7572, 3, 73, 74syl3anc 1372 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐บ supp โˆ…) โ†” (๐‘ฅ โˆˆ ๐ต โˆง (๐บโ€˜๐‘ฅ) โ‰  โˆ…)))
7675simplbda 501 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐บโ€˜๐‘ฅ) โ‰  โˆ…)
77 on0eln0 6378 . . . . . . . . . . . . 13 ((๐บโ€˜๐‘ฅ) โˆˆ On โ†’ (โˆ… โˆˆ (๐บโ€˜๐‘ฅ) โ†” (๐บโ€˜๐‘ฅ) โ‰  โˆ…))
7871, 77syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โˆ… โˆˆ (๐บโ€˜๐‘ฅ) โ†” (๐บโ€˜๐‘ฅ) โ‰  โˆ…))
7976, 78mpbird 257 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ โˆ… โˆˆ (๐บโ€˜๐‘ฅ))
80 omword1 8525 . . . . . . . . . . 11 ((((๐ด โ†‘o ๐‘ฅ) โˆˆ On โˆง (๐บโ€˜๐‘ฅ) โˆˆ On) โˆง โˆ… โˆˆ (๐บโ€˜๐‘ฅ)) โ†’ (๐ด โ†‘o ๐‘ฅ) โŠ† ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)))
8167, 71, 79, 80syl21anc 837 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โŠ† ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)))
82 eqid 2737 . . . . . . . . . . . 12 OrdIso( E , (๐บ supp โˆ…)) = OrdIso( E , (๐บ supp โˆ…))
834adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐บ โˆˆ ๐‘†)
84 eqid 2737 . . . . . . . . . . . 12 seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , (๐บ supp โˆ…))โ€˜๐‘˜)) ยทo (๐บโ€˜(OrdIso( E , (๐บ supp โˆ…))โ€˜๐‘˜))) +o ๐‘ง)), โˆ…) = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , (๐บ supp โˆ…))โ€˜๐‘˜)) ยทo (๐บโ€˜(OrdIso( E , (๐บ supp โˆ…))โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
851, 56, 57, 82, 83, 84, 63cantnfle 9614 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)) โŠ† ((๐ด CNF ๐ต)โ€˜๐บ))
86 cantnf.v . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = ๐‘)
8786adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = ๐‘)
8885, 87sseqtrd 3989 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)) โŠ† ๐‘)
8981, 88sstrd 3959 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โŠ† ๐‘)
9039adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹))
9124adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
92 ontr2 6369 . . . . . . . . . 10 (((๐ด โ†‘o ๐‘ฅ) โˆˆ On โˆง (๐ด โ†‘o ๐‘‹) โˆˆ On) โ†’ (((๐ด โ†‘o ๐‘ฅ) โŠ† ๐‘ โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹)))
9367, 91, 92syl2anc 585 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (((๐ด โ†‘o ๐‘ฅ) โŠ† ๐‘ โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹)))
9489, 90, 93mp2and 698 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹))
9522adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘‹ โˆˆ On)
9652adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐ด โˆˆ (On โˆ– 2o))
97 oeord 8540 . . . . . . . . 9 ((๐‘ฅ โˆˆ On โˆง ๐‘‹ โˆˆ On โˆง ๐ด โˆˆ (On โˆ– 2o)) โ†’ (๐‘ฅ โˆˆ ๐‘‹ โ†” (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹)))
9865, 95, 96, 97syl3anc 1372 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐‘ฅ โˆˆ ๐‘‹ โ†” (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹)))
9994, 98mpbird 257 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ฅ โˆˆ ๐‘‹)
10099ex 414 . . . . . 6 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐บ supp โˆ…) โ†’ ๐‘ฅ โˆˆ ๐‘‹))
101100ssrdv 3955 . . . . 5 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ๐‘‹)
102 cantnf.f . . . . 5 ๐น = (๐‘ก โˆˆ ๐ต โ†ฆ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)))
1031, 2, 3, 4, 55, 26, 101, 102cantnfp1 9624 . . . 4 (๐œ‘ โ†’ (๐น โˆˆ ๐‘† โˆง ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ))))
104103simprd 497 . . 3 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
10586oveq2d 7378 . . 3 (๐œ‘ โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘))
106104, 105, 443eqtrd 2781 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = ๐ถ)
1071, 2, 3cantnff 9617 . . . 4 (๐œ‘ โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
108107ffnd 6674 . . 3 (๐œ‘ โ†’ (๐ด CNF ๐ต) Fn ๐‘†)
109103simpld 496 . . 3 (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
110 fnfvelrn 7036 . . 3 (((๐ด CNF ๐ต) Fn ๐‘† โˆง ๐น โˆˆ ๐‘†) โ†’ ((๐ด CNF ๐ต)โ€˜๐น) โˆˆ ran (๐ด CNF ๐ต))
111108, 109, 110syl2anc 585 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) โˆˆ ran (๐ด CNF ๐ต))
112106, 111eqeltrrd 2839 1 (๐œ‘ โ†’ ๐ถ โˆˆ ran (๐ด CNF ๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆ€wral 3065  โˆƒwrex 3074  {crab 3410  Vcvv 3448   โˆ– cdif 3912   โŠ† wss 3915  โˆ…c0 4287  ifcif 4491  โŸจcop 4597  โˆช cuni 4870  โˆฉ cint 4912   class class class wbr 5110  {copab 5172   โ†ฆ cmpt 5193   E cep 5541  dom cdm 5638  ran crn 5639  Oncon0 6322  โ„ฉcio 6451   Fn wfn 6496  โŸถwf 6497  โ€˜cfv 6501  (class class class)co 7362   โˆˆ cmpo 7364  1st c1st 7924  2nd c2nd 7925   supp csupp 8097  seqฯ‰cseqom 8398  1oc1o 8410  2oc2o 8411   +o coa 8414   ยทo comu 8415   โ†‘o coe 8416   finSupp cfsupp 9312  OrdIsocoi 9452   CNF ccnf 9604
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-seqom 8399  df-1o 8417  df-2o 8418  df-oadd 8421  df-omul 8422  df-oexp 8423  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-oi 9453  df-cnf 9605
This theorem is referenced by:  cantnflem4  9635
  Copyright terms: Public domain W3C validator