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

Theorem cantnflem3 9688
Description: Lemma for cantnf 9690. 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 8605 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 9678 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 9687 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ด โˆˆ (On โˆ– 2o) โˆง ๐ถ โˆˆ (On โˆ– 1o)))
10 eqid 2730 . . . . . . . . . . . . . . 15 ๐‘‹ = ๐‘‹
11 eqid 2730 . . . . . . . . . . . . . . 15 ๐‘Œ = ๐‘Œ
12 eqid 2730 . . . . . . . . . . . . . . 15 ๐‘ = ๐‘
1310, 11, 123pm3.2i 1337 . . . . . . . . . . . . . 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 8604 . . . . . . . . . . . . . 14 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ถ โˆˆ (On โˆ– 1o)) โ†’ (((๐‘‹ โˆˆ On โˆง ๐‘Œ โˆˆ (๐ด โˆ– 1o) โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘) = ๐ถ) โ†” (๐‘‹ = ๐‘‹ โˆง ๐‘Œ = ๐‘Œ โˆง ๐‘ = ๐‘)))
1913, 18mpbiri 257 . . . . . . . . . . . . 13 ((๐ด โˆˆ (On โˆ– 2o) โˆง ๐ถ โˆˆ (On โˆ– 1o)) โ†’ ((๐‘‹ โˆˆ On โˆง ๐‘Œ โˆˆ (๐ด โˆ– 1o) โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘) = ๐ถ))
209, 19syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘‹ โˆˆ On โˆง ๐‘Œ โˆˆ (๐ด โˆ– 1o) โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โˆง (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘) = ๐ถ))
2120simpld 493 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‹ โˆˆ On โˆง ๐‘Œ โˆˆ (๐ด โˆ– 1o) โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)))
2221simp1d 1140 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘‹ โˆˆ On)
23 oecl 8539 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘‹ โˆˆ On) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
242, 22, 23syl2anc 582 . . . . . . . . 9 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
2521simp2d 1141 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Œ โˆˆ (๐ด โˆ– 1o))
2625eldifad 3959 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ด)
27 onelon 6388 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘Œ โˆˆ ๐ด) โ†’ ๐‘Œ โˆˆ On)
282, 26, 27syl2anc 582 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘Œ โˆˆ On)
29 dif1o 8502 . . . . . . . . . . . 12 (๐‘Œ โˆˆ (๐ด โˆ– 1o) โ†” (๐‘Œ โˆˆ ๐ด โˆง ๐‘Œ โ‰  โˆ…))
3029simprbi 495 . . . . . . . . . . 11 (๐‘Œ โˆˆ (๐ด โˆ– 1o) โ†’ ๐‘Œ โ‰  โˆ…)
3125, 30syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ โ‰  โˆ…)
32 on0eln0 6419 . . . . . . . . . . 11 (๐‘Œ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘Œ โ†” ๐‘Œ โ‰  โˆ…))
3328, 32syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆ… โˆˆ ๐‘Œ โ†” ๐‘Œ โ‰  โˆ…))
3431, 33mpbird 256 . . . . . . . . 9 (๐œ‘ โ†’ โˆ… โˆˆ ๐‘Œ)
35 omword1 8575 . . . . . . . . 9 ((((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐‘Œ โˆˆ On) โˆง โˆ… โˆˆ ๐‘Œ) โ†’ (๐ด โ†‘o ๐‘‹) โІ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ))
3624, 28, 34, 35syl21anc 834 . . . . . . . 8 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โІ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ))
37 omcl 8538 . . . . . . . . . . 11 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐‘Œ โˆˆ On) โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โˆˆ On)
3824, 28, 37syl2anc 582 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โˆˆ On)
3921simp3d 1142 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹))
40 onelon 6388 . . . . . . . . . . 11 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โ†’ ๐‘ โˆˆ On)
4124, 39, 40syl2anc 582 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ On)
42 oaword1 8554 . . . . . . . . . 10 ((((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โˆˆ On โˆง ๐‘ โˆˆ On) โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โІ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘))
4338, 41, 42syl2anc 582 . . . . . . . . 9 (๐œ‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โІ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘))
4420simprd 494 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘) = ๐ถ)
4543, 44sseqtrd 4021 . . . . . . . 8 (๐œ‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โІ ๐ถ)
4636, 45sstrd 3991 . . . . . . 7 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โІ ๐ถ)
47 oecl 8539 . . . . . . . . 9 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
482, 3, 47syl2anc 582 . . . . . . . 8 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
49 ontr2 6410 . . . . . . . 8 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง (๐ด โ†‘o ๐ต) โˆˆ On) โ†’ (((๐ด โ†‘o ๐‘‹) โІ ๐ถ โˆง ๐ถ โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต)))
5024, 48, 49syl2anc 582 . . . . . . 7 (๐œ‘ โ†’ (((๐ด โ†‘o ๐‘‹) โІ ๐ถ โˆง ๐ถ โˆˆ (๐ด โ†‘o ๐ต)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต)))
5146, 6, 50mp2and 695 . . . . . 6 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต))
529simpld 493 . . . . . . 7 (๐œ‘ โ†’ ๐ด โˆˆ (On โˆ– 2o))
53 oeord 8590 . . . . . . 7 ((๐‘‹ โˆˆ On โˆง ๐ต โˆˆ On โˆง ๐ด โˆˆ (On โˆ– 2o)) โ†’ (๐‘‹ โˆˆ ๐ต โ†” (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต)))
5422, 3, 52, 53syl3anc 1369 . . . . . 6 (๐œ‘ โ†’ (๐‘‹ โˆˆ ๐ต โ†” (๐ด โ†‘o ๐‘‹) โˆˆ (๐ด โ†‘o ๐ต)))
5551, 54mpbird 256 . . . . 5 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
562adantr 479 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐ด โˆˆ On)
573adantr 479 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐ต โˆˆ On)
58 suppssdm 8164 . . . . . . . . . . . . . . 15 (๐บ supp โˆ…) โІ dom ๐บ
591, 2, 3cantnfs 9663 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บ โˆˆ ๐‘† โ†” (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…)))
604, 59mpbid 231 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…))
6160simpld 493 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐บ:๐ตโŸถ๐ด)
6258, 61fssdm 6736 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐บ supp โˆ…) โІ ๐ต)
6362sselda 3981 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ฅ โˆˆ ๐ต)
64 onelon 6388 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
6557, 63, 64syl2anc 582 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ฅ โˆˆ On)
66 oecl 8539 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ On)
6756, 65, 66syl2anc 582 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ On)
6861adantr 479 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐บ:๐ตโŸถ๐ด)
6968, 63ffvelcdmd 7086 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐บโ€˜๐‘ฅ) โˆˆ ๐ด)
70 onelon 6388 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง (๐บโ€˜๐‘ฅ) โˆˆ ๐ด) โ†’ (๐บโ€˜๐‘ฅ) โˆˆ On)
7156, 69, 70syl2anc 582 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐บโ€˜๐‘ฅ) โˆˆ On)
7261ffnd 6717 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐บ Fn ๐ต)
738elexd 3493 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ… โˆˆ V)
74 elsuppfn 8158 . . . . . . . . . . . . . 14 ((๐บ Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ (๐‘ฅ โˆˆ (๐บ supp โˆ…) โ†” (๐‘ฅ โˆˆ ๐ต โˆง (๐บโ€˜๐‘ฅ) โ‰  โˆ…)))
7572, 3, 73, 74syl3anc 1369 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐บ supp โˆ…) โ†” (๐‘ฅ โˆˆ ๐ต โˆง (๐บโ€˜๐‘ฅ) โ‰  โˆ…)))
7675simplbda 498 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐บโ€˜๐‘ฅ) โ‰  โˆ…)
77 on0eln0 6419 . . . . . . . . . . . . 13 ((๐บโ€˜๐‘ฅ) โˆˆ On โ†’ (โˆ… โˆˆ (๐บโ€˜๐‘ฅ) โ†” (๐บโ€˜๐‘ฅ) โ‰  โˆ…))
7871, 77syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โˆ… โˆˆ (๐บโ€˜๐‘ฅ) โ†” (๐บโ€˜๐‘ฅ) โ‰  โˆ…))
7976, 78mpbird 256 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ โˆ… โˆˆ (๐บโ€˜๐‘ฅ))
80 omword1 8575 . . . . . . . . . . 11 ((((๐ด โ†‘o ๐‘ฅ) โˆˆ On โˆง (๐บโ€˜๐‘ฅ) โˆˆ On) โˆง โˆ… โˆˆ (๐บโ€˜๐‘ฅ)) โ†’ (๐ด โ†‘o ๐‘ฅ) โІ ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)))
8167, 71, 79, 80syl21anc 834 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โІ ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)))
82 eqid 2730 . . . . . . . . . . . 12 OrdIso( E , (๐บ supp โˆ…)) = OrdIso( E , (๐บ supp โˆ…))
834adantr 479 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐บ โˆˆ ๐‘†)
84 eqid 2730 . . . . . . . . . . . 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 9668 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)) โІ ((๐ด CNF ๐ต)โ€˜๐บ))
86 cantnf.v . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = ๐‘)
8786adantr 479 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = ๐‘)
8885, 87sseqtrd 4021 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)) โІ ๐‘)
8981, 88sstrd 3991 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โІ ๐‘)
9039adantr 479 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹))
9124adantr 479 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
92 ontr2 6410 . . . . . . . . . 10 (((๐ด โ†‘o ๐‘ฅ) โˆˆ On โˆง (๐ด โ†‘o ๐‘‹) โˆˆ On) โ†’ (((๐ด โ†‘o ๐‘ฅ) โІ ๐‘ โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹)))
9367, 91, 92syl2anc 582 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (((๐ด โ†‘o ๐‘ฅ) โІ ๐‘ โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹)))
9489, 90, 93mp2and 695 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹))
9522adantr 479 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘‹ โˆˆ On)
9652adantr 479 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐ด โˆˆ (On โˆ– 2o))
97 oeord 8590 . . . . . . . . 9 ((๐‘ฅ โˆˆ On โˆง ๐‘‹ โˆˆ On โˆง ๐ด โˆˆ (On โˆ– 2o)) โ†’ (๐‘ฅ โˆˆ ๐‘‹ โ†” (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹)))
9865, 95, 96, 97syl3anc 1369 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐‘ฅ โˆˆ ๐‘‹ โ†” (๐ด โ†‘o ๐‘ฅ) โˆˆ (๐ด โ†‘o ๐‘‹)))
9994, 98mpbird 256 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ฅ โˆˆ ๐‘‹)
10099ex 411 . . . . . 6 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐บ supp โˆ…) โ†’ ๐‘ฅ โˆˆ ๐‘‹))
101100ssrdv 3987 . . . . 5 (๐œ‘ โ†’ (๐บ supp โˆ…) โІ ๐‘‹)
102 cantnf.f . . . . 5 ๐น = (๐‘ก โˆˆ ๐ต โ†ฆ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)))
1031, 2, 3, 4, 55, 26, 101, 102cantnfp1 9678 . . . 4 (๐œ‘ โ†’ (๐น โˆˆ ๐‘† โˆง ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ))))
104103simprd 494 . . 3 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
10586oveq2d 7427 . . 3 (๐œ‘ โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘))
106104, 105, 443eqtrd 2774 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = ๐ถ)
1071, 2, 3cantnff 9671 . . . 4 (๐œ‘ โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
108107ffnd 6717 . . 3 (๐œ‘ โ†’ (๐ด CNF ๐ต) Fn ๐‘†)
109103simpld 493 . . 3 (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
110 fnfvelrn 7081 . . 3 (((๐ด CNF ๐ต) Fn ๐‘† โˆง ๐น โˆˆ ๐‘†) โ†’ ((๐ด CNF ๐ต)โ€˜๐น) โˆˆ ran (๐ด CNF ๐ต))
111108, 109, 110syl2anc 582 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) โˆˆ ran (๐ด CNF ๐ต))
112106, 111eqeltrrd 2832 1 (๐œ‘ โ†’ ๐ถ โˆˆ ran (๐ด CNF ๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆง w3a 1085   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2938  โˆ€wral 3059  โˆƒwrex 3068  {crab 3430  Vcvv 3472   โˆ– cdif 3944   โІ wss 3947  โˆ…c0 4321  ifcif 4527  โŸจcop 4633  โˆช cuni 4907  โˆฉ cint 4949   class class class wbr 5147  {copab 5209   โ†ฆ cmpt 5230   E cep 5578  dom cdm 5675  ran crn 5676  Oncon0 6363  โ„ฉcio 6492   Fn wfn 6537  โŸถwf 6538  โ€˜cfv 6542  (class class class)co 7411   โˆˆ cmpo 7413  1st c1st 7975  2nd c2nd 7976   supp csupp 8148  seqฯ‰cseqom 8449  1oc1o 8461  2oc2o 8462   +o coa 8465   ยทo comu 8466   โ†‘o coe 8467   finSupp cfsupp 9363  OrdIsocoi 9506   CNF ccnf 9658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-seqom 8450  df-1o 8468  df-2o 8469  df-oadd 8472  df-omul 8473  df-oexp 8474  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-oi 9507  df-cnf 9659
This theorem is referenced by:  cantnflem4  9689
  Copyright terms: Public domain W3C validator