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

Theorem cantnfp1lem3 9671
Description: Lemma for cantnfp1 9672. (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(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)))
cantnfp1.e (๐œ‘ โ†’ โˆ… โˆˆ ๐‘Œ)
cantnfp1.o ๐‘‚ = OrdIso( E , (๐น supp โˆ…))
cantnfp1.h ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐‘‚โ€˜๐‘˜)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
cantnfp1.k ๐พ = OrdIso( E , (๐บ supp โˆ…))
cantnfp1.m ๐‘€ = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐พโ€˜๐‘˜)) ยทo (๐บโ€˜(๐พโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
Assertion
Ref Expression
cantnfp1lem3 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
Distinct variable groups:   ๐‘ก,๐‘˜,๐‘ง,๐ต   ๐ด,๐‘˜,๐‘ก,๐‘ง   ๐‘˜,๐น,๐‘ง   ๐‘†,๐‘˜,๐‘ก,๐‘ง   ๐‘˜,๐บ,๐‘ก,๐‘ง   ๐‘˜,๐พ,๐‘ก,๐‘ง   ๐‘˜,๐‘‚,๐‘ง   ๐œ‘,๐‘˜,๐‘ก,๐‘ง   ๐‘˜,๐‘Œ,๐‘ก,๐‘ง   ๐‘˜,๐‘‹,๐‘ก,๐‘ง
Allowed substitution hints:   ๐น(๐‘ก)   ๐ป(๐‘ง,๐‘ก,๐‘˜)   ๐‘€(๐‘ง,๐‘ก,๐‘˜)   ๐‘‚(๐‘ก)

Proof of Theorem cantnfp1lem3
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 cantnfp1.o . . 3 ๐‘‚ = OrdIso( E , (๐น supp โˆ…))
5 cantnfp1.g . . . 4 (๐œ‘ โ†’ ๐บ โˆˆ ๐‘†)
6 cantnfp1.x . . . 4 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
7 cantnfp1.y . . . 4 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ด)
8 cantnfp1.s . . . 4 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ๐‘‹)
9 cantnfp1.f . . . 4 ๐น = (๐‘ก โˆˆ ๐ต โ†ฆ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)))
101, 2, 3, 5, 6, 7, 8, 9cantnfp1lem1 9669 . . 3 (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
11 cantnfp1.h . . 3 ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐‘‚โ€˜๐‘˜)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
121, 2, 3, 4, 10, 11cantnfval 9659 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (๐ปโ€˜dom ๐‘‚))
13 cantnfp1.e . . . 4 (๐œ‘ โ†’ โˆ… โˆˆ ๐‘Œ)
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 9670 . . 3 (๐œ‘ โ†’ dom ๐‘‚ = suc โˆช dom ๐‘‚)
1514fveq2d 6892 . 2 (๐œ‘ โ†’ (๐ปโ€˜dom ๐‘‚) = (๐ปโ€˜suc โˆช dom ๐‘‚))
161, 2, 3, 4, 10cantnfcl 9658 . . . . . . 7 (๐œ‘ โ†’ ( E We (๐น supp โˆ…) โˆง dom ๐‘‚ โˆˆ ฯ‰))
1716simprd 496 . . . . . 6 (๐œ‘ โ†’ dom ๐‘‚ โˆˆ ฯ‰)
1814, 17eqeltrrd 2834 . . . . 5 (๐œ‘ โ†’ suc โˆช dom ๐‘‚ โˆˆ ฯ‰)
19 peano2b 7868 . . . . 5 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†” suc โˆช dom ๐‘‚ โˆˆ ฯ‰)
2018, 19sylibr 233 . . . 4 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ ฯ‰)
211, 2, 3, 4, 10, 11cantnfsuc 9661 . . . 4 ((๐œ‘ โˆง โˆช dom ๐‘‚ โˆˆ ฯ‰) โ†’ (๐ปโ€˜suc โˆช dom ๐‘‚) = (((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) +o (๐ปโ€˜โˆช dom ๐‘‚)))
2220, 21mpdan 685 . . 3 (๐œ‘ โ†’ (๐ปโ€˜suc โˆช dom ๐‘‚) = (((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) +o (๐ปโ€˜โˆช dom ๐‘‚)))
23 ovexd 7440 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐น supp โˆ…) โˆˆ V)
2416simpld 495 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ E We (๐น supp โˆ…))
254oiiso 9528 . . . . . . . . . . . . . . 15 (((๐น supp โˆ…) โˆˆ V โˆง E We (๐น supp โˆ…)) โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)))
2623, 24, 25syl2anc 584 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)))
27 isof1o 7316 . . . . . . . . . . . . . 14 (๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)) โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…))
2826, 27syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…))
29 f1ocnv 6842 . . . . . . . . . . . . 13 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ โ—ก๐‘‚:(๐น supp โˆ…)โ€“1-1-ontoโ†’dom ๐‘‚)
30 f1of 6830 . . . . . . . . . . . . 13 (โ—ก๐‘‚:(๐น supp โˆ…)โ€“1-1-ontoโ†’dom ๐‘‚ โ†’ โ—ก๐‘‚:(๐น supp โˆ…)โŸถdom ๐‘‚)
3128, 29, 303syl 18 . . . . . . . . . . . 12 (๐œ‘ โ†’ โ—ก๐‘‚:(๐น supp โˆ…)โŸถdom ๐‘‚)
32 iftrue 4533 . . . . . . . . . . . . . . 15 (๐‘ก = ๐‘‹ โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = ๐‘Œ)
339, 32, 6, 7fvmptd3 7018 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐นโ€˜๐‘‹) = ๐‘Œ)
3413ne0d 4334 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘Œ โ‰  โˆ…)
3533, 34eqnetrd 3008 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐นโ€˜๐‘‹) โ‰  โˆ…)
367adantr 481 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ก โˆˆ ๐ต) โ†’ ๐‘Œ โˆˆ ๐ด)
371, 2, 3cantnfs 9657 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ โˆˆ ๐‘† โ†” (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…)))
385, 37mpbid 231 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…))
3938simpld 495 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ:๐ตโŸถ๐ด)
4039ffvelcdmda 7083 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ก โˆˆ ๐ต) โ†’ (๐บโ€˜๐‘ก) โˆˆ ๐ด)
4136, 40ifcld 4573 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ก โˆˆ ๐ต) โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) โˆˆ ๐ด)
4241, 9fmptd 7110 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐น:๐ตโŸถ๐ด)
4342ffnd 6715 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐น Fn ๐ต)
44 0ex 5306 . . . . . . . . . . . . . . 15 โˆ… โˆˆ V
4544a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ… โˆˆ V)
46 elsuppfn 8152 . . . . . . . . . . . . . 14 ((๐น Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ (๐‘‹ โˆˆ (๐น supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐นโ€˜๐‘‹) โ‰  โˆ…)))
4743, 3, 45, 46syl3anc 1371 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐น supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐นโ€˜๐‘‹) โ‰  โˆ…)))
486, 35, 47mpbir2and 711 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ (๐น supp โˆ…))
4931, 48ffvelcdmd 7084 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚)
50 elssuni 4940 . . . . . . . . . . 11 ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚)
5149, 50syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚)
524oicl 9520 . . . . . . . . . . . 12 Ord dom ๐‘‚
53 ordelon 6385 . . . . . . . . . . . 12 ((Ord dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚) โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On)
5452, 49, 53sylancr 587 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On)
55 nnon 7857 . . . . . . . . . . . 12 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ โˆช dom ๐‘‚ โˆˆ On)
5620, 55syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ On)
57 ontri1 6395 . . . . . . . . . . 11 (((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On โˆง โˆช dom ๐‘‚ โˆˆ On) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹)))
5854, 56, 57syl2anc 584 . . . . . . . . . 10 (๐œ‘ โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹)))
5951, 58mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹))
60 sucidg 6442 . . . . . . . . . . . . . 14 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚)
6120, 60syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚)
6261, 14eleqtrrd 2836 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ dom ๐‘‚)
63 isorel 7319 . . . . . . . . . . . 12 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)) โˆง (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚)) โ†’ (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
6426, 62, 49, 63syl12anc 835 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
65 fvex 6901 . . . . . . . . . . . 12 (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ V
6665epeli 5581 . . . . . . . . . . 11 (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹))
67 fvex 6901 . . . . . . . . . . . 12 (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โˆˆ V
6867epeli 5581 . . . . . . . . . . 11 ((๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)))
6964, 66, 683bitr3g 312 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
70 f1ocnvfv2 7271 . . . . . . . . . . . 12 ((๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โˆง ๐‘‹ โˆˆ (๐น supp โˆ…)) โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) = ๐‘‹)
7128, 48, 70syl2anc 584 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) = ๐‘‹)
7271eleq2d 2819 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
7369, 72bitrd 278 . . . . . . . . 9 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
7459, 73mtbid 323 . . . . . . . 8 (๐œ‘ โ†’ ยฌ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹)
758sseld 3980 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…) โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
76 suppssdm 8158 . . . . . . . . . . . . . . . 16 (๐น supp โˆ…) โŠ† dom ๐น
7776, 42fssdm 6734 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ๐ต)
78 onss 7768 . . . . . . . . . . . . . . . 16 (๐ต โˆˆ On โ†’ ๐ต โŠ† On)
793, 78syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ต โŠ† On)
8077, 79sstrd 3991 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† On)
814oif 9521 . . . . . . . . . . . . . . . 16 ๐‘‚:dom ๐‘‚โŸถ(๐น supp โˆ…)
8281ffvelcdmi 7082 . . . . . . . . . . . . . . 15 (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐น supp โˆ…))
8362, 82syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐น supp โˆ…))
8480, 83sseldd 3982 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On)
85 eloni 6371 . . . . . . . . . . . . 13 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On โ†’ Ord (๐‘‚โ€˜โˆช dom ๐‘‚))
8684, 85syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ Ord (๐‘‚โ€˜โˆช dom ๐‘‚))
87 ordn2lp 6381 . . . . . . . . . . . 12 (Ord (๐‘‚โ€˜โˆช dom ๐‘‚) โ†’ ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆง ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
8886, 87syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆง ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
89 imnan 400 . . . . . . . . . . 11 (((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)) โ†” ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆง ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
9088, 89sylibr 233 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
9175, 90syld 47 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…) โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
92 onelon 6386 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘‹ โˆˆ ๐ต) โ†’ ๐‘‹ โˆˆ On)
933, 6, 92syl2anc 584 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ On)
94 eloni 6371 . . . . . . . . . . . 12 (๐‘‹ โˆˆ On โ†’ Ord ๐‘‹)
9593, 94syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ Ord ๐‘‹)
96 ordirr 6379 . . . . . . . . . . 11 (Ord ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹)
9795, 96syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹)
98 elsni 4644 . . . . . . . . . . . 12 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹} โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹)
9998eleq2d 2819 . . . . . . . . . . 11 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹} โ†’ (๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚) โ†” ๐‘‹ โˆˆ ๐‘‹))
10099notbid 317 . . . . . . . . . 10 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹} โ†’ (ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚) โ†” ยฌ ๐‘‹ โˆˆ ๐‘‹))
10197, 100syl5ibrcom 246 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹} โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
102 eqeq1 2736 . . . . . . . . . . . . . . 15 (๐‘ก = ๐‘˜ โ†’ (๐‘ก = ๐‘‹ โ†” ๐‘˜ = ๐‘‹))
103 fveq2 6888 . . . . . . . . . . . . . . 15 (๐‘ก = ๐‘˜ โ†’ (๐บโ€˜๐‘ก) = (๐บโ€˜๐‘˜))
104102, 103ifbieq2d 4553 . . . . . . . . . . . . . 14 (๐‘ก = ๐‘˜ โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)))
105 eldifi 4125 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โ†’ ๐‘˜ โˆˆ ๐ต)
106105adantl 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ๐‘˜ โˆˆ ๐ต)
1077adantr 481 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ๐‘Œ โˆˆ ๐ด)
108 fvex 6901 . . . . . . . . . . . . . . 15 (๐บโ€˜๐‘˜) โˆˆ V
109 ifexg 4576 . . . . . . . . . . . . . . 15 ((๐‘Œ โˆˆ ๐ด โˆง (๐บโ€˜๐‘˜) โˆˆ V) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) โˆˆ V)
110107, 108, 109sylancl 586 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) โˆˆ V)
1119, 104, 106, 110fvmptd3 7018 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)))
112 eldifn 4126 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โ†’ ยฌ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
113112adantl 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ยฌ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
114 velsn 4643 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ {๐‘‹} โ†” ๐‘˜ = ๐‘‹)
115 elun2 4176 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ {๐‘‹} โ†’ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
116114, 115sylbir 234 . . . . . . . . . . . . . . 15 (๐‘˜ = ๐‘‹ โ†’ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
117113, 116nsyl 140 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ยฌ ๐‘˜ = ๐‘‹)
118117iffalsed 4538 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = (๐บโ€˜๐‘˜))
119 ssun1 4171 . . . . . . . . . . . . . . . 16 (๐บ supp โˆ…) โŠ† ((๐บ supp โˆ…) โˆช {๐‘‹})
120 sscon 4137 . . . . . . . . . . . . . . . 16 ((๐บ supp โˆ…) โŠ† ((๐บ supp โˆ…) โˆช {๐‘‹}) โ†’ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โŠ† (๐ต โˆ– (๐บ supp โˆ…)))
121119, 120ax-mp 5 . . . . . . . . . . . . . . 15 (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โŠ† (๐ต โˆ– (๐บ supp โˆ…))
122121sseli 3977 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โ†’ ๐‘˜ โˆˆ (๐ต โˆ– (๐บ supp โˆ…)))
123 ssidd 4004 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† (๐บ supp โˆ…))
12439, 123, 3, 13suppssr 8177 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐บ supp โˆ…))) โ†’ (๐บโ€˜๐‘˜) = โˆ…)
125122, 124sylan2 593 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ (๐บโ€˜๐‘˜) = โˆ…)
126111, 118, 1253eqtrd 2776 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ (๐นโ€˜๐‘˜) = โˆ…)
12742, 126suppss 8175 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ((๐บ supp โˆ…) โˆช {๐‘‹}))
128127, 83sseldd 3982 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
129 elun 4147 . . . . . . . . . 10 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}) โ†” ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…) โˆจ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹}))
130128, 129sylib 217 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…) โˆจ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹}))
13191, 101, 130mpjaod 858 . . . . . . . 8 (๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚))
132 ioran 982 . . . . . . . 8 (ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)) โ†” (ยฌ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆง ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
13374, 131, 132sylanbrc 583 . . . . . . 7 (๐œ‘ โ†’ ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
134 ordtri3 6397 . . . . . . . 8 ((Ord (๐‘‚โ€˜โˆช dom ๐‘‚) โˆง Ord ๐‘‹) โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹ โ†” ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚))))
13586, 95, 134syl2anc 584 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹ โ†” ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚))))
136133, 135mpbird 256 . . . . . 6 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹)
137136oveq2d 7421 . . . . 5 (๐œ‘ โ†’ (๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) = (๐ด โ†‘o ๐‘‹))
138136fveq2d 6892 . . . . . 6 (๐œ‘ โ†’ (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚)) = (๐นโ€˜๐‘‹))
139138, 33eqtrd 2772 . . . . 5 (๐œ‘ โ†’ (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚)) = ๐‘Œ)
140137, 139oveq12d 7423 . . . 4 (๐œ‘ โ†’ ((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) = ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ))
141 nnord 7859 . . . . . . . . 9 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ Ord โˆช dom ๐‘‚)
14220, 141syl 17 . . . . . . . 8 (๐œ‘ โ†’ Ord โˆช dom ๐‘‚)
143 sssucid 6441 . . . . . . . . . 10 โˆช dom ๐‘‚ โŠ† suc โˆช dom ๐‘‚
144143, 14sseqtrrid 4034 . . . . . . . . 9 (๐œ‘ โ†’ โˆช dom ๐‘‚ โŠ† dom ๐‘‚)
145 f1ofo 6837 . . . . . . . . . . . . 13 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ ๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…))
14628, 145syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…))
147 foima 6807 . . . . . . . . . . . 12 (๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…) โ†’ (๐‘‚ โ€œ dom ๐‘‚) = (๐น supp โˆ…))
148146, 147syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ dom ๐‘‚) = (๐น supp โˆ…))
149 ffn 6714 . . . . . . . . . . . . . 14 (๐‘‚:dom ๐‘‚โŸถ(๐น supp โˆ…) โ†’ ๐‘‚ Fn dom ๐‘‚)
15081, 149ax-mp 5 . . . . . . . . . . . . 13 ๐‘‚ Fn dom ๐‘‚
151 fnsnfv 6967 . . . . . . . . . . . . 13 ((๐‘‚ Fn dom ๐‘‚ โˆง โˆช dom ๐‘‚ โˆˆ dom ๐‘‚) โ†’ {(๐‘‚โ€˜โˆช dom ๐‘‚)} = (๐‘‚ โ€œ {โˆช dom ๐‘‚}))
152150, 62, 151sylancr 587 . . . . . . . . . . . 12 (๐œ‘ โ†’ {(๐‘‚โ€˜โˆช dom ๐‘‚)} = (๐‘‚ โ€œ {โˆช dom ๐‘‚}))
153136sneqd 4639 . . . . . . . . . . . 12 (๐œ‘ โ†’ {(๐‘‚โ€˜โˆช dom ๐‘‚)} = {๐‘‹})
154152, 153eqtr3d 2774 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ {โˆช dom ๐‘‚}) = {๐‘‹})
155148, 154difeq12d 4122 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})) = ((๐น supp โˆ…) โˆ– {๐‘‹}))
156 ordirr 6379 . . . . . . . . . . . . . . . . 17 (Ord โˆช dom ๐‘‚ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚)
157142, 156syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚)
158 disjsn 4714 . . . . . . . . . . . . . . . 16 ((โˆช dom ๐‘‚ โˆฉ {โˆช dom ๐‘‚}) = โˆ… โ†” ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚)
159157, 158sylibr 233 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆฉ {โˆช dom ๐‘‚}) = โˆ…)
160 disj3 4452 . . . . . . . . . . . . . . 15 ((โˆช dom ๐‘‚ โˆฉ {โˆช dom ๐‘‚}) = โˆ… โ†” โˆช dom ๐‘‚ = (โˆช dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}))
161159, 160sylib 217 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆช dom ๐‘‚ = (โˆช dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}))
162 difun2 4479 . . . . . . . . . . . . . 14 ((โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}) โˆ– {โˆช dom ๐‘‚}) = (โˆช dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})
163161, 162eqtr4di 2790 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆช dom ๐‘‚ = ((โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}) โˆ– {โˆช dom ๐‘‚}))
164 df-suc 6367 . . . . . . . . . . . . . . 15 suc โˆช dom ๐‘‚ = (โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚})
16514, 164eqtrdi 2788 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ dom ๐‘‚ = (โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}))
166165difeq1d 4120 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}) = ((โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}) โˆ– {โˆช dom ๐‘‚}))
167163, 166eqtr4d 2775 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆช dom ๐‘‚ = (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}))
168167imaeq2d 6057 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ โˆช dom ๐‘‚) = (๐‘‚ โ€œ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})))
169 dff1o3 6836 . . . . . . . . . . . . 13 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†” (๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…) โˆง Fun โ—ก๐‘‚))
170169simprbi 497 . . . . . . . . . . . 12 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ Fun โ—ก๐‘‚)
171 imadif 6629 . . . . . . . . . . . 12 (Fun โ—ก๐‘‚ โ†’ (๐‘‚ โ€œ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})) = ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})))
17228, 170, 1713syl 18 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})) = ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})))
173168, 172eqtrd 2772 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‚ โ€œ โˆช dom ๐‘‚) = ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})))
1748, 97ssneldd 3984 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…))
175 disjsn 4714 . . . . . . . . . . . . 13 (((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ… โ†” ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…))
176174, 175sylibr 233 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ…)
177 fvex 6901 . . . . . . . . . . . . . . . . . . . . 21 (๐บโ€˜๐‘‹) โˆˆ V
178 dif1o 8496 . . . . . . . . . . . . . . . . . . . . 21 ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” ((๐บโ€˜๐‘‹) โˆˆ V โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…))
179177, 178mpbiran 707 . . . . . . . . . . . . . . . . . . . 20 ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” (๐บโ€˜๐‘‹) โ‰  โˆ…)
18039ffnd 6715 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ๐บ Fn ๐ต)
181 elsuppfn 8152 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐บ Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…)))
182180, 3, 45, 181syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…)))
183179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” (๐บโ€˜๐‘‹) โ‰  โˆ…))
184183bicomd 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โ‰  โˆ… โ†” (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o)))
185184anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ((๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o))))
186182, 185bitrd 278 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o))))
1878sseld 3980 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†’ ๐‘‹ โˆˆ ๐‘‹))
188186, 187sylbird 259 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o)) โ†’ ๐‘‹ โˆˆ ๐‘‹))
1896, 188mpand 693 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†’ ๐‘‹ โˆˆ ๐‘‹))
190179, 189biimtrrid 242 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โ‰  โˆ… โ†’ ๐‘‹ โˆˆ ๐‘‹))
191190necon1bd 2958 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (ยฌ ๐‘‹ โˆˆ ๐‘‹ โ†’ (๐บโ€˜๐‘‹) = โˆ…))
19297, 191mpd 15 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บโ€˜๐‘‹) = โˆ…)
193192adantr 481 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐บโ€˜๐‘‹) = โˆ…)
194 fveqeq2 6897 . . . . . . . . . . . . . . . 16 (๐‘˜ = ๐‘‹ โ†’ ((๐บโ€˜๐‘˜) = โˆ… โ†” (๐บโ€˜๐‘‹) = โˆ…))
195193, 194syl5ibrcom 246 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐‘˜ = ๐‘‹ โ†’ (๐บโ€˜๐‘˜) = โˆ…))
196 eldifi 4125 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…)) โ†’ ๐‘˜ โˆˆ ๐ต)
197196adantl 482 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ ๐‘˜ โˆˆ ๐ต)
1987adantr 481 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ ๐‘Œ โˆˆ ๐ด)
199198, 108, 109sylancl 586 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) โˆˆ V)
2009, 104, 197, 199fvmptd3 7018 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)))
201 ssidd 4004 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† (๐น supp โˆ…))
20242, 201, 3, 13suppssr 8177 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐นโ€˜๐‘˜) = โˆ…)
203200, 202eqtr3d 2774 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = โˆ…)
204 iffalse 4536 . . . . . . . . . . . . . . . . 17 (ยฌ ๐‘˜ = ๐‘‹ โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = (๐บโ€˜๐‘˜))
205204eqeq1d 2734 . . . . . . . . . . . . . . . 16 (ยฌ ๐‘˜ = ๐‘‹ โ†’ (if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = โˆ… โ†” (๐บโ€˜๐‘˜) = โˆ…))
206203, 205syl5ibcom 244 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (ยฌ ๐‘˜ = ๐‘‹ โ†’ (๐บโ€˜๐‘˜) = โˆ…))
207195, 206pm2.61d 179 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐บโ€˜๐‘˜) = โˆ…)
20839, 207suppss 8175 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† (๐น supp โˆ…))
209 reldisj 4450 . . . . . . . . . . . . 13 ((๐บ supp โˆ…) โŠ† (๐น supp โˆ…) โ†’ (((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ… โ†” (๐บ supp โˆ…) โŠ† ((๐น supp โˆ…) โˆ– {๐‘‹})))
210208, 209syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ… โ†” (๐บ supp โˆ…) โŠ† ((๐น supp โˆ…) โˆ– {๐‘‹})))
211176, 210mpbid 231 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ((๐น supp โˆ…) โˆ– {๐‘‹}))
212 uncom 4152 . . . . . . . . . . . . 13 ((๐บ supp โˆ…) โˆช {๐‘‹}) = ({๐‘‹} โˆช (๐บ supp โˆ…))
213127, 212sseqtrdi 4031 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ({๐‘‹} โˆช (๐บ supp โˆ…)))
214 ssundif 4486 . . . . . . . . . . . 12 ((๐น supp โˆ…) โŠ† ({๐‘‹} โˆช (๐บ supp โˆ…)) โ†” ((๐น supp โˆ…) โˆ– {๐‘‹}) โŠ† (๐บ supp โˆ…))
215213, 214sylib 217 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐น supp โˆ…) โˆ– {๐‘‹}) โŠ† (๐บ supp โˆ…))
216211, 215eqssd 3998 . . . . . . . . . 10 (๐œ‘ โ†’ (๐บ supp โˆ…) = ((๐น supp โˆ…) โˆ– {๐‘‹}))
217155, 173, 2163eqtr4rd 2783 . . . . . . . . 9 (๐œ‘ โ†’ (๐บ supp โˆ…) = (๐‘‚ โ€œ โˆช dom ๐‘‚))
218 isores3 7328 . . . . . . . . 9 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)) โˆง โˆช dom ๐‘‚ โŠ† dom ๐‘‚ โˆง (๐บ supp โˆ…) = (๐‘‚ โ€œ โˆช dom ๐‘‚)) โ†’ (๐‘‚ โ†พ โˆช dom ๐‘‚) Isom E , E (โˆช dom ๐‘‚, (๐บ supp โˆ…)))
21926, 144, 217, 218syl3anc 1371 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‚ โ†พ โˆช dom ๐‘‚) Isom E , E (โˆช dom ๐‘‚, (๐บ supp โˆ…)))
220 cantnfp1.k . . . . . . . . . . 11 ๐พ = OrdIso( E , (๐บ supp โˆ…))
2211, 2, 3, 220, 5cantnfcl 9658 . . . . . . . . . 10 (๐œ‘ โ†’ ( E We (๐บ supp โˆ…) โˆง dom ๐พ โˆˆ ฯ‰))
222221simpld 495 . . . . . . . . 9 (๐œ‘ โ†’ E We (๐บ supp โˆ…))
223 epse 5658 . . . . . . . . 9 E Se (๐บ supp โˆ…)
224220oieu 9530 . . . . . . . . 9 (( E We (๐บ supp โˆ…) โˆง E Se (๐บ supp โˆ…)) โ†’ ((Ord โˆช dom ๐‘‚ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) Isom E , E (โˆช dom ๐‘‚, (๐บ supp โˆ…))) โ†” (โˆช dom ๐‘‚ = dom ๐พ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) = ๐พ)))
225222, 223, 224sylancl 586 . . . . . . . 8 (๐œ‘ โ†’ ((Ord โˆช dom ๐‘‚ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) Isom E , E (โˆช dom ๐‘‚, (๐บ supp โˆ…))) โ†” (โˆช dom ๐‘‚ = dom ๐พ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) = ๐พ)))
226142, 219, 225mpbi2and 710 . . . . . . 7 (๐œ‘ โ†’ (โˆช dom ๐‘‚ = dom ๐พ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) = ๐พ))
227226simpld 495 . . . . . 6 (๐œ‘ โ†’ โˆช dom ๐‘‚ = dom ๐พ)
228227fveq2d 6892 . . . . 5 (๐œ‘ โ†’ (๐‘€โ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜dom ๐พ))
229 eleq1 2821 . . . . . . . . . 10 (๐‘ฅ = โˆ… โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†” โˆ… โˆˆ dom ๐‘‚))
230 fveq2 6888 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜โˆ…))
231 fveq2 6888 . . . . . . . . . . . 12 (๐‘ฅ = โˆ… โ†’ (๐‘€โ€˜๐‘ฅ) = (๐‘€โ€˜โˆ…))
232 cantnfp1.m . . . . . . . . . . . . . 14 ๐‘€ = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐พโ€˜๐‘˜)) ยทo (๐บโ€˜(๐พโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
233232seqom0g 8452 . . . . . . . . . . . . 13 (โˆ… โˆˆ V โ†’ (๐‘€โ€˜โˆ…) = โˆ…)
23444, 233ax-mp 5 . . . . . . . . . . . 12 (๐‘€โ€˜โˆ…) = โˆ…
235231, 234eqtrdi 2788 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ (๐‘€โ€˜๐‘ฅ) = โˆ…)
236230, 235eqeq12d 2748 . . . . . . . . . 10 (๐‘ฅ = โˆ… โ†’ ((๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ) โ†” (๐ปโ€˜โˆ…) = โˆ…))
237229, 236imbi12d 344 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ ((๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ)) โ†” (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…)))
238237imbi2d 340 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ ((๐œ‘ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ))) โ†” (๐œ‘ โ†’ (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…))))
239 eleq1 2821 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†” ๐‘ฆ โˆˆ dom ๐‘‚))
240 fveq2 6888 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜๐‘ฆ))
241 fveq2 6888 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘€โ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฆ))
242240, 241eqeq12d 2748 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ) โ†” (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ)))
243239, 242imbi12d 344 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ)) โ†” (๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ))))
244243imbi2d 340 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((๐œ‘ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ))) โ†” (๐œ‘ โ†’ (๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ)))))
245 eleq1 2821 . . . . . . . . . 10 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ dom ๐‘‚))
246 fveq2 6888 . . . . . . . . . . 11 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜suc ๐‘ฆ))
247 fveq2 6888 . . . . . . . . . . 11 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐‘€โ€˜๐‘ฅ) = (๐‘€โ€˜suc ๐‘ฆ))
248246, 247eqeq12d 2748 . . . . . . . . . 10 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ) โ†” (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ)))
249245, 248imbi12d 344 . . . . . . . . 9 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ)) โ†” (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ))))
250249imbi2d 340 . . . . . . . 8 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐œ‘ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ))) โ†” (๐œ‘ โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ)))))
251 eleq1 2821 . . . . . . . . . 10 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†” โˆช dom ๐‘‚ โˆˆ dom ๐‘‚))
252 fveq2 6888 . . . . . . . . . . 11 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜โˆช dom ๐‘‚))
253 fveq2 6888 . . . . . . . . . . 11 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ (๐‘€โ€˜๐‘ฅ) = (๐‘€โ€˜โˆช dom ๐‘‚))
254252, 253eqeq12d 2748 . . . . . . . . . 10 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ ((๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ) โ†” (๐ปโ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜โˆช dom ๐‘‚)))
255251, 254imbi12d 344 . . . . . . . . 9 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ ((๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ)) โ†” (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜โˆช dom ๐‘‚))))
256255imbi2d 340 . . . . . . . 8 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ ((๐œ‘ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ))) โ†” (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜โˆช dom ๐‘‚)))))
25711seqom0g 8452 . . . . . . . . 9 (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…)
258257a1i 11 . . . . . . . 8 (๐œ‘ โ†’ (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…))
259 nnord 7859 . . . . . . . . . . . . . . . 16 (dom ๐‘‚ โˆˆ ฯ‰ โ†’ Ord dom ๐‘‚)
26017, 259syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ Ord dom ๐‘‚)
261 ordtr 6375 . . . . . . . . . . . . . . 15 (Ord dom ๐‘‚ โ†’ Tr dom ๐‘‚)
262260, 261syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ Tr dom ๐‘‚)
263 trsuc 6448 . . . . . . . . . . . . . 14 ((Tr dom ๐‘‚ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ dom ๐‘‚)
264262, 263sylan 580 . . . . . . . . . . . . 13 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ dom ๐‘‚)
265264ex 413 . . . . . . . . . . . 12 (๐œ‘ โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ๐‘ฆ โˆˆ dom ๐‘‚))
266265imim1d 82 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ)) โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ))))
267 oveq2 7413 . . . . . . . . . . . . . 14 ((๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ) โ†’ (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
268 elnn 7862 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ dom ๐‘‚ โˆง dom ๐‘‚ โˆˆ ฯ‰) โ†’ ๐‘ฆ โˆˆ ฯ‰)
269268ancoms 459 . . . . . . . . . . . . . . . . 17 ((dom ๐‘‚ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ ฯ‰)
27017, 264, 269syl2an2r 683 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ ฯ‰)
2711, 2, 3, 4, 10, 11cantnfsuc 9661 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐ปโ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)))
272270, 271syldan 591 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐ปโ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)))
2731, 2, 3, 220, 5, 232cantnfsuc 9661 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘€โ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
274270, 273syldan 591 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐‘€โ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
275226simprd 496 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‚ โ†พ โˆช dom ๐‘‚) = ๐พ)
276275fveq1d 6890 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((๐‘‚ โ†พ โˆช dom ๐‘‚)โ€˜๐‘ฆ) = (๐พโ€˜๐‘ฆ))
277276adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐‘‚ โ†พ โˆช dom ๐‘‚)โ€˜๐‘ฆ) = (๐พโ€˜๐‘ฆ))
27814eleq2d 2819 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚))
279278biimpa 477 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚)
280142adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ Ord โˆช dom ๐‘‚)
281 ordsucelsuc 7806 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord โˆช dom ๐‘‚ โ†’ (๐‘ฆ โˆˆ โˆช dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚))
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐‘ฆ โˆˆ โˆช dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚))
283279, 282mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ โˆช dom ๐‘‚)
284283fvresd 6908 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐‘‚ โ†พ โˆช dom ๐‘‚)โ€˜๐‘ฆ) = (๐‘‚โ€˜๐‘ฆ))
285277, 284eqtr3d 2774 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐พโ€˜๐‘ฆ) = (๐‘‚โ€˜๐‘ฆ))
286285oveq2d 7421 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐ด โ†‘o (๐พโ€˜๐‘ฆ)) = (๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)))
287 eqeq1 2736 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐พโ€˜๐‘ฆ) โ†’ (๐‘ก = ๐‘‹ โ†” (๐พโ€˜๐‘ฆ) = ๐‘‹))
288 fveq2 6888 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐พโ€˜๐‘ฆ) โ†’ (๐บโ€˜๐‘ก) = (๐บโ€˜(๐พโ€˜๐‘ฆ)))
289287, 288ifbieq2d 4553 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐พโ€˜๐‘ฆ) โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))))
290 suppssdm 8158 . . . . . . . . . . . . . . . . . . . . . . 23 (๐บ supp โˆ…) โŠ† dom ๐บ
291290, 39fssdm 6734 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
292291adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
293227adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ โˆช dom ๐‘‚ = dom ๐พ)
294283, 293eleqtrd 2835 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ dom ๐พ)
295220oif 9521 . . . . . . . . . . . . . . . . . . . . . . 23 ๐พ:dom ๐พโŸถ(๐บ supp โˆ…)
296295ffvelcdmi 7082 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ dom ๐พ โ†’ (๐พโ€˜๐‘ฆ) โˆˆ (๐บ supp โˆ…))
297294, 296syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐พโ€˜๐‘ฆ) โˆˆ (๐บ supp โˆ…))
298292, 297sseldd 3982 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐พโ€˜๐‘ฆ) โˆˆ ๐ต)
2997adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘Œ โˆˆ ๐ด)
300 fvex 6901 . . . . . . . . . . . . . . . . . . . . 21 (๐บโ€˜(๐พโ€˜๐‘ฆ)) โˆˆ V
301 ifexg 4576 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘Œ โˆˆ ๐ด โˆง (๐บโ€˜(๐พโ€˜๐‘ฆ)) โˆˆ V) โ†’ if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))) โˆˆ V)
302299, 300, 301sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))) โˆˆ V)
3039, 289, 298, 302fvmptd3 7018 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฆ)) = if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))))
304285fveq2d 6892 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฆ)) = (๐นโ€˜(๐‘‚โ€˜๐‘ฆ)))
305174adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…))
306 nelneq 2857 . . . . . . . . . . . . . . . . . . . . 21 (((๐พโ€˜๐‘ฆ) โˆˆ (๐บ supp โˆ…) โˆง ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…)) โ†’ ยฌ (๐พโ€˜๐‘ฆ) = ๐‘‹)
307297, 305, 306syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ยฌ (๐พโ€˜๐‘ฆ) = ๐‘‹)
308307iffalsed 4538 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))) = (๐บโ€˜(๐พโ€˜๐‘ฆ)))
309303, 304, 3083eqtr3rd 2781 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐บโ€˜(๐พโ€˜๐‘ฆ)) = (๐นโ€˜(๐‘‚โ€˜๐‘ฆ)))
310286, 309oveq12d 7423 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) = ((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))))
311310oveq1d 7420 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
312274, 311eqtrd 2772 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐‘€โ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
313272, 312eqeq12d 2748 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ) โ†” (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ))))
314267, 313imbitrrid 245 . . . . . . . . . . . . 13 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ) โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ)))
315314ex 413 . . . . . . . . . . . 12 (๐œ‘ โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ((๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ) โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ))))
316315a2d 29 . . . . . . . . . . 11 (๐œ‘ โ†’ ((suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ)) โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ))))
317266, 316syld 47 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ)) โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ))))
318317a2i 14 . . . . . . . . 9 ((๐œ‘ โ†’ (๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ))) โ†’ (๐œ‘ โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ))))
319318a1i 11 . . . . . . . 8 (๐‘ฆ โˆˆ ฯ‰ โ†’ ((๐œ‘ โ†’ (๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ))) โ†’ (๐œ‘ โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ)))))
320238, 244, 250, 256, 258, 319finds 7885 . . . . . . 7 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜โˆช dom ๐‘‚))))
32120, 320mpcom 38 . . . . . 6 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜โˆช dom ๐‘‚)))
32262, 321mpd 15 . . . . 5 (๐œ‘ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜โˆช dom ๐‘‚))
3231, 2, 3, 220, 5, 232cantnfval 9659 . . . . 5 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = (๐‘€โ€˜dom ๐พ))
324228, 322, 3233eqtr4d 2782 . . . 4 (๐œ‘ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = ((๐ด CNF ๐ต)โ€˜๐บ))
325140, 324oveq12d 7423 . . 3 (๐œ‘ โ†’ (((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) +o (๐ปโ€˜โˆช dom ๐‘‚)) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
32622, 325eqtrd 2772 . 2 (๐œ‘ โ†’ (๐ปโ€˜suc โˆช dom ๐‘‚) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
32712, 15, 3263eqtrd 2776 1 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2940  Vcvv 3474   โˆ– cdif 3944   โˆช cun 3945   โˆฉ cin 3946   โŠ† wss 3947  โˆ…c0 4321  ifcif 4527  {csn 4627  โˆช cuni 4907   class class class wbr 5147   โ†ฆ cmpt 5230  Tr wtr 5264   E cep 5578   Se wse 5628   We wwe 5629  โ—กccnv 5674  dom cdm 5675   โ†พ cres 5677   โ€œ cima 5678  Ord word 6360  Oncon0 6361  suc csuc 6363  Fun wfun 6534   Fn wfn 6535  โŸถwf 6536  โ€“ontoโ†’wfo 6538  โ€“1-1-ontoโ†’wf1o 6539  โ€˜cfv 6540   Isom wiso 6541  (class class class)co 7405   โˆˆ cmpo 7407  ฯ‰com 7851   supp csupp 8142  seqฯ‰cseqom 8443  1oc1o 8455   +o coa 8459   ยทo comu 8460   โ†‘o coe 8461   finSupp cfsupp 9357  OrdIsocoi 9500   CNF ccnf 9652
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 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
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 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 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-seqom 8444  df-1o 8462  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-oi 9501  df-cnf 9653
This theorem is referenced by:  cantnfp1  9672
  Copyright terms: Public domain W3C validator