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

Theorem cantnfp1 9678
Description: If ๐น is created by adding a single term (๐นโ€˜๐‘‹) = ๐‘Œ to ๐บ, where ๐‘‹ is larger than any element of the support of ๐บ, then ๐น is also a finitely supported function and it is assigned the value ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ๐‘ง where ๐‘ง is the value of ๐บ. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 1-Jul-2019.)
Hypotheses
Ref Expression
cantnfs.s ๐‘† = dom (๐ด CNF ๐ต)
cantnfs.a (๐œ‘ โ†’ ๐ด โˆˆ On)
cantnfs.b (๐œ‘ โ†’ ๐ต โˆˆ On)
cantnfp1.g (๐œ‘ โ†’ ๐บ โˆˆ ๐‘†)
cantnfp1.x (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
cantnfp1.y (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ด)
cantnfp1.s (๐œ‘ โ†’ (๐บ supp โˆ…) โІ ๐‘‹)
cantnfp1.f ๐น = (๐‘ก โˆˆ ๐ต โ†ฆ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)))
Assertion
Ref Expression
cantnfp1 (๐œ‘ โ†’ (๐น โˆˆ ๐‘† โˆง ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ))))
Distinct variable groups:   ๐‘ก,๐ต   ๐‘ก,๐ด   ๐‘ก,๐‘†   ๐‘ก,๐บ   ๐œ‘,๐‘ก   ๐‘ก,๐‘Œ   ๐‘ก,๐‘‹
Allowed substitution hint:   ๐น(๐‘ก)

Proof of Theorem cantnfp1
Dummy variables ๐‘˜ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfp1.f . . . . . 6 ๐น = (๐‘ก โˆˆ ๐ต โ†ฆ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)))
2 cantnfs.b . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ต โˆˆ On)
3 cantnfp1.x . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
4 onelon 6388 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘‹ โˆˆ ๐ต) โ†’ ๐‘‹ โˆˆ On)
52, 3, 4syl2anc 582 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ On)
6 eloni 6373 . . . . . . . . . . . 12 (๐‘‹ โˆˆ On โ†’ Ord ๐‘‹)
7 ordirr 6381 . . . . . . . . . . . 12 (Ord ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹)
85, 6, 73syl 18 . . . . . . . . . . 11 (๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹)
9 fvex 6903 . . . . . . . . . . . . . 14 (๐บโ€˜๐‘‹) โˆˆ V
10 dif1o 8502 . . . . . . . . . . . . . 14 ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” ((๐บโ€˜๐‘‹) โˆˆ V โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…))
119, 10mpbiran 705 . . . . . . . . . . . . 13 ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” (๐บโ€˜๐‘‹) โ‰  โˆ…)
12 cantnfp1.g . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ๐บ โˆˆ ๐‘†)
13 cantnfs.s . . . . . . . . . . . . . . . . . . . . 21 ๐‘† = dom (๐ด CNF ๐ต)
14 cantnfs.a . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ด โˆˆ On)
1513, 14, 2cantnfs 9663 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ โˆˆ ๐‘† โ†” (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…)))
1612, 15mpbid 231 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…))
1716simpld 493 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ:๐ตโŸถ๐ด)
1817ffnd 6717 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ๐บ Fn ๐ต)
19 0ex 5306 . . . . . . . . . . . . . . . . . 18 โˆ… โˆˆ V
2019a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ โˆ… โˆˆ V)
21 elsuppfn 8158 . . . . . . . . . . . . . . . . 17 ((๐บ Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…)))
2218, 2, 20, 21syl3anc 1369 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…)))
2311bicomi 223 . . . . . . . . . . . . . . . . . 18 ((๐บโ€˜๐‘‹) โ‰  โˆ… โ†” (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o))
2423a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โ‰  โˆ… โ†” (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o)))
2524anbi2d 627 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o))))
2622, 25bitrd 278 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o))))
27 cantnfp1.s . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐บ supp โˆ…) โІ ๐‘‹)
2827sseld 3980 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†’ ๐‘‹ โˆˆ ๐‘‹))
2926, 28sylbird 259 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o)) โ†’ ๐‘‹ โˆˆ ๐‘‹))
303, 29mpand 691 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†’ ๐‘‹ โˆˆ ๐‘‹))
3111, 30biimtrrid 242 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โ‰  โˆ… โ†’ ๐‘‹ โˆˆ ๐‘‹))
3231necon1bd 2956 . . . . . . . . . . 11 (๐œ‘ โ†’ (ยฌ ๐‘‹ โˆˆ ๐‘‹ โ†’ (๐บโ€˜๐‘‹) = โˆ…))
338, 32mpd 15 . . . . . . . . . 10 (๐œ‘ โ†’ (๐บโ€˜๐‘‹) = โˆ…)
3433ad3antrrr 726 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘Œ = โˆ…) โˆง ๐‘ก โˆˆ ๐ต) โˆง ๐‘ก = ๐‘‹) โ†’ (๐บโ€˜๐‘‹) = โˆ…)
35 simpr 483 . . . . . . . . . 10 ((((๐œ‘ โˆง ๐‘Œ = โˆ…) โˆง ๐‘ก โˆˆ ๐ต) โˆง ๐‘ก = ๐‘‹) โ†’ ๐‘ก = ๐‘‹)
3635fveq2d 6894 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘Œ = โˆ…) โˆง ๐‘ก โˆˆ ๐ต) โˆง ๐‘ก = ๐‘‹) โ†’ (๐บโ€˜๐‘ก) = (๐บโ€˜๐‘‹))
37 simpllr 772 . . . . . . . . 9 ((((๐œ‘ โˆง ๐‘Œ = โˆ…) โˆง ๐‘ก โˆˆ ๐ต) โˆง ๐‘ก = ๐‘‹) โ†’ ๐‘Œ = โˆ…)
3834, 36, 373eqtr4rd 2781 . . . . . . . 8 ((((๐œ‘ โˆง ๐‘Œ = โˆ…) โˆง ๐‘ก โˆˆ ๐ต) โˆง ๐‘ก = ๐‘‹) โ†’ ๐‘Œ = (๐บโ€˜๐‘ก))
39 eqidd 2731 . . . . . . . 8 ((((๐œ‘ โˆง ๐‘Œ = โˆ…) โˆง ๐‘ก โˆˆ ๐ต) โˆง ยฌ ๐‘ก = ๐‘‹) โ†’ (๐บโ€˜๐‘ก) = (๐บโ€˜๐‘ก))
4038, 39ifeqda 4563 . . . . . . 7 (((๐œ‘ โˆง ๐‘Œ = โˆ…) โˆง ๐‘ก โˆˆ ๐ต) โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = (๐บโ€˜๐‘ก))
4140mpteq2dva 5247 . . . . . 6 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ (๐‘ก โˆˆ ๐ต โ†ฆ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก))) = (๐‘ก โˆˆ ๐ต โ†ฆ (๐บโ€˜๐‘ก)))
421, 41eqtrid 2782 . . . . 5 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ ๐น = (๐‘ก โˆˆ ๐ต โ†ฆ (๐บโ€˜๐‘ก)))
4317feqmptd 6959 . . . . . 6 (๐œ‘ โ†’ ๐บ = (๐‘ก โˆˆ ๐ต โ†ฆ (๐บโ€˜๐‘ก)))
4443adantr 479 . . . . 5 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ ๐บ = (๐‘ก โˆˆ ๐ต โ†ฆ (๐บโ€˜๐‘ก)))
4542, 44eqtr4d 2773 . . . 4 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ ๐น = ๐บ)
4612adantr 479 . . . 4 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ ๐บ โˆˆ ๐‘†)
4745, 46eqeltrd 2831 . . 3 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ ๐น โˆˆ ๐‘†)
48 oecl 8539 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
4914, 2, 48syl2anc 582 . . . . . . 7 (๐œ‘ โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
5013, 14, 2cantnff 9671 . . . . . . . 8 (๐œ‘ โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
5150, 12ffvelcdmd 7086 . . . . . . 7 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) โˆˆ (๐ด โ†‘o ๐ต))
52 onelon 6388 . . . . . . 7 (((๐ด โ†‘o ๐ต) โˆˆ On โˆง ((๐ด CNF ๐ต)โ€˜๐บ) โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) โˆˆ On)
5349, 51, 52syl2anc 582 . . . . . 6 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) โˆˆ On)
5453adantr 479 . . . . 5 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) โˆˆ On)
55 oa0r 8540 . . . . 5 (((๐ด CNF ๐ต)โ€˜๐บ) โˆˆ On โ†’ (โˆ… +o ((๐ด CNF ๐ต)โ€˜๐บ)) = ((๐ด CNF ๐ต)โ€˜๐บ))
5654, 55syl 17 . . . 4 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ (โˆ… +o ((๐ด CNF ๐ต)โ€˜๐บ)) = ((๐ด CNF ๐ต)โ€˜๐บ))
57 oveq2 7419 . . . . . 6 (๐‘Œ = โˆ… โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) = ((๐ด โ†‘o ๐‘‹) ยทo โˆ…))
58 oecl 8539 . . . . . . . 8 ((๐ด โˆˆ On โˆง ๐‘‹ โˆˆ On) โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
5914, 5, 58syl2anc 582 . . . . . . 7 (๐œ‘ โ†’ (๐ด โ†‘o ๐‘‹) โˆˆ On)
60 om0 8519 . . . . . . 7 ((๐ด โ†‘o ๐‘‹) โˆˆ On โ†’ ((๐ด โ†‘o ๐‘‹) ยทo โˆ…) = โˆ…)
6159, 60syl 17 . . . . . 6 (๐œ‘ โ†’ ((๐ด โ†‘o ๐‘‹) ยทo โˆ…) = โˆ…)
6257, 61sylan9eqr 2792 . . . . 5 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) = โˆ…)
6362oveq1d 7426 . . . 4 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)) = (โˆ… +o ((๐ด CNF ๐ต)โ€˜๐บ)))
6445fveq2d 6894 . . . 4 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = ((๐ด CNF ๐ต)โ€˜๐บ))
6556, 63, 643eqtr4rd 2781 . . 3 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
6647, 65jca 510 . 2 ((๐œ‘ โˆง ๐‘Œ = โˆ…) โ†’ (๐น โˆˆ ๐‘† โˆง ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ))))
6714adantr 479 . . . 4 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ ๐ด โˆˆ On)
682adantr 479 . . . 4 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ ๐ต โˆˆ On)
6912adantr 479 . . . 4 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ ๐บ โˆˆ ๐‘†)
703adantr 479 . . . 4 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ ๐‘‹ โˆˆ ๐ต)
71 cantnfp1.y . . . . 5 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ด)
7271adantr 479 . . . 4 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ ๐‘Œ โˆˆ ๐ด)
7327adantr 479 . . . 4 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ (๐บ supp โˆ…) โІ ๐‘‹)
7413, 67, 68, 69, 70, 72, 73, 1cantnfp1lem1 9675 . . 3 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ ๐น โˆˆ ๐‘†)
75 onelon 6388 . . . . . . 7 ((๐ด โˆˆ On โˆง ๐‘Œ โˆˆ ๐ด) โ†’ ๐‘Œ โˆˆ On)
7614, 71, 75syl2anc 582 . . . . . 6 (๐œ‘ โ†’ ๐‘Œ โˆˆ On)
77 on0eln0 6419 . . . . . 6 (๐‘Œ โˆˆ On โ†’ (โˆ… โˆˆ ๐‘Œ โ†” ๐‘Œ โ‰  โˆ…))
7876, 77syl 17 . . . . 5 (๐œ‘ โ†’ (โˆ… โˆˆ ๐‘Œ โ†” ๐‘Œ โ‰  โˆ…))
7978biimpar 476 . . . 4 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ โˆ… โˆˆ ๐‘Œ)
80 eqid 2730 . . . 4 OrdIso( E , (๐น supp โˆ…)) = OrdIso( E , (๐น supp โˆ…))
81 eqid 2730 . . . 4 seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , (๐น supp โˆ…))โ€˜๐‘˜)) ยทo (๐นโ€˜(OrdIso( E , (๐น supp โˆ…))โ€˜๐‘˜))) +o ๐‘ง)), โˆ…) = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , (๐น supp โˆ…))โ€˜๐‘˜)) ยทo (๐นโ€˜(OrdIso( E , (๐น supp โˆ…))โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
82 eqid 2730 . . . 4 OrdIso( E , (๐บ supp โˆ…)) = OrdIso( E , (๐บ supp โˆ…))
83 eqid 2730 . . . 4 seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , (๐บ supp โˆ…))โ€˜๐‘˜)) ยทo (๐บโ€˜(OrdIso( E , (๐บ supp โˆ…))โ€˜๐‘˜))) +o ๐‘ง)), โˆ…) = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (OrdIso( E , (๐บ supp โˆ…))โ€˜๐‘˜)) ยทo (๐บโ€˜(OrdIso( E , (๐บ supp โˆ…))โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
8413, 67, 68, 69, 70, 72, 73, 1, 79, 80, 81, 82, 83cantnfp1lem3 9677 . . 3 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
8574, 84jca 510 . 2 ((๐œ‘ โˆง ๐‘Œ โ‰  โˆ…) โ†’ (๐น โˆˆ ๐‘† โˆง ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ))))
8666, 85pm2.61dane 3027 1 (๐œ‘ โ†’ (๐น โˆˆ ๐‘† โˆง ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2938  Vcvv 3472   โˆ– cdif 3944   โІ wss 3947  โˆ…c0 4321  ifcif 4527   class class class wbr 5147   โ†ฆ cmpt 5230   E cep 5578  dom cdm 5675  Ord word 6362  Oncon0 6363   Fn wfn 6537  โŸถwf 6538  โ€˜cfv 6542  (class class class)co 7411   โˆˆ cmpo 7413   supp csupp 8148  seqฯ‰cseqom 8449  1oc1o 8461   +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-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:  cantnflem1d  9685  cantnflem1  9686  cantnflem3  9688  cantnfresb  42376
  Copyright terms: Public domain W3C validator