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

Theorem cantnflem3 9686
Description: Lemma for cantnf 9688. 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 8603 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 9676 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 9685 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ด โˆˆ (On โˆ– 2o) โˆง ๐ถ โˆˆ (On โˆ– 1o)))
10 eqid 2733 . . . . . . . . . . . . . . 15 ๐‘‹ = ๐‘‹
11 eqid 2733 . . . . . . . . . . . . . . 15 ๐‘Œ = ๐‘Œ
12 eqid 2733 . . . . . . . . . . . . . . 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 8602 . . . . . . . . . . . . . 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 8537 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘‹ โˆˆ On) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
242, 22, 23syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
2521simp2d 1144 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘Œ โˆˆ (๐ด โˆ– 1o))
2625eldifad 3961 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ด)
27 onelon 6390 . . . . . . . . . 10 ((๐ด โˆˆ On โˆง ๐‘Œ โˆˆ ๐ด) โ†’ ๐‘Œ โˆˆ On)
282, 26, 27syl2anc 585 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘Œ โˆˆ On)
29 dif1o 8500 . . . . . . . . . . . 12 (๐‘Œ โˆˆ (๐ด โˆ– 1o) โ†” (๐‘Œ โˆˆ ๐ด โˆง ๐‘Œ โ‰  โˆ…))
3029simprbi 498 . . . . . . . . . . 11 (๐‘Œ โˆˆ (๐ด โˆ– 1o) โ†’ ๐‘Œ โ‰  โˆ…)
3125, 30syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘Œ โ‰  โˆ…)
32 on0eln0 6421 . . . . . . . . . . 11 (๐‘Œ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘Œ โ†” ๐‘Œ โ‰  โˆ…))
3328, 32syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆ… โˆˆ ๐‘Œ โ†” ๐‘Œ โ‰  โˆ…))
3431, 33mpbird 257 . . . . . . . . 9 (๐œ‘ โ†’ โˆ… โˆˆ ๐‘Œ)
35 omword1 8573 . . . . . . . . 9 ((((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐‘Œ โˆˆ On) โˆง โˆ… โˆˆ ๐‘Œ) โ†’ (๐ด โ†‘o ๐‘‹) โŠ† ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ))
3624, 28, 34, 35syl21anc 837 . . . . . . . 8 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โŠ† ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ))
37 omcl 8536 . . . . . . . . . . 11 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐‘Œ โˆˆ On) โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โˆˆ On)
3824, 28, 37syl2anc 585 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โˆˆ On)
3921simp3d 1145 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹))
40 onelon 6390 . . . . . . . . . . 11 (((๐ด โ†‘o ๐‘‹) โˆˆ On โˆง ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹)) โ†’ ๐‘ โˆˆ On)
4124, 39, 40syl2anc 585 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ On)
42 oaword1 8552 . . . . . . . . . 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 4023 . . . . . . . 8 (๐œ‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) โŠ† ๐ถ)
4636, 45sstrd 3993 . . . . . . 7 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โŠ† ๐ถ)
47 oecl 8537 . . . . . . . . 9 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
482, 3, 47syl2anc 585 . . . . . . . 8 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
49 ontr2 6412 . . . . . . . 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 8588 . . . . . . 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 8162 . . . . . . . . . . . . . . 15 (๐บ supp โˆ…) โŠ† dom ๐บ
591, 2, 3cantnfs 9661 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บ โˆˆ ๐‘† โ†” (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…)))
604, 59mpbid 231 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…))
6160simpld 496 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐บ:๐ตโŸถ๐ด)
6258, 61fssdm 6738 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
6362sselda 3983 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ฅ โˆˆ ๐ต)
64 onelon 6390 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
6557, 63, 64syl2anc 585 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ฅ โˆˆ On)
66 oecl 8537 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ On)
6756, 65, 66syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โˆˆ On)
6861adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐บ:๐ตโŸถ๐ด)
6968, 63ffvelcdmd 7088 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐บโ€˜๐‘ฅ) โˆˆ ๐ด)
70 onelon 6390 . . . . . . . . . . . 12 ((๐ด โˆˆ On โˆง (๐บโ€˜๐‘ฅ) โˆˆ ๐ด) โ†’ (๐บโ€˜๐‘ฅ) โˆˆ On)
7156, 69, 70syl2anc 585 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐บโ€˜๐‘ฅ) โˆˆ On)
7261ffnd 6719 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐บ Fn ๐ต)
738elexd 3495 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ… โˆˆ V)
74 elsuppfn 8156 . . . . . . . . . . . . . 14 ((๐บ Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ (๐‘ฅ โˆˆ (๐บ supp โˆ…) โ†” (๐‘ฅ โˆˆ ๐ต โˆง (๐บโ€˜๐‘ฅ) โ‰  โˆ…)))
7572, 3, 73, 74syl3anc 1372 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (๐บ supp โˆ…) โ†” (๐‘ฅ โˆˆ ๐ต โˆง (๐บโ€˜๐‘ฅ) โ‰  โˆ…)))
7675simplbda 501 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐บโ€˜๐‘ฅ) โ‰  โˆ…)
77 on0eln0 6421 . . . . . . . . . . . . 13 ((๐บโ€˜๐‘ฅ) โˆˆ On โ†’ (โˆ… โˆˆ (๐บโ€˜๐‘ฅ) โ†” (๐บโ€˜๐‘ฅ) โ‰  โˆ…))
7871, 77syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โˆ… โˆˆ (๐บโ€˜๐‘ฅ) โ†” (๐บโ€˜๐‘ฅ) โ‰  โˆ…))
7976, 78mpbird 257 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ โˆ… โˆˆ (๐บโ€˜๐‘ฅ))
80 omword1 8573 . . . . . . . . . . 11 ((((๐ด โ†‘o ๐‘ฅ) โˆˆ On โˆง (๐บโ€˜๐‘ฅ) โˆˆ On) โˆง โˆ… โˆˆ (๐บโ€˜๐‘ฅ)) โ†’ (๐ด โ†‘o ๐‘ฅ) โŠ† ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)))
8167, 71, 79, 80syl21anc 837 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โŠ† ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)))
82 eqid 2733 . . . . . . . . . . . 12 OrdIso( E , (๐บ supp โˆ…)) = OrdIso( E , (๐บ supp โˆ…))
834adantr 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐บ โˆˆ ๐‘†)
84 eqid 2733 . . . . . . . . . . . 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 9666 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)) โŠ† ((๐ด CNF ๐ต)โ€˜๐บ))
86 cantnf.v . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = ๐‘)
8786adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = ๐‘)
8885, 87sseqtrd 4023 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐ด โ†‘o ๐‘ฅ) ยทo (๐บโ€˜๐‘ฅ)) โŠ† ๐‘)
8981, 88sstrd 3993 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘ฅ) โŠ† ๐‘)
9039adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘ โˆˆ (๐ด โ†‘o ๐‘‹))
9124adantr 482 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
92 ontr2 6412 . . . . . . . . . 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 8588 . . . . . . . . 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 3989 . . . . 5 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ๐‘‹)
102 cantnf.f . . . . 5 ๐น = (๐‘ก โˆˆ ๐ต โ†ฆ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)))
1031, 2, 3, 4, 55, 26, 101, 102cantnfp1 9676 . . . 4 (๐œ‘ โ†’ (๐น โˆˆ ๐‘† โˆง ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ))))
104103simprd 497 . . 3 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
10586oveq2d 7425 . . 3 (๐œ‘ โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘))
106104, 105, 443eqtrd 2777 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = ๐ถ)
1071, 2, 3cantnff 9669 . . . 4 (๐œ‘ โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
108107ffnd 6719 . . 3 (๐œ‘ โ†’ (๐ด CNF ๐ต) Fn ๐‘†)
109103simpld 496 . . 3 (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
110 fnfvelrn 7083 . . 3 (((๐ด CNF ๐ต) Fn ๐‘† โˆง ๐น โˆˆ ๐‘†) โ†’ ((๐ด CNF ๐ต)โ€˜๐น) โˆˆ ran (๐ด CNF ๐ต))
111108, 109, 110syl2anc 585 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) โˆˆ ran (๐ด CNF ๐ต))
112106, 111eqeltrrd 2835 1 (๐œ‘ โ†’ ๐ถ โˆˆ ran (๐ด CNF ๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2941  โˆ€wral 3062  โˆƒwrex 3071  {crab 3433  Vcvv 3475   โˆ– cdif 3946   โŠ† wss 3949  โˆ…c0 4323  ifcif 4529  โŸจcop 4635  โˆช cuni 4909  โˆฉ cint 4951   class class class wbr 5149  {copab 5211   โ†ฆ cmpt 5232   E cep 5580  dom cdm 5677  ran crn 5678  Oncon0 6365  โ„ฉcio 6494   Fn wfn 6539  โŸถwf 6540  โ€˜cfv 6544  (class class class)co 7409   โˆˆ cmpo 7411  1st c1st 7973  2nd c2nd 7974   supp csupp 8146  seqฯ‰cseqom 8447  1oc1o 8459  2oc2o 8460   +o coa 8463   ยทo comu 8464   โ†‘o coe 8465   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:  cantnflem4  9687
  Copyright terms: Public domain W3C validator