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

Theorem cantnfp1lem3 9677
Description: Lemma for cantnfp1 9678. (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 9675 . . 3 (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
11 cantnfp1.h . . 3 ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐‘‚โ€˜๐‘˜)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
121, 2, 3, 4, 10, 11cantnfval 9665 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = (๐ปโ€˜dom ๐‘‚))
13 cantnfp1.e . . . 4 (๐œ‘ โ†’ โˆ… โˆˆ ๐‘Œ)
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 9676 . . 3 (๐œ‘ โ†’ dom ๐‘‚ = suc โˆช dom ๐‘‚)
1514fveq2d 6895 . 2 (๐œ‘ โ†’ (๐ปโ€˜dom ๐‘‚) = (๐ปโ€˜suc โˆช dom ๐‘‚))
161, 2, 3, 4, 10cantnfcl 9664 . . . . . . 7 (๐œ‘ โ†’ ( E We (๐น supp โˆ…) โˆง dom ๐‘‚ โˆˆ ฯ‰))
1716simprd 496 . . . . . 6 (๐œ‘ โ†’ dom ๐‘‚ โˆˆ ฯ‰)
1814, 17eqeltrrd 2834 . . . . 5 (๐œ‘ โ†’ suc โˆช dom ๐‘‚ โˆˆ ฯ‰)
19 peano2b 7874 . . . . 5 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†” suc โˆช dom ๐‘‚ โˆˆ ฯ‰)
2018, 19sylibr 233 . . . 4 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ ฯ‰)
211, 2, 3, 4, 10, 11cantnfsuc 9667 . . . 4 ((๐œ‘ โˆง โˆช dom ๐‘‚ โˆˆ ฯ‰) โ†’ (๐ปโ€˜suc โˆช dom ๐‘‚) = (((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) +o (๐ปโ€˜โˆช dom ๐‘‚)))
2220, 21mpdan 685 . . 3 (๐œ‘ โ†’ (๐ปโ€˜suc โˆช dom ๐‘‚) = (((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) +o (๐ปโ€˜โˆช dom ๐‘‚)))
23 ovexd 7446 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐น supp โˆ…) โˆˆ V)
2416simpld 495 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ E We (๐น supp โˆ…))
254oiiso 9534 . . . . . . . . . . . . . . 15 (((๐น supp โˆ…) โˆˆ V โˆง E We (๐น supp โˆ…)) โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)))
2623, 24, 25syl2anc 584 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)))
27 isof1o 7322 . . . . . . . . . . . . . 14 (๐‘‚ Isom E , E (dom ๐‘‚, (๐น supp โˆ…)) โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…))
2826, 27syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…))
29 f1ocnv 6845 . . . . . . . . . . . . 13 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ โ—ก๐‘‚:(๐น supp โˆ…)โ€“1-1-ontoโ†’dom ๐‘‚)
30 f1of 6833 . . . . . . . . . . . . 13 (โ—ก๐‘‚:(๐น supp โˆ…)โ€“1-1-ontoโ†’dom ๐‘‚ โ†’ โ—ก๐‘‚:(๐น supp โˆ…)โŸถdom ๐‘‚)
3128, 29, 303syl 18 . . . . . . . . . . . 12 (๐œ‘ โ†’ โ—ก๐‘‚:(๐น supp โˆ…)โŸถdom ๐‘‚)
32 iftrue 4534 . . . . . . . . . . . . . . 15 (๐‘ก = ๐‘‹ โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = ๐‘Œ)
339, 32, 6, 7fvmptd3 7021 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐นโ€˜๐‘‹) = ๐‘Œ)
3413ne0d 4335 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘Œ โ‰  โˆ…)
3533, 34eqnetrd 3008 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐นโ€˜๐‘‹) โ‰  โˆ…)
367adantr 481 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ก โˆˆ ๐ต) โ†’ ๐‘Œ โˆˆ ๐ด)
371, 2, 3cantnfs 9663 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐บ โˆˆ ๐‘† โ†” (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…)))
385, 37mpbid 231 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…))
3938simpld 495 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ:๐ตโŸถ๐ด)
4039ffvelcdmda 7086 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ก โˆˆ ๐ต) โ†’ (๐บโ€˜๐‘ก) โˆˆ ๐ด)
4136, 40ifcld 4574 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ก โˆˆ ๐ต) โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) โˆˆ ๐ด)
4241, 9fmptd 7115 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐น:๐ตโŸถ๐ด)
4342ffnd 6718 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐น Fn ๐ต)
44 0ex 5307 . . . . . . . . . . . . . . 15 โˆ… โˆˆ V
4544a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆ… โˆˆ V)
46 elsuppfn 8158 . . . . . . . . . . . . . 14 ((๐น Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ (๐‘‹ โˆˆ (๐น supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐นโ€˜๐‘‹) โ‰  โˆ…)))
4743, 3, 45, 46syl3anc 1371 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‹ โˆˆ (๐น supp โˆ…) โ†” (๐‘‹ โˆˆ ๐ต โˆง (๐นโ€˜๐‘‹) โ‰  โˆ…)))
486, 35, 47mpbir2and 711 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ (๐น supp โˆ…))
4931, 48ffvelcdmd 7087 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚)
50 elssuni 4941 . . . . . . . . . . 11 ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚)
5149, 50syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚)
524oicl 9526 . . . . . . . . . . . 12 Ord dom ๐‘‚
53 ordelon 6388 . . . . . . . . . . . 12 ((Ord dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚) โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On)
5452, 49, 53sylancr 587 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On)
55 nnon 7863 . . . . . . . . . . . 12 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ โˆช dom ๐‘‚ โˆˆ On)
5620, 55syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ On)
57 ontri1 6398 . . . . . . . . . . 11 (((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On โˆง โˆช dom ๐‘‚ โˆˆ On) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹)))
5854, 56, 57syl2anc 584 . . . . . . . . . 10 (๐œ‘ โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹)))
5951, 58mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹))
60 sucidg 6445 . . . . . . . . . . . . . 14 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚)
6120, 60syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚)
6261, 14eleqtrrd 2836 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ dom ๐‘‚)
63 isorel 7325 . . . . . . . . . . . 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 6904 . . . . . . . . . . . 12 (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ V
6665epeli 5582 . . . . . . . . . . 11 (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹))
67 fvex 6904 . . . . . . . . . . . 12 (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โˆˆ V
6867epeli 5582 . . . . . . . . . . 11 ((๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)))
6964, 66, 683bitr3g 312 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
70 f1ocnvfv2 7277 . . . . . . . . . . . 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 3981 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…) โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
76 suppssdm 8164 . . . . . . . . . . . . . . . 16 (๐น supp โˆ…) โŠ† dom ๐น
7776, 42fssdm 6737 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ๐ต)
78 onss 7774 . . . . . . . . . . . . . . . 16 (๐ต โˆˆ On โ†’ ๐ต โŠ† On)
793, 78syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ต โŠ† On)
8077, 79sstrd 3992 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† On)
814oif 9527 . . . . . . . . . . . . . . . 16 ๐‘‚:dom ๐‘‚โŸถ(๐น supp โˆ…)
8281ffvelcdmi 7085 . . . . . . . . . . . . . . 15 (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐น supp โˆ…))
8362, 82syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐น supp โˆ…))
8480, 83sseldd 3983 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On)
85 eloni 6374 . . . . . . . . . . . . 13 ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On โ†’ Ord (๐‘‚โ€˜โˆช dom ๐‘‚))
8684, 85syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ Ord (๐‘‚โ€˜โˆช dom ๐‘‚))
87 ordn2lp 6384 . . . . . . . . . . . 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 6389 . . . . . . . . . . . . 13 ((๐ต โˆˆ On โˆง ๐‘‹ โˆˆ ๐ต) โ†’ ๐‘‹ โˆˆ On)
933, 6, 92syl2anc 584 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‹ โˆˆ On)
94 eloni 6374 . . . . . . . . . . . 12 (๐‘‹ โˆˆ On โ†’ Ord ๐‘‹)
9593, 94syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ Ord ๐‘‹)
96 ordirr 6382 . . . . . . . . . . 11 (Ord ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹)
9795, 96syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹)
98 elsni 4645 . . . . . . . . . . . 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 6891 . . . . . . . . . . . . . . 15 (๐‘ก = ๐‘˜ โ†’ (๐บโ€˜๐‘ก) = (๐บโ€˜๐‘˜))
104102, 103ifbieq2d 4554 . . . . . . . . . . . . . 14 (๐‘ก = ๐‘˜ โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)))
105 eldifi 4126 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โ†’ ๐‘˜ โˆˆ ๐ต)
106105adantl 482 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ๐‘˜ โˆˆ ๐ต)
1077adantr 481 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ๐‘Œ โˆˆ ๐ด)
108 fvex 6904 . . . . . . . . . . . . . . 15 (๐บโ€˜๐‘˜) โˆˆ V
109 ifexg 4577 . . . . . . . . . . . . . . 15 ((๐‘Œ โˆˆ ๐ด โˆง (๐บโ€˜๐‘˜) โˆˆ V) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) โˆˆ V)
110107, 108, 109sylancl 586 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) โˆˆ V)
1119, 104, 106, 110fvmptd3 7021 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)))
112 eldifn 4127 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โ†’ ยฌ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
113112adantl 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ยฌ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
114 velsn 4644 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ {๐‘‹} โ†” ๐‘˜ = ๐‘‹)
115 elun2 4177 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ {๐‘‹} โ†’ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
116114, 115sylbir 234 . . . . . . . . . . . . . . 15 (๐‘˜ = ๐‘‹ โ†’ ๐‘˜ โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
117113, 116nsyl 140 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ ยฌ ๐‘˜ = ๐‘‹)
118117iffalsed 4539 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = (๐บโ€˜๐‘˜))
119 ssun1 4172 . . . . . . . . . . . . . . . 16 (๐บ supp โˆ…) โŠ† ((๐บ supp โˆ…) โˆช {๐‘‹})
120 sscon 4138 . . . . . . . . . . . . . . . 16 ((๐บ supp โˆ…) โŠ† ((๐บ supp โˆ…) โˆช {๐‘‹}) โ†’ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โŠ† (๐ต โˆ– (๐บ supp โˆ…)))
121119, 120ax-mp 5 . . . . . . . . . . . . . . 15 (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โŠ† (๐ต โˆ– (๐บ supp โˆ…))
122121sseli 3978 . . . . . . . . . . . . . 14 (๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹})) โ†’ ๐‘˜ โˆˆ (๐ต โˆ– (๐บ supp โˆ…)))
123 ssidd 4005 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† (๐บ supp โˆ…))
12439, 123, 3, 13suppssr 8183 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐บ supp โˆ…))) โ†’ (๐บโ€˜๐‘˜) = โˆ…)
125122, 124sylan2 593 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ (๐บโ€˜๐‘˜) = โˆ…)
126111, 118, 1253eqtrd 2776 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– ((๐บ supp โˆ…) โˆช {๐‘‹}))) โ†’ (๐นโ€˜๐‘˜) = โˆ…)
12742, 126suppss 8181 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ((๐บ supp โˆ…) โˆช {๐‘‹}))
128127, 83sseldd 3983 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ((๐บ supp โˆ…) โˆช {๐‘‹}))
129 elun 4148 . . . . . . . . . 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 6400 . . . . . . . 8 ((Ord (๐‘‚โ€˜โˆช dom ๐‘‚) โˆง Ord ๐‘‹) โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹ โ†” ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚))))
13586, 95, 134syl2anc 584 . . . . . . 7 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹ โ†” ยฌ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ (๐‘‚โ€˜โˆช dom ๐‘‚))))
136133, 135mpbird 256 . . . . . 6 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) = ๐‘‹)
137136oveq2d 7427 . . . . 5 (๐œ‘ โ†’ (๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) = (๐ด โ†‘o ๐‘‹))
138136fveq2d 6895 . . . . . 6 (๐œ‘ โ†’ (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚)) = (๐นโ€˜๐‘‹))
139138, 33eqtrd 2772 . . . . 5 (๐œ‘ โ†’ (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚)) = ๐‘Œ)
140137, 139oveq12d 7429 . . . 4 (๐œ‘ โ†’ ((๐ด โ†‘o (๐‘‚โ€˜โˆช dom ๐‘‚)) ยทo (๐นโ€˜(๐‘‚โ€˜โˆช dom ๐‘‚))) = ((๐ด โ†‘o ๐‘‹) ยทo ๐‘Œ))
141 nnord 7865 . . . . . . . . 9 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ Ord โˆช dom ๐‘‚)
14220, 141syl 17 . . . . . . . 8 (๐œ‘ โ†’ Ord โˆช dom ๐‘‚)
143 sssucid 6444 . . . . . . . . . 10 โˆช dom ๐‘‚ โŠ† suc โˆช dom ๐‘‚
144143, 14sseqtrrid 4035 . . . . . . . . 9 (๐œ‘ โ†’ โˆช dom ๐‘‚ โŠ† dom ๐‘‚)
145 f1ofo 6840 . . . . . . . . . . . . 13 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ ๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…))
14628, 145syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…))
147 foima 6810 . . . . . . . . . . . 12 (๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…) โ†’ (๐‘‚ โ€œ dom ๐‘‚) = (๐น supp โˆ…))
148146, 147syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ dom ๐‘‚) = (๐น supp โˆ…))
149 ffn 6717 . . . . . . . . . . . . . 14 (๐‘‚:dom ๐‘‚โŸถ(๐น supp โˆ…) โ†’ ๐‘‚ Fn dom ๐‘‚)
15081, 149ax-mp 5 . . . . . . . . . . . . 13 ๐‘‚ Fn dom ๐‘‚
151 fnsnfv 6970 . . . . . . . . . . . . 13 ((๐‘‚ Fn dom ๐‘‚ โˆง โˆช dom ๐‘‚ โˆˆ dom ๐‘‚) โ†’ {(๐‘‚โ€˜โˆช dom ๐‘‚)} = (๐‘‚ โ€œ {โˆช dom ๐‘‚}))
152150, 62, 151sylancr 587 . . . . . . . . . . . 12 (๐œ‘ โ†’ {(๐‘‚โ€˜โˆช dom ๐‘‚)} = (๐‘‚ โ€œ {โˆช dom ๐‘‚}))
153136sneqd 4640 . . . . . . . . . . . 12 (๐œ‘ โ†’ {(๐‘‚โ€˜โˆช dom ๐‘‚)} = {๐‘‹})
154152, 153eqtr3d 2774 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ {โˆช dom ๐‘‚}) = {๐‘‹})
155148, 154difeq12d 4123 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})) = ((๐น supp โˆ…) โˆ– {๐‘‹}))
156 ordirr 6382 . . . . . . . . . . . . . . . . 17 (Ord โˆช dom ๐‘‚ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚)
157142, 156syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚)
158 disjsn 4715 . . . . . . . . . . . . . . . 16 ((โˆช dom ๐‘‚ โˆฉ {โˆช dom ๐‘‚}) = โˆ… โ†” ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚)
159157, 158sylibr 233 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆฉ {โˆช dom ๐‘‚}) = โˆ…)
160 disj3 4453 . . . . . . . . . . . . . . 15 ((โˆช dom ๐‘‚ โˆฉ {โˆช dom ๐‘‚}) = โˆ… โ†” โˆช dom ๐‘‚ = (โˆช dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}))
161159, 160sylib 217 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ โˆช dom ๐‘‚ = (โˆช dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}))
162 difun2 4480 . . . . . . . . . . . . . 14 ((โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}) โˆ– {โˆช dom ๐‘‚}) = (โˆช dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})
163161, 162eqtr4di 2790 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆช dom ๐‘‚ = ((โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}) โˆ– {โˆช dom ๐‘‚}))
164 df-suc 6370 . . . . . . . . . . . . . . 15 suc โˆช dom ๐‘‚ = (โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚})
16514, 164eqtrdi 2788 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ dom ๐‘‚ = (โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}))
166165difeq1d 4121 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}) = ((โˆช dom ๐‘‚ โˆช {โˆช dom ๐‘‚}) โˆ– {โˆช dom ๐‘‚}))
167163, 166eqtr4d 2775 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆช dom ๐‘‚ = (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚}))
168167imaeq2d 6059 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ โˆช dom ๐‘‚) = (๐‘‚ โ€œ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})))
169 dff1o3 6839 . . . . . . . . . . . . 13 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†” (๐‘‚:dom ๐‘‚โ€“ontoโ†’(๐น supp โˆ…) โˆง Fun โ—ก๐‘‚))
170169simprbi 497 . . . . . . . . . . . 12 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐น supp โˆ…) โ†’ Fun โ—ก๐‘‚)
171 imadif 6632 . . . . . . . . . . . 12 (Fun โ—ก๐‘‚ โ†’ (๐‘‚ โ€œ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})) = ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})))
17228, 170, 1713syl 18 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚ โ€œ (dom ๐‘‚ โˆ– {โˆช dom ๐‘‚})) = ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})))
173168, 172eqtrd 2772 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘‚ โ€œ โˆช dom ๐‘‚) = ((๐‘‚ โ€œ dom ๐‘‚) โˆ– (๐‘‚ โ€œ {โˆช dom ๐‘‚})))
1748, 97ssneldd 3985 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…))
175 disjsn 4715 . . . . . . . . . . . . 13 (((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ… โ†” ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…))
176174, 175sylibr 233 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ…)
177 fvex 6904 . . . . . . . . . . . . . . . . . . . . 21 (๐บโ€˜๐‘‹) โˆˆ V
178 dif1o 8502 . . . . . . . . . . . . . . . . . . . . 21 ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” ((๐บโ€˜๐‘‹) โˆˆ V โˆง (๐บโ€˜๐‘‹) โ‰  โˆ…))
179177, 178mpbiran 707 . . . . . . . . . . . . . . . . . . . 20 ((๐บโ€˜๐‘‹) โˆˆ (V โˆ– 1o) โ†” (๐บโ€˜๐‘‹) โ‰  โˆ…)
18039ffnd 6718 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ๐บ Fn ๐ต)
181 elsuppfn 8158 . . . . . . . . . . . . . . . . . . . . . . . 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 3981 . . . . . . . . . . . . . . . . . . . . . 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 6900 . . . . . . . . . . . . . . . 16 (๐‘˜ = ๐‘‹ โ†’ ((๐บโ€˜๐‘˜) = โˆ… โ†” (๐บโ€˜๐‘‹) = โˆ…))
195193, 194syl5ibrcom 246 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐‘˜ = ๐‘‹ โ†’ (๐บโ€˜๐‘˜) = โˆ…))
196 eldifi 4126 . . . . . . . . . . . . . . . . . . 19 (๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…)) โ†’ ๐‘˜ โˆˆ ๐ต)
197196adantl 482 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ ๐‘˜ โˆˆ ๐ต)
1987adantr 481 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ ๐‘Œ โˆˆ ๐ด)
199198, 108, 109sylancl 586 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) โˆˆ V)
2009, 104, 197, 199fvmptd3 7021 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)))
201 ssidd 4005 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† (๐น supp โˆ…))
20242, 201, 3, 13suppssr 8183 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐นโ€˜๐‘˜) = โˆ…)
203200, 202eqtr3d 2774 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = โˆ…)
204 iffalse 4537 . . . . . . . . . . . . . . . . 17 (ยฌ ๐‘˜ = ๐‘‹ โ†’ if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = (๐บโ€˜๐‘˜))
205204eqeq1d 2734 . . . . . . . . . . . . . . . 16 (ยฌ ๐‘˜ = ๐‘‹ โ†’ (if(๐‘˜ = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘˜)) = โˆ… โ†” (๐บโ€˜๐‘˜) = โˆ…))
206203, 205syl5ibcom 244 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (ยฌ ๐‘˜ = ๐‘‹ โ†’ (๐บโ€˜๐‘˜) = โˆ…))
207195, 206pm2.61d 179 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐บโ€˜๐‘˜) = โˆ…)
20839, 207suppss 8181 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† (๐น supp โˆ…))
209 reldisj 4451 . . . . . . . . . . . . 13 ((๐บ supp โˆ…) โŠ† (๐น supp โˆ…) โ†’ (((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ… โ†” (๐บ supp โˆ…) โŠ† ((๐น supp โˆ…) โˆ– {๐‘‹})))
210208, 209syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐บ supp โˆ…) โˆฉ {๐‘‹}) = โˆ… โ†” (๐บ supp โˆ…) โŠ† ((๐น supp โˆ…) โˆ– {๐‘‹})))
211176, 210mpbid 231 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ((๐น supp โˆ…) โˆ– {๐‘‹}))
212 uncom 4153 . . . . . . . . . . . . 13 ((๐บ supp โˆ…) โˆช {๐‘‹}) = ({๐‘‹} โˆช (๐บ supp โˆ…))
213127, 212sseqtrdi 4032 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† ({๐‘‹} โˆช (๐บ supp โˆ…)))
214 ssundif 4487 . . . . . . . . . . . 12 ((๐น supp โˆ…) โŠ† ({๐‘‹} โˆช (๐บ supp โˆ…)) โ†” ((๐น supp โˆ…) โˆ– {๐‘‹}) โŠ† (๐บ supp โˆ…))
215213, 214sylib 217 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐น supp โˆ…) โˆ– {๐‘‹}) โŠ† (๐บ supp โˆ…))
216211, 215eqssd 3999 . . . . . . . . . 10 (๐œ‘ โ†’ (๐บ supp โˆ…) = ((๐น supp โˆ…) โˆ– {๐‘‹}))
217155, 173, 2163eqtr4rd 2783 . . . . . . . . 9 (๐œ‘ โ†’ (๐บ supp โˆ…) = (๐‘‚ โ€œ โˆช dom ๐‘‚))
218 isores3 7334 . . . . . . . . 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 9664 . . . . . . . . . 10 (๐œ‘ โ†’ ( E We (๐บ supp โˆ…) โˆง dom ๐พ โˆˆ ฯ‰))
222221simpld 495 . . . . . . . . 9 (๐œ‘ โ†’ E We (๐บ supp โˆ…))
223 epse 5659 . . . . . . . . 9 E Se (๐บ supp โˆ…)
224220oieu 9536 . . . . . . . . 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 6895 . . . . 5 (๐œ‘ โ†’ (๐‘€โ€˜โˆช dom ๐‘‚) = (๐‘€โ€˜dom ๐พ))
229 eleq1 2821 . . . . . . . . . 10 (๐‘ฅ = โˆ… โ†’ (๐‘ฅ โˆˆ dom ๐‘‚ โ†” โˆ… โˆˆ dom ๐‘‚))
230 fveq2 6891 . . . . . . . . . . 11 (๐‘ฅ = โˆ… โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜โˆ…))
231 fveq2 6891 . . . . . . . . . . . 12 (๐‘ฅ = โˆ… โ†’ (๐‘€โ€˜๐‘ฅ) = (๐‘€โ€˜โˆ…))
232 cantnfp1.m . . . . . . . . . . . . . 14 ๐‘€ = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐พโ€˜๐‘˜)) ยทo (๐บโ€˜(๐พโ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
233232seqom0g 8458 . . . . . . . . . . . . 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 6891 . . . . . . . . . . 11 (๐‘ฅ = ๐‘ฆ โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜๐‘ฆ))
241 fveq2 6891 . . . . . . . . . . 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 6891 . . . . . . . . . . 11 (๐‘ฅ = suc ๐‘ฆ โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜suc ๐‘ฆ))
247 fveq2 6891 . . . . . . . . . . 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 6891 . . . . . . . . . . 11 (๐‘ฅ = โˆช dom ๐‘‚ โ†’ (๐ปโ€˜๐‘ฅ) = (๐ปโ€˜โˆช dom ๐‘‚))
253 fveq2 6891 . . . . . . . . . . 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 8458 . . . . . . . . 9 (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…)
258257a1i 11 . . . . . . . 8 (๐œ‘ โ†’ (โˆ… โˆˆ dom ๐‘‚ โ†’ (๐ปโ€˜โˆ…) = โˆ…))
259 nnord 7865 . . . . . . . . . . . . . . . 16 (dom ๐‘‚ โˆˆ ฯ‰ โ†’ Ord dom ๐‘‚)
26017, 259syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ Ord dom ๐‘‚)
261 ordtr 6378 . . . . . . . . . . . . . . 15 (Ord dom ๐‘‚ โ†’ Tr dom ๐‘‚)
262260, 261syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ Tr dom ๐‘‚)
263 trsuc 6451 . . . . . . . . . . . . . 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 7419 . . . . . . . . . . . . . 14 ((๐ปโ€˜๐‘ฆ) = (๐‘€โ€˜๐‘ฆ) โ†’ (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
268 elnn 7868 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ dom ๐‘‚ โˆง dom ๐‘‚ โˆˆ ฯ‰) โ†’ ๐‘ฆ โˆˆ ฯ‰)
269268ancoms 459 . . . . . . . . . . . . . . . . 17 ((dom ๐‘‚ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ ฯ‰)
27017, 264, 269syl2an2r 683 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ ฯ‰)
2711, 2, 3, 4, 10, 11cantnfsuc 9667 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐ปโ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)))
272270, 271syldan 591 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐ปโ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))) +o (๐ปโ€˜๐‘ฆ)))
2731, 2, 3, 220, 5, 232cantnfsuc 9667 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰) โ†’ (๐‘€โ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
274270, 273syldan 591 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐‘€โ€˜suc ๐‘ฆ) = (((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) +o (๐‘€โ€˜๐‘ฆ)))
275226simprd 496 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘‚ โ†พ โˆช dom ๐‘‚) = ๐พ)
276275fveq1d 6893 . . . . . . . . . . . . . . . . . . . . 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 7812 . . . . . . . . . . . . . . . . . . . . . . 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 6911 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐‘‚ โ†พ โˆช dom ๐‘‚)โ€˜๐‘ฆ) = (๐‘‚โ€˜๐‘ฆ))
285277, 284eqtr3d 2774 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐พโ€˜๐‘ฆ) = (๐‘‚โ€˜๐‘ฆ))
286285oveq2d 7427 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐ด โ†‘o (๐พโ€˜๐‘ฆ)) = (๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)))
287 eqeq1 2736 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐พโ€˜๐‘ฆ) โ†’ (๐‘ก = ๐‘‹ โ†” (๐พโ€˜๐‘ฆ) = ๐‘‹))
288 fveq2 6891 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ก = (๐พโ€˜๐‘ฆ) โ†’ (๐บโ€˜๐‘ก) = (๐บโ€˜(๐พโ€˜๐‘ฆ)))
289287, 288ifbieq2d 4554 . . . . . . . . . . . . . . . . . . . 20 (๐‘ก = (๐พโ€˜๐‘ฆ) โ†’ if(๐‘ก = ๐‘‹, ๐‘Œ, (๐บโ€˜๐‘ก)) = if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))))
290 suppssdm 8164 . . . . . . . . . . . . . . . . . . . . . . 23 (๐บ supp โˆ…) โŠ† dom ๐บ
291290, 39fssdm 6737 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
292291adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
293227adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ โˆช dom ๐‘‚ = dom ๐พ)
294283, 293eleqtrd 2835 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘ฆ โˆˆ dom ๐พ)
295220oif 9527 . . . . . . . . . . . . . . . . . . . . . . 23 ๐พ:dom ๐พโŸถ(๐บ supp โˆ…)
296295ffvelcdmi 7085 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ dom ๐พ โ†’ (๐พโ€˜๐‘ฆ) โˆˆ (๐บ supp โˆ…))
297294, 296syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐พโ€˜๐‘ฆ) โˆˆ (๐บ supp โˆ…))
298292, 297sseldd 3983 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐พโ€˜๐‘ฆ) โˆˆ ๐ต)
2997adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ๐‘Œ โˆˆ ๐ด)
300 fvex 6904 . . . . . . . . . . . . . . . . . . . . 21 (๐บโ€˜(๐พโ€˜๐‘ฆ)) โˆˆ V
301 ifexg 4577 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘Œ โˆˆ ๐ด โˆง (๐บโ€˜(๐พโ€˜๐‘ฆ)) โˆˆ V) โ†’ if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))) โˆˆ V)
302299, 300, 301sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))) โˆˆ V)
3039, 289, 298, 302fvmptd3 7021 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฆ)) = if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))))
304285fveq2d 6895 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฆ)) = (๐นโ€˜(๐‘‚โ€˜๐‘ฆ)))
305174adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…))
306 nelneq 2857 . . . . . . . . . . . . . . . . . . . . 21 (((๐พโ€˜๐‘ฆ) โˆˆ (๐บ supp โˆ…) โˆง ยฌ ๐‘‹ โˆˆ (๐บ supp โˆ…)) โ†’ ยฌ (๐พโ€˜๐‘ฆ) = ๐‘‹)
307297, 305, 306syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ยฌ (๐พโ€˜๐‘ฆ) = ๐‘‹)
308307iffalsed 4539 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ if((๐พโ€˜๐‘ฆ) = ๐‘‹, ๐‘Œ, (๐บโ€˜(๐พโ€˜๐‘ฆ))) = (๐บโ€˜(๐พโ€˜๐‘ฆ)))
309303, 304, 3083eqtr3rd 2781 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ (๐บโ€˜(๐พโ€˜๐‘ฆ)) = (๐นโ€˜(๐‘‚โ€˜๐‘ฆ)))
310286, 309oveq12d 7429 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚) โ†’ ((๐ด โ†‘o (๐พโ€˜๐‘ฆ)) ยทo (๐บโ€˜(๐พโ€˜๐‘ฆ))) = ((๐ด โ†‘o (๐‘‚โ€˜๐‘ฆ)) ยทo (๐นโ€˜(๐‘‚โ€˜๐‘ฆ))))
311310oveq1d 7426 . . . . . . . . . . . . . . . 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 7891 . . . . . . 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 9665 . . . . 5 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = (๐‘€โ€˜dom ๐พ))
324228, 322, 3233eqtr4d 2782 . . . 4 (๐œ‘ โ†’ (๐ปโ€˜โˆช dom ๐‘‚) = ((๐ด CNF ๐ต)โ€˜๐บ))
325140, 324oveq12d 7429 . . 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 3945   โˆช cun 3946   โˆฉ cin 3947   โŠ† wss 3948  โˆ…c0 4322  ifcif 4528  {csn 4628  โˆช cuni 4908   class class class wbr 5148   โ†ฆ cmpt 5231  Tr wtr 5265   E cep 5579   Se wse 5629   We wwe 5630  โ—กccnv 5675  dom cdm 5676   โ†พ cres 5678   โ€œ cima 5679  Ord word 6363  Oncon0 6364  suc csuc 6366  Fun wfun 6537   Fn wfn 6538  โŸถwf 6539  โ€“ontoโ†’wfo 6541  โ€“1-1-ontoโ†’wf1o 6542  โ€˜cfv 6543   Isom wiso 6544  (class class class)co 7411   โˆˆ cmpo 7413  ฯ‰com 7857   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 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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  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-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:  cantnfp1  9678
  Copyright terms: Public domain W3C validator