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

Theorem cantnfp1lem3 9621
Description: Lemma for cantnfp1 9622. (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 9619 . . 3 (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
11 cantnfp1.h . . 3 ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐‘‚โ€˜๐‘˜)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
121, 2, 3, 4, 10, 11cantnfval 9609 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (๐ปโ€˜dom ๐‘‚))
13 cantnfp1.e . . . 4 (๐œ‘ โ†’ โˆ… โˆˆ ๐‘Œ)
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 9620 . . 3 (๐œ‘ โ†’ dom ๐‘‚ = suc โˆช dom ๐‘‚)
1514fveq2d 6847 . 2 (๐œ‘ โ†’ (๐ปโ€˜dom ๐‘‚) = (๐ปโ€˜suc โˆช dom ๐‘‚))
161, 2, 3, 4, 10cantnfcl 9608 . . . . . . 7 (๐œ‘ โ†’ ( E We (๐น supp โˆ…) โˆง dom ๐‘‚ โˆˆ ฯ‰))
1716simprd 497 . . . . . 6 (๐œ‘ โ†’ dom ๐‘‚ โˆˆ ฯ‰)
1814, 17eqeltrrd 2835 . . . . 5 (๐œ‘ โ†’ suc โˆช dom ๐‘‚ โˆˆ ฯ‰)
19 peano2b 7820 . . . . 5 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†” suc โˆช dom ๐‘‚ โˆˆ ฯ‰)
2018, 19sylibr 233 . . . 4 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ ฯ‰)
211, 2, 3, 4, 10, 11cantnfsuc 9611 . . . 4 ((๐œ‘ โˆง โˆช dom ๐‘‚ โˆˆ ฯ‰) โ†’ (๐ปโ€˜suc โˆช dom ๐‘‚) = (((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) +o (๐ปโ€˜โˆช dom ๐‘‚)))
2220, 21mpdan 686 . . 3 (๐œ‘ โ†’ (๐ปโ€˜suc โˆช dom ๐‘‚) = (((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) +o (๐ปโ€˜โˆช dom ๐‘‚)))
23 ovexd 7393 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐น supp โˆ…) โˆˆ V)
2416simpld 496 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ E We (๐น supp โˆ…))
254oiiso 9478 . . . . . . . . . . . . . . 15 (((๐น supp โˆ…) โˆˆ V โˆง E We (๐น supp โˆ…)) โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)))
2623, 24, 25syl2anc 585 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)))
27 isof1o 7269 . . . . . . . . . . . . . 14 (๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)) โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…))
2826, 27syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…))
29 f1ocnv 6797 . . . . . . . . . . . . 13 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ โ—ก๐‘‚:(๐น supp โˆ…)โ€“1-1-ontoโ†’dom ๐‘‚)
30 f1of 6785 . . . . . . . . . . . . 13 (โ—ก๐‘‚:(๐น supp โˆ…)โ€“1-1-ontoโ†’dom ๐‘‚ โ†’ โ—ก๐‘‚:(๐น supp โˆ…)โŸถdom ๐‘‚)
3128, 29, 303syl 18 . . . . . . . . . . . 12 (๐œ‘ โ†’ โ—ก๐‘‚:(๐น supp โˆ…)โŸถdom ๐‘‚)
32 iftrue 4493 . . . . . . . . . . . . . . 15 (๐‘ก = ๐‘‹ โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = ๐‘Œ)
339, 32, 6, 7fvmptd3 6972 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐นโ€˜๐‘‹) = ๐‘Œ)
3413ne0d 4296 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘Œ โ‰  โˆ…)
3533, 34eqnetrd 3008 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐นโ€˜๐‘‹) โ‰  โˆ…)
367adantr 482 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ก โˆˆ ๐ต) โ†’ ๐‘Œ โˆˆ ๐ด)
371, 2, 3cantnfs 9607 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ โˆˆ ๐‘† โ†” (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…)))
385, 37mpbid 231 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…))
3938simpld 496 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ:๐ตโŸถ๐ด)
4039ffvelcdmda 7036 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ก โˆˆ ๐ต) โ†’ (๐บโ€˜๐‘ก) โˆˆ ๐ด)
4136, 40ifcld 4533 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ก โˆˆ ๐ต) โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) โˆˆ ๐ด)
4241, 9fmptd 7063 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐น:๐ตโŸถ๐ด)
4342ffnd 6670 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐น Fn ๐ต)
44 0ex 5265 . . . . . . . . . . . . . . 15 โˆ… โˆˆ V
4544a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ… โˆˆ V)
46 elsuppfn 8103 . . . . . . . . . . . . . 14 ((๐น Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ (๐‘‹ โˆˆ (๐น supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐นโ€˜๐‘‹) โ‰  โˆ…)))
4743, 3, 45, 46syl3anc 1372 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐น supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐นโ€˜๐‘‹) โ‰  โˆ…)))
486, 35, 47mpbir2and 712 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ (๐น supp โˆ…))
4931, 48ffvelcdmd 7037 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚)
50 elssuni 4899 . . . . . . . . . . 11 ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚)
5149, 50syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚)
524oicl 9470 . . . . . . . . . . . 12 Ord dom ๐‘‚
53 ordelon 6342 . . . . . . . . . . . 12 ((Ord dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚) โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On)
5452, 49, 53sylancr 588 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On)
55 nnon 7809 . . . . . . . . . . . 12 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ โˆช dom ๐‘‚ โˆˆ On)
5620, 55syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ On)
57 ontri1 6352 . . . . . . . . . . 11 (((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On โˆง โˆช dom ๐‘‚ โˆˆ On) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹)))
5854, 56, 57syl2anc 585 . . . . . . . . . 10 (๐œ‘ โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹)))
5951, 58mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹))
60 sucidg 6399 . . . . . . . . . . . . . 14 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚)
6120, 60syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚)
6261, 14eleqtrrd 2837 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ dom ๐‘‚)
63 isorel 7272 . . . . . . . . . . . 12 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)) โˆง (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚)) โ†’ (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
6426, 62, 49, 63syl12anc 836 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
65 fvex 6856 . . . . . . . . . . . 12 (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ V
6665epeli 5540 . . . . . . . . . . 11 (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹))
67 fvex 6856 . . . . . . . . . . . 12 (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โˆˆ V
6867epeli 5540 . . . . . . . . . . 11 ((๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)))
6964, 66, 683bitr3g 313 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
70 f1ocnvfv2 7224 . . . . . . . . . . . 12 ((๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โˆง ๐‘‹ โˆˆ (๐น supp โˆ…)) โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) = ๐‘‹)
7128, 48, 70syl2anc 585 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) = ๐‘‹)
7271eleq2d 2820 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
7369, 72bitrd 279 . . . . . . . . 9 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
7459, 73mtbid 324 . . . . . . . 8 (๐œ‘ โ†’ ยฌ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹)
758sseld 3944 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…) โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
76 suppssdm 8109 . . . . . . . . . . . . . . . 16 (๐น supp โˆ…) โŠ† dom ๐น
7776, 42fssdm 6689 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ๐ต)
78 onss 7720 . . . . . . . . . . . . . . . 16 (๐ต โˆˆ On โ†’ ๐ต โŠ† On)
793, 78syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ต โŠ† On)
8077, 79sstrd 3955 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† On)
814oif 9471 . . . . . . . . . . . . . . . 16 ๐‘‚:dom ๐‘‚โŸถ(๐น supp โˆ…)
8281ffvelcdmi 7035 . . . . . . . . . . . . . . 15 (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐น supp โˆ…))
8362, 82syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐น supp โˆ…))
8480, 83sseldd 3946 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On)
85 eloni 6328 . . . . . . . . . . . . 13 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On โ†’ Ord (๐‘‚โ€˜โˆช dom ๐‘‚))
8684, 85syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ Ord (๐‘‚โ€˜โˆช dom ๐‘‚))
87 ordn2lp 6338 . . . . . . . . . . . 12 (Ord (๐‘‚โ€˜โˆช dom ๐‘‚) โ†’ ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆง ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
8886, 87syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆง ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
89 imnan 401 . . . . . . . . . . 11 (((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)) โ†” ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆง ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
9088, 89sylibr 233 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
9175, 90syld 47 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…) โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
92 onelon 6343 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘‹ โˆˆ ๐ต) โ†’ ๐‘‹ โˆˆ On)
933, 6, 92syl2anc 585 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ On)
94 eloni 6328 . . . . . . . . . . . 12 (๐‘‹ โˆˆ On โ†’ Ord ๐‘‹)
9593, 94syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ Ord ๐‘‹)
96 ordirr 6336 . . . . . . . . . . 11 (Ord ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹)
9795, 96syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹)
98 elsni 4604 . . . . . . . . . . . 12 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹} โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹)
9998eleq2d 2820 . . . . . . . . . . 11 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹} โ†’ (๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚) โ†” ๐‘‹ โˆˆ ๐‘‹))
10099notbid 318 . . . . . . . . . 10 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹} โ†’ (ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚) โ†” ยฌ ๐‘‹ โˆˆ ๐‘‹))
10197, 100syl5ibrcom 247 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹} โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
102 eqeq1 2737 . . . . . . . . . . . . . . 15 (๐‘ก = ๐‘˜ โ†’ (๐‘ก = ๐‘‹ โ†” ๐‘˜ = ๐‘‹))
103 fveq2 6843 . . . . . . . . . . . . . . 15 (๐‘ก = ๐‘˜ โ†’ (๐บโ€˜๐‘ก) = (๐บโ€˜๐‘˜))
104102, 103ifbieq2d 4513 . . . . . . . . . . . . . 14 (๐‘ก = ๐‘˜ โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)))
105 eldifi 4087 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โ†’ ๐‘˜ โˆˆ ๐ต)
106105adantl 483 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ๐‘˜ โˆˆ ๐ต)
1077adantr 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ๐‘Œ โˆˆ ๐ด)
108 fvex 6856 . . . . . . . . . . . . . . 15 (๐บโ€˜๐‘˜) โˆˆ V
109 ifexg 4536 . . . . . . . . . . . . . . 15 ((๐‘Œ โˆˆ ๐ด โˆง (๐บโ€˜๐‘˜) โˆˆ V) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) โˆˆ V)
110107, 108, 109sylancl 587 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) โˆˆ V)
1119, 104, 106, 110fvmptd3 6972 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)))
112 eldifn 4088 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โ†’ ยฌ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
113112adantl 483 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ยฌ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
114 velsn 4603 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ {๐‘‹} โ†” ๐‘˜ = ๐‘‹)
115 elun2 4138 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ {๐‘‹} โ†’ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
116114, 115sylbir 234 . . . . . . . . . . . . . . 15 (๐‘˜ = ๐‘‹ โ†’ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
117113, 116nsyl 140 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ยฌ ๐‘˜ = ๐‘‹)
118117iffalsed 4498 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = (๐บโ€˜๐‘˜))
119 ssun1 4133 . . . . . . . . . . . . . . . 16 (๐บ supp โˆ…) โŠ† ((๐บ supp โˆ…) โˆช {๐‘‹})
120 sscon 4099 . . . . . . . . . . . . . . . 16 ((๐บ supp โˆ…) โŠ† ((๐บ supp โˆ…) โˆช {๐‘‹}) โ†’ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โŠ† (๐ต โˆ– (๐บ supp โˆ…)))
121119, 120ax-mp 5 . . . . . . . . . . . . . . 15 (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โŠ† (๐ต โˆ– (๐บ supp โˆ…))
122121sseli 3941 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โ†’ ๐‘˜ โˆˆ (๐ต โˆ– (๐บ supp โˆ…)))
123 ssidd 3968 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† (๐บ supp โˆ…))
12439, 123, 3, 13suppssr 8128 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐บ supp โˆ…))) โ†’ (๐บโ€˜๐‘˜) = โˆ…)
125122, 124sylan2 594 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ (๐บโ€˜๐‘˜) = โˆ…)
126111, 118, 1253eqtrd 2777 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ (๐นโ€˜๐‘˜) = โˆ…)
12742, 126suppss 8126 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ((๐บ supp โˆ…) โˆช {๐‘‹}))
128127, 83sseldd 3946 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
129 elun 4109 . . . . . . . . . 10 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}) โ†” ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…) โˆจ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹}))
130128, 129sylib 217 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…) โˆจ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ {๐‘‹}))
13191, 101, 130mpjaod 859 . . . . . . . 8 (๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚))
132 ioran 983 . . . . . . . 8 (ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)) โ†” (ยฌ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆง ยฌ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
13374, 131, 132sylanbrc 584 . . . . . . 7 (๐œ‘ โ†’ ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚)))
134 ordtri3 6354 . . . . . . . 8 ((Ord (๐‘‚โ€˜โˆช dom ๐‘‚) โˆง Ord ๐‘‹) โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹ โ†” ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚))))
13586, 95, 134syl2anc 585 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹ โ†” ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚))))
136133, 135mpbird 257 . . . . . 6 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹)
137136oveq2d 7374 . . . . 5 (๐œ‘ โ†’ (๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) = (๐ด โ†‘o ๐‘‹))
138136fveq2d 6847 . . . . . 6 (๐œ‘ โ†’ (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚)) = (๐นโ€˜๐‘‹))
139138, 33eqtrd 2773 . . . . 5 (๐œ‘ โ†’ (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚)) = ๐‘Œ)
140137, 139oveq12d 7376 . . . 4 (๐œ‘ โ†’ ((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) = ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ))
141 nnord 7811 . . . . . . . . 9 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ Ord โˆช dom ๐‘‚)
14220, 141syl 17 . . . . . . . 8 (๐œ‘ โ†’ Ord โˆช dom ๐‘‚)
143 sssucid 6398 . . . . . . . . . 10 โˆช dom ๐‘‚ โŠ† suc โˆช dom ๐‘‚
144143, 14sseqtrrid 3998 . . . . . . . . 9 (๐œ‘ โ†’ โˆช dom ๐‘‚ โŠ† dom ๐‘‚)
145 f1ofo 6792 . . . . . . . . . . . . 13 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ ๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…))
14628, 145syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…))
147 foima 6762 . . . . . . . . . . . 12 (๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…) โ†’ (๐‘‚ โ€œ dom ๐‘‚) = (๐น supp โˆ…))
148146, 147syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ dom ๐‘‚) = (๐น supp โˆ…))
149 ffn 6669 . . . . . . . . . . . . . 14 (๐‘‚:dom ๐‘‚โŸถ(๐น supp โˆ…) โ†’ ๐‘‚ Fn dom ๐‘‚)
15081, 149ax-mp 5 . . . . . . . . . . . . 13 ๐‘‚ Fn dom ๐‘‚
151 fnsnfv 6921 . . . . . . . . . . . . 13 ((๐‘‚ Fn dom ๐‘‚ โˆง โˆช dom ๐‘‚ โˆˆ dom ๐‘‚) โ†’ {(๐‘‚โ€˜โˆช dom ๐‘‚)} = (๐‘‚ โ€œ {โˆช dom ๐‘‚}))
152150, 62, 151sylancr 588 . . . . . . . . . . . 12 (๐œ‘ โ†’ {(๐‘‚โ€˜โˆช dom ๐‘‚)} = (๐‘‚ โ€œ {โˆช dom ๐‘‚}))
153136sneqd 4599 . . . . . . . . . . . 12 (๐œ‘ โ†’ {(๐‘‚โ€˜โˆช dom ๐‘‚)} = {๐‘‹})
154152, 153eqtr3d 2775 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ {โˆช dom ๐‘‚}) = {๐‘‹})
155148, 154difeq12d 4084 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})) = ((๐น supp โˆ…) โˆ– {๐‘‹}))
156 ordirr 6336 . . . . . . . . . . . . . . . . 17 (Ord โˆช dom ๐‘‚ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚)
157142, 156syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚)
158 disjsn 4673 . . . . . . . . . . . . . . . 16 ((โˆช dom ๐‘‚ โˆฉ {โˆช dom ๐‘‚}) = โˆ… โ†” ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚)
159157, 158sylibr 233 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆฉ {โˆช dom ๐‘‚}) = โˆ…)
160 disj3 4414 . . . . . . . . . . . . . . 15 ((โˆช dom ๐‘‚ โˆฉ {โˆช dom ๐‘‚}) = โˆ… โ†” โˆช dom ๐‘‚ = (โˆช dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}))
161159, 160sylib 217 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆช dom ๐‘‚ = (โˆช dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}))
162 difun2 4441 . . . . . . . . . . . . . 14 ((โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}) โˆ– {โˆช dom ๐‘‚}) = (โˆช dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})
163161, 162eqtr4di 2791 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆช dom ๐‘‚ = ((โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}) โˆ– {โˆช dom ๐‘‚}))
164 df-suc 6324 . . . . . . . . . . . . . . 15 suc โˆช dom ๐‘‚ = (โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚})
16514, 164eqtrdi 2789 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ dom ๐‘‚ = (โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}))
166165difeq1d 4082 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}) = ((โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}) โˆ– {โˆช dom ๐‘‚}))
167163, 166eqtr4d 2776 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆช dom ๐‘‚ = (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}))
168167imaeq2d 6014 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ โˆช dom ๐‘‚) = (๐‘‚ โ€œ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})))
169 dff1o3 6791 . . . . . . . . . . . . 13 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†” (๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…) โˆง Fun โ—ก๐‘‚))
170169simprbi 498 . . . . . . . . . . . 12 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ Fun โ—ก๐‘‚)
171 imadif 6586 . . . . . . . . . . . 12 (Fun โ—ก๐‘‚ โ†’ (๐‘‚ โ€œ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})) = ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})))
17228, 170, 1713syl 18 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})) = ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})))
173168, 172eqtrd 2773 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‚ โ€œ โˆช dom ๐‘‚) = ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})))
1748, 97ssneldd 3948 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…))
175 disjsn 4673 . . . . . . . . . . . . 13 (((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ… โ†” ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…))
176174, 175sylibr 233 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ…)
177 fvex 6856 . . . . . . . . . . . . . . . . . . . . 21 (๐บโ€˜๐‘‹) โˆˆ V
178 dif1o 8447 . . . . . . . . . . . . . . . . . . . . 21 ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” ((๐บโ€˜๐‘‹) โˆˆ V โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…))
179177, 178mpbiran 708 . . . . . . . . . . . . . . . . . . . 20 ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” (๐บโ€˜๐‘‹) โ‰  โˆ…)
18039ffnd 6670 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ๐บ Fn ๐ต)
181 elsuppfn 8103 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐บ Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…)))
182180, 3, 45, 181syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…)))
183179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” (๐บโ€˜๐‘‹) โ‰  โˆ…))
184183bicomd 222 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โ‰  โˆ… โ†” (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o)))
185184anbi2d 630 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ ((๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o))))
186182, 185bitrd 279 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o))))
1878sseld 3944 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†’ ๐‘‹ โˆˆ ๐‘‹))
188186, 187sylbird 260 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((๐‘‹ โˆˆ ๐ต โˆง (๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o)) โ†’ ๐‘‹ โˆˆ ๐‘‹))
1896, 188mpand 694 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†’ ๐‘‹ โˆˆ ๐‘‹))
190179, 189biimtrrid 242 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐บโ€˜๐‘‹) โ‰  โˆ… โ†’ ๐‘‹ โˆˆ ๐‘‹))
191190necon1bd 2958 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (ยฌ ๐‘‹ โˆˆ ๐‘‹ โ†’ (๐บโ€˜๐‘‹) = โˆ…))
19297, 191mpd 15 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บโ€˜๐‘‹) = โˆ…)
193192adantr 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐บโ€˜๐‘‹) = โˆ…)
194 fveqeq2 6852 . . . . . . . . . . . . . . . 16 (๐‘˜ = ๐‘‹ โ†’ ((๐บโ€˜๐‘˜) = โˆ… โ†” (๐บโ€˜๐‘‹) = โˆ…))
195193, 194syl5ibrcom 247 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐‘˜ = ๐‘‹ โ†’ (๐บโ€˜๐‘˜) = โˆ…))
196 eldifi 4087 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…)) โ†’ ๐‘˜ โˆˆ ๐ต)
197196adantl 483 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ ๐‘˜ โˆˆ ๐ต)
1987adantr 482 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ ๐‘Œ โˆˆ ๐ด)
199198, 108, 109sylancl 587 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) โˆˆ V)
2009, 104, 197, 199fvmptd3 6972 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)))
201 ssidd 3968 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† (๐น supp โˆ…))
20242, 201, 3, 13suppssr 8128 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐นโ€˜๐‘˜) = โˆ…)
203200, 202eqtr3d 2775 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = โˆ…)
204 iffalse 4496 . . . . . . . . . . . . . . . . 17 (ยฌ ๐‘˜ = ๐‘‹ โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = (๐บโ€˜๐‘˜))
205204eqeq1d 2735 . . . . . . . . . . . . . . . 16 (ยฌ ๐‘˜ = ๐‘‹ โ†’ (if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = โˆ… โ†” (๐บโ€˜๐‘˜) = โˆ…))
206203, 205syl5ibcom 244 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (ยฌ ๐‘˜ = ๐‘‹ โ†’ (๐บโ€˜๐‘˜) = โˆ…))
207195, 206pm2.61d 179 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐บโ€˜๐‘˜) = โˆ…)
20839, 207suppss 8126 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† (๐น supp โˆ…))
209 reldisj 4412 . . . . . . . . . . . . 13 ((๐บ supp โˆ…) โŠ† (๐น supp โˆ…) โ†’ (((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ… โ†” (๐บ supp โˆ…) โŠ† ((๐น supp โˆ…) โˆ– {๐‘‹})))
210208, 209syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ… โ†” (๐บ supp โˆ…) โŠ† ((๐น supp โˆ…) โˆ– {๐‘‹})))
211176, 210mpbid 231 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ((๐น supp โˆ…) โˆ– {๐‘‹}))
212 uncom 4114 . . . . . . . . . . . . 13 ((๐บ supp โˆ…) โˆช {๐‘‹}) = ({๐‘‹} โˆช (๐บ supp โˆ…))
213127, 212sseqtrdi 3995 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ({๐‘‹} โˆช (๐บ supp โˆ…)))
214 ssundif 4446 . . . . . . . . . . . 12 ((๐น supp โˆ…) โŠ† ({๐‘‹} โˆช (๐บ supp โˆ…)) โ†” ((๐น supp โˆ…) โˆ– {๐‘‹}) โŠ† (๐บ supp โˆ…))
215213, 214sylib 217 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐น supp โˆ…) โˆ– {๐‘‹}) โŠ† (๐บ supp โˆ…))
216211, 215eqssd 3962 . . . . . . . . . 10 (๐œ‘ โ†’ (๐บ supp โˆ…) = ((๐น supp โˆ…) โˆ– {๐‘‹}))
217155, 173, 2163eqtr4rd 2784 . . . . . . . . 9 (๐œ‘ โ†’ (๐บ supp โˆ…) = (๐‘‚ โ€œ โˆช dom ๐‘‚))
218 isores3 7281 . . . . . . . . 9 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)) โˆง โˆช dom ๐‘‚ โŠ† dom ๐‘‚ โˆง (๐บ supp โˆ…) = (๐‘‚ โ€œ โˆช dom ๐‘‚)) โ†’ (๐‘‚ โ†พ โˆช dom ๐‘‚) Isom E , E (โˆช dom ๐‘‚, (๐บ supp โˆ…)))
21926, 144, 217, 218syl3anc 1372 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‚ โ†พ โˆช dom ๐‘‚) Isom E , E (โˆช dom ๐‘‚, (๐บ supp โˆ…)))
220 cantnfp1.k . . . . . . . . . . 11 ๐พ = OrdIso( E , (๐บ supp โˆ…))
2211, 2, 3, 220, 5cantnfcl 9608 . . . . . . . . . 10 (๐œ‘ โ†’ ( E We (๐บ supp โˆ…) โˆง dom ๐พ โˆˆ ฯ‰))
222221simpld 496 . . . . . . . . 9 (๐œ‘ โ†’ E We (๐บ supp โˆ…))
223 epse 5617 . . . . . . . . 9 E Se (๐บ supp โˆ…)
224220oieu 9480 . . . . . . . . 9 (( E We (๐บ supp โˆ…) โˆง E Se (๐บ supp โˆ…)) โ†’ ((Ord โˆช dom ๐‘‚ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) Isom E , E (โˆช dom ๐‘‚, (๐บ supp โˆ…))) โ†” (โˆช dom ๐‘‚ = dom ๐พ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) = ๐พ)))
225222, 223, 224sylancl 587 . . . . . . . 8 (๐œ‘ โ†’ ((Ord โˆช dom ๐‘‚ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) Isom E , E (โˆช dom ๐‘‚, (๐บ supp โˆ…))) โ†” (โˆช dom ๐‘‚ = dom ๐พ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) = ๐พ)))
226142, 219, 225mpbi2and 711 . . . . . . 7 (๐œ‘ โ†’ (โˆช dom ๐‘‚ = dom ๐พ โˆง (๐‘‚ โ†พ โˆช dom ๐‘‚) = ๐พ))
227226simpld 496 . . . . . 6 (๐œ‘ โ†’ โˆช dom ๐‘‚ = dom ๐พ)
228227fveq2d 6847 . . . . 5 (๐œ‘ โ†’ (๐‘€โ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜dom ๐พ))
229 eleq1 2822 . . . . . . . . . 10 (๐‘ฅ = โˆ… โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†” โˆ… โˆˆ dom ๐‘‚))
230 fveq2 6843 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜โˆ…))
231 fveq2 6843 . . . . . . . . . . . 12 (๐‘ฅ = โˆ… โ†’ (๐‘€โ€˜๐‘ฅ) = (๐‘€โ€˜โˆ…))
232 cantnfp1.m . . . . . . . . . . . . . 14 ๐‘€ = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐พโ€˜๐‘˜)) ยทo (๐บโ€˜(๐พโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
233232seqom0g 8403 . . . . . . . . . . . . 13 (โˆ… โˆˆ V โ†’ (๐‘€โ€˜โˆ…) = โˆ…)
23444, 233ax-mp 5 . . . . . . . . . . . 12 (๐‘€โ€˜โˆ…) = โˆ…
235231, 234eqtrdi 2789 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ (๐‘€โ€˜๐‘ฅ) = โˆ…)
236230, 235eqeq12d 2749 . . . . . . . . . 10 (๐‘ฅ = โˆ… โ†’ ((๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ) โ†” (๐ปโ€˜โˆ…) = โˆ…))
237229, 236imbi12d 345 . . . . . . . . 9 (๐‘ฅ = โˆ… โ†’ ((๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ)) โ†” (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…)))
238237imbi2d 341 . . . . . . . 8 (๐‘ฅ = โˆ… โ†’ ((๐œ‘ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ))) โ†” (๐œ‘ โ†’ (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…))))
239 eleq1 2822 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†” ๐‘ฆ โˆˆ dom ๐‘‚))
240 fveq2 6843 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜๐‘ฆ))
241 fveq2 6843 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘€โ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฆ))
242240, 241eqeq12d 2749 . . . . . . . . . 10 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ) โ†” (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ)))
243239, 242imbi12d 345 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ)) โ†” (๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ))))
244243imbi2d 341 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((๐œ‘ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ))) โ†” (๐œ‘ โ†’ (๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ)))))
245 eleq1 2822 . . . . . . . . . 10 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ dom ๐‘‚))
246 fveq2 6843 . . . . . . . . . . 11 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜suc ๐‘ฆ))
247 fveq2 6843 . . . . . . . . . . 11 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐‘€โ€˜๐‘ฅ) = (๐‘€โ€˜suc ๐‘ฆ))
248246, 247eqeq12d 2749 . . . . . . . . . 10 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ) โ†” (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ)))
249245, 248imbi12d 345 . . . . . . . . 9 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ)) โ†” (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ))))
250249imbi2d 341 . . . . . . . 8 (๐‘ฅ = suc ๐‘ฆ โ†’ ((๐œ‘ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ))) โ†” (๐œ‘ โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ)))))
251 eleq1 2822 . . . . . . . . . 10 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†” โˆช dom ๐‘‚ โˆˆ dom ๐‘‚))
252 fveq2 6843 . . . . . . . . . . 11 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜โˆช dom ๐‘‚))
253 fveq2 6843 . . . . . . . . . . 11 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ (๐‘€โ€˜๐‘ฅ) = (๐‘€โ€˜โˆช dom ๐‘‚))
254252, 253eqeq12d 2749 . . . . . . . . . 10 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ ((๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ) โ†” (๐ปโ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜โˆช dom ๐‘‚)))
255251, 254imbi12d 345 . . . . . . . . 9 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ ((๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ)) โ†” (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜โˆช dom ๐‘‚))))
256255imbi2d 341 . . . . . . . 8 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ ((๐œ‘ โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐‘€โ€˜๐‘ฅ))) โ†” (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜โˆช dom ๐‘‚)))))
25711seqom0g 8403 . . . . . . . . 9 (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…)
258257a1i 11 . . . . . . . 8 (๐œ‘ โ†’ (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…))
259 nnord 7811 . . . . . . . . . . . . . . . 16 (dom ๐‘‚ โˆˆ ฯ‰ โ†’ Ord dom ๐‘‚)
26017, 259syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ Ord dom ๐‘‚)
261 ordtr 6332 . . . . . . . . . . . . . . 15 (Ord dom ๐‘‚ โ†’ Tr dom ๐‘‚)
262260, 261syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ Tr dom ๐‘‚)
263 trsuc 6405 . . . . . . . . . . . . . 14 ((Tr dom ๐‘‚ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ dom ๐‘‚)
264262, 263sylan 581 . . . . . . . . . . . . 13 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ dom ๐‘‚)
265264ex 414 . . . . . . . . . . . 12 (๐œ‘ โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ๐‘ฆ โˆˆ dom ๐‘‚))
266265imim1d 82 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ)) โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ))))
267 oveq2 7366 . . . . . . . . . . . . . 14 ((๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ) โ†’ (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
268 elnn 7814 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ dom ๐‘‚ โˆง dom ๐‘‚ โˆˆ ฯ‰) โ†’ ๐‘ฆ โˆˆ ฯ‰)
269268ancoms 460 . . . . . . . . . . . . . . . . 17 ((dom ๐‘‚ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ ฯ‰)
27017, 264, 269syl2an2r 684 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ ฯ‰)
2711, 2, 3, 4, 10, 11cantnfsuc 9611 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐ปโ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)))
272270, 271syldan 592 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐ปโ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)))
2731, 2, 3, 220, 5, 232cantnfsuc 9611 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘€โ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
274270, 273syldan 592 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐‘€โ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
275226simprd 497 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‚ โ†พ โˆช dom ๐‘‚) = ๐พ)
276275fveq1d 6845 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((๐‘‚ โ†พ โˆช dom ๐‘‚)โ€˜๐‘ฆ) = (๐พโ€˜๐‘ฆ))
277276adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐‘‚ โ†พ โˆช dom ๐‘‚)โ€˜๐‘ฆ) = (๐พโ€˜๐‘ฆ))
27814eleq2d 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ (suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚))
279278biimpa 478 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚)
280142adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ Ord โˆช dom ๐‘‚)
281 ordsucelsuc 7758 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord โˆช dom ๐‘‚ โ†’ (๐‘ฆ โˆˆ โˆช dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚))
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐‘ฆ โˆˆ โˆช dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚))
283279, 282mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ โˆช dom ๐‘‚)
284283fvresd 6863 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐‘‚ โ†พ โˆช dom ๐‘‚)โ€˜๐‘ฆ) = (๐‘‚โ€˜๐‘ฆ))
285277, 284eqtr3d 2775 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐พโ€˜๐‘ฆ) = (๐‘‚โ€˜๐‘ฆ))
286285oveq2d 7374 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐ด โ†‘o (๐พโ€˜๐‘ฆ)) = (๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)))
287 eqeq1 2737 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐พโ€˜๐‘ฆ) โ†’ (๐‘ก = ๐‘‹ โ†” (๐พโ€˜๐‘ฆ) = ๐‘‹))
288 fveq2 6843 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐พโ€˜๐‘ฆ) โ†’ (๐บโ€˜๐‘ก) = (๐บโ€˜(๐พโ€˜๐‘ฆ)))
289287, 288ifbieq2d 4513 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐พโ€˜๐‘ฆ) โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))))
290 suppssdm 8109 . . . . . . . . . . . . . . . . . . . . . . 23 (๐บ supp โˆ…) โŠ† dom ๐บ
291290, 39fssdm 6689 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
292291adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
293227adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ โˆช dom ๐‘‚ = dom ๐พ)
294283, 293eleqtrd 2836 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ dom ๐พ)
295220oif 9471 . . . . . . . . . . . . . . . . . . . . . . 23 ๐พ:dom ๐พโŸถ(๐บ supp โˆ…)
296295ffvelcdmi 7035 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ dom ๐พ โ†’ (๐พโ€˜๐‘ฆ) โˆˆ (๐บ supp โˆ…))
297294, 296syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐พโ€˜๐‘ฆ) โˆˆ (๐บ supp โˆ…))
298292, 297sseldd 3946 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐พโ€˜๐‘ฆ) โˆˆ ๐ต)
2997adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘Œ โˆˆ ๐ด)
300 fvex 6856 . . . . . . . . . . . . . . . . . . . . 21 (๐บโ€˜(๐พโ€˜๐‘ฆ)) โˆˆ V
301 ifexg 4536 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘Œ โˆˆ ๐ด โˆง (๐บโ€˜(๐พโ€˜๐‘ฆ)) โˆˆ V) โ†’ if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))) โˆˆ V)
302299, 300, 301sylancl 587 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))) โˆˆ V)
3039, 289, 298, 302fvmptd3 6972 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฆ)) = if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))))
304285fveq2d 6847 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฆ)) = (๐นโ€˜(๐‘‚โ€˜๐‘ฆ)))
305174adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…))
306 nelneq 2858 . . . . . . . . . . . . . . . . . . . . 21 (((๐พโ€˜๐‘ฆ) โˆˆ (๐บ supp โˆ…) โˆง ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…)) โ†’ ยฌ (๐พโ€˜๐‘ฆ) = ๐‘‹)
307297, 305, 306syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ยฌ (๐พโ€˜๐‘ฆ) = ๐‘‹)
308307iffalsed 4498 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))) = (๐บโ€˜(๐พโ€˜๐‘ฆ)))
309303, 304, 3083eqtr3rd 2782 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐บโ€˜(๐พโ€˜๐‘ฆ)) = (๐นโ€˜(๐‘‚โ€˜๐‘ฆ)))
310286, 309oveq12d 7376 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) = ((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))))
311310oveq1d 7373 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
312274, 311eqtrd 2773 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐‘€โ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
313272, 312eqeq12d 2749 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ) โ†” (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ))))
314267, 313imbitrrid 245 . . . . . . . . . . . . 13 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ) โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐‘€โ€˜suc ๐‘ฆ)))
315314ex 414 . . . . . . . . . . . 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 7836 . . . . . . 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 9609 . . . . 5 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = (๐‘€โ€˜dom ๐พ))
324228, 322, 3233eqtr4d 2783 . . . 4 (๐œ‘ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = ((๐ด CNF ๐ต)โ€˜๐บ))
325140, 324oveq12d 7376 . . 3 (๐œ‘ โ†’ (((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) +o (๐ปโ€˜โˆช dom ๐‘‚)) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
32622, 325eqtrd 2773 . 2 (๐œ‘ โ†’ (๐ปโ€˜suc โˆช dom ๐‘‚) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
32712, 15, 3263eqtrd 2777 1 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ) +o ((๐ด CNF ๐ต)โ€˜๐บ)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  Vcvv 3444   โˆ– cdif 3908   โˆช cun 3909   โˆฉ cin 3910   โŠ† wss 3911  โˆ…c0 4283  ifcif 4487  {csn 4587  โˆช cuni 4866   class class class wbr 5106   โ†ฆ cmpt 5189  Tr wtr 5223   E cep 5537   Se wse 5587   We wwe 5588  โ—กccnv 5633  dom cdm 5634   โ†พ cres 5636   โ€œ cima 5637  Ord word 6317  Oncon0 6318  suc csuc 6320  Fun wfun 6491   Fn wfn 6492  โŸถwf 6493  โ€“ontoโ†’wfo 6495  โ€“1-1-ontoโ†’wf1o 6496  โ€˜cfv 6497   Isom wiso 6498  (class class class)co 7358   โˆˆ cmpo 7360  ฯ‰com 7803   supp csupp 8093  seqฯ‰cseqom 8394  1oc1o 8406   +o coa 8410   ยทo comu 8411   โ†‘o coe 8412   finSupp cfsupp 9308  OrdIsocoi 9450   CNF ccnf 9602
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 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
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 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-seqom 8395  df-1o 8413  df-er 8651  df-map 8770  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-oi 9451  df-cnf 9603
This theorem is referenced by:  cantnfp1  9622
  Copyright terms: Public domain W3C validator