Metamath Proof Explorer


Theorem cantnfp1lem3

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 1-Jul-2019)

Ref Expression
Hypotheses 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 cantnfp1lem3 ( ๐œ‘ โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐น ) = ( ( ( ๐ด โ†‘o ๐‘‹ ) ยทo ๐‘Œ ) +o ( ( ๐ด CNF ๐ต ) โ€˜ ๐บ ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s โŠข ๐‘† = dom ( ๐ด CNF ๐ต )
2 cantnfs.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ On )
3 cantnfs.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ On )
4 cantnfp1.g โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ ๐‘† )
5 cantnfp1.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
6 cantnfp1.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ด )
7 cantnfp1.s โŠข ( ๐œ‘ โ†’ ( ๐บ supp โˆ… ) โŠ† ๐‘‹ )
8 cantnfp1.f โŠข ๐น = ( ๐‘ก โˆˆ ๐ต โ†ฆ if ( ๐‘ก = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘ก ) ) )
9 cantnfp1.e โŠข ( ๐œ‘ โ†’ โˆ… โˆˆ ๐‘Œ )
10 cantnfp1.o โŠข ๐‘‚ = OrdIso ( E , ( ๐น supp โˆ… ) )
11 cantnfp1.h โŠข ๐ป = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘˜ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… )
12 cantnfp1.k โŠข ๐พ = OrdIso ( E , ( ๐บ supp โˆ… ) )
13 cantnfp1.m โŠข ๐‘€ = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( ๐พ โ€˜ ๐‘˜ ) ) ยทo ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… )
14 1 2 3 4 5 6 7 8 cantnfp1lem1 โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ๐‘† )
15 1 2 3 10 14 11 cantnfval โŠข ( ๐œ‘ โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐น ) = ( ๐ป โ€˜ dom ๐‘‚ ) )
16 1 2 3 4 5 6 7 8 9 10 cantnfp1lem2 โŠข ( ๐œ‘ โ†’ dom ๐‘‚ = suc โˆช dom ๐‘‚ )
17 16 fveq2d โŠข ( ๐œ‘ โ†’ ( ๐ป โ€˜ dom ๐‘‚ ) = ( ๐ป โ€˜ suc โˆช dom ๐‘‚ ) )
18 1 2 3 10 14 cantnfcl โŠข ( ๐œ‘ โ†’ ( E We ( ๐น supp โˆ… ) โˆง dom ๐‘‚ โˆˆ ฯ‰ ) )
19 18 simprd โŠข ( ๐œ‘ โ†’ dom ๐‘‚ โˆˆ ฯ‰ )
20 16 19 eqeltrrd โŠข ( ๐œ‘ โ†’ suc โˆช dom ๐‘‚ โˆˆ ฯ‰ )
21 peano2b โŠข ( โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†” suc โˆช dom ๐‘‚ โˆˆ ฯ‰ )
22 20 21 sylibr โŠข ( ๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ ฯ‰ )
23 1 2 3 10 14 11 cantnfsuc โŠข ( ( ๐œ‘ โˆง โˆช dom ๐‘‚ โˆˆ ฯ‰ ) โ†’ ( ๐ป โ€˜ suc โˆช dom ๐‘‚ ) = ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ) +o ( ๐ป โ€˜ โˆช dom ๐‘‚ ) ) )
24 22 23 mpdan โŠข ( ๐œ‘ โ†’ ( ๐ป โ€˜ suc โˆช dom ๐‘‚ ) = ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ) +o ( ๐ป โ€˜ โˆช dom ๐‘‚ ) ) )
25 ovexd โŠข ( ๐œ‘ โ†’ ( ๐น supp โˆ… ) โˆˆ V )
26 18 simpld โŠข ( ๐œ‘ โ†’ E We ( ๐น supp โˆ… ) )
27 10 oiiso โŠข ( ( ( ๐น supp โˆ… ) โˆˆ V โˆง E We ( ๐น supp โˆ… ) ) โ†’ ๐‘‚ Isom E , E ( dom ๐‘‚ , ( ๐น supp โˆ… ) ) )
28 25 26 27 syl2anc โŠข ( ๐œ‘ โ†’ ๐‘‚ Isom E , E ( dom ๐‘‚ , ( ๐น supp โˆ… ) ) )
29 isof1o โŠข ( ๐‘‚ Isom E , E ( dom ๐‘‚ , ( ๐น supp โˆ… ) ) โ†’ ๐‘‚ : dom ๐‘‚ โ€“1-1-ontoโ†’ ( ๐น supp โˆ… ) )
30 28 29 syl โŠข ( ๐œ‘ โ†’ ๐‘‚ : dom ๐‘‚ โ€“1-1-ontoโ†’ ( ๐น supp โˆ… ) )
31 f1ocnv โŠข ( ๐‘‚ : dom ๐‘‚ โ€“1-1-ontoโ†’ ( ๐น supp โˆ… ) โ†’ โ—ก ๐‘‚ : ( ๐น supp โˆ… ) โ€“1-1-ontoโ†’ dom ๐‘‚ )
32 f1of โŠข ( โ—ก ๐‘‚ : ( ๐น supp โˆ… ) โ€“1-1-ontoโ†’ dom ๐‘‚ โ†’ โ—ก ๐‘‚ : ( ๐น supp โˆ… ) โŸถ dom ๐‘‚ )
33 30 31 32 3syl โŠข ( ๐œ‘ โ†’ โ—ก ๐‘‚ : ( ๐น supp โˆ… ) โŸถ dom ๐‘‚ )
34 iftrue โŠข ( ๐‘ก = ๐‘‹ โ†’ if ( ๐‘ก = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘ก ) ) = ๐‘Œ )
35 8 34 5 6 fvmptd3 โŠข ( ๐œ‘ โ†’ ( ๐น โ€˜ ๐‘‹ ) = ๐‘Œ )
36 9 ne0d โŠข ( ๐œ‘ โ†’ ๐‘Œ โ‰  โˆ… )
37 35 36 eqnetrd โŠข ( ๐œ‘ โ†’ ( ๐น โ€˜ ๐‘‹ ) โ‰  โˆ… )
38 6 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ก โˆˆ ๐ต ) โ†’ ๐‘Œ โˆˆ ๐ด )
39 1 2 3 cantnfs โŠข ( ๐œ‘ โ†’ ( ๐บ โˆˆ ๐‘† โ†” ( ๐บ : ๐ต โŸถ ๐ด โˆง ๐บ finSupp โˆ… ) ) )
40 4 39 mpbid โŠข ( ๐œ‘ โ†’ ( ๐บ : ๐ต โŸถ ๐ด โˆง ๐บ finSupp โˆ… ) )
41 40 simpld โŠข ( ๐œ‘ โ†’ ๐บ : ๐ต โŸถ ๐ด )
42 41 ffvelrnda โŠข ( ( ๐œ‘ โˆง ๐‘ก โˆˆ ๐ต ) โ†’ ( ๐บ โ€˜ ๐‘ก ) โˆˆ ๐ด )
43 38 42 ifcld โŠข ( ( ๐œ‘ โˆง ๐‘ก โˆˆ ๐ต ) โ†’ if ( ๐‘ก = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘ก ) ) โˆˆ ๐ด )
44 43 8 fmptd โŠข ( ๐œ‘ โ†’ ๐น : ๐ต โŸถ ๐ด )
45 44 ffnd โŠข ( ๐œ‘ โ†’ ๐น Fn ๐ต )
46 0ex โŠข โˆ… โˆˆ V
47 46 a1i โŠข ( ๐œ‘ โ†’ โˆ… โˆˆ V )
48 elsuppfn โŠข ( ( ๐น Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V ) โ†’ ( ๐‘‹ โˆˆ ( ๐น supp โˆ… ) โ†” ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐น โ€˜ ๐‘‹ ) โ‰  โˆ… ) ) )
49 45 3 47 48 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ ( ๐น supp โˆ… ) โ†” ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐น โ€˜ ๐‘‹ ) โ‰  โˆ… ) ) )
50 5 37 49 mpbir2and โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( ๐น supp โˆ… ) )
51 33 50 ffvelrnd โŠข ( ๐œ‘ โ†’ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โˆˆ dom ๐‘‚ )
52 elssuni โŠข ( ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โˆˆ dom ๐‘‚ โ†’ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โŠ† โˆช dom ๐‘‚ )
53 51 52 syl โŠข ( ๐œ‘ โ†’ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โŠ† โˆช dom ๐‘‚ )
54 10 oicl โŠข Ord dom ๐‘‚
55 ordelon โŠข ( ( Ord dom ๐‘‚ โˆง ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โˆˆ dom ๐‘‚ ) โ†’ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โˆˆ On )
56 54 51 55 sylancr โŠข ( ๐œ‘ โ†’ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โˆˆ On )
57 nnon โŠข ( โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ โˆช dom ๐‘‚ โˆˆ On )
58 22 57 syl โŠข ( ๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ On )
59 ontri1 โŠข ( ( ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โˆˆ On โˆง โˆช dom ๐‘‚ โˆˆ On ) โ†’ ( ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) )
60 56 58 59 syl2anc โŠข ( ๐œ‘ โ†’ ( ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) )
61 53 60 mpbid โŠข ( ๐œ‘ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) )
62 sucidg โŠข ( โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚ )
63 22 62 syl โŠข ( ๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚ )
64 63 16 eleqtrrd โŠข ( ๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ )
65 isorel โŠข ( ( ๐‘‚ Isom E , E ( dom ๐‘‚ , ( ๐น supp โˆ… ) ) โˆง ( โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โˆˆ dom ๐‘‚ ) ) โ†’ ( โˆช dom ๐‘‚ E ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โ†” ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) E ( ๐‘‚ โ€˜ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) ) )
66 28 64 51 65 syl12anc โŠข ( ๐œ‘ โ†’ ( โˆช dom ๐‘‚ E ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โ†” ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) E ( ๐‘‚ โ€˜ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) ) )
67 fvex โŠข ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โˆˆ V
68 67 epeli โŠข ( โˆช dom ๐‘‚ E ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โ†” โˆช dom ๐‘‚ โˆˆ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) )
69 fvex โŠข ( ๐‘‚ โ€˜ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) โˆˆ V
70 69 epeli โŠข ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) E ( ๐‘‚ โ€˜ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) โ†” ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ๐‘‚ โ€˜ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) )
71 66 68 70 3bitr3g โŠข ( ๐œ‘ โ†’ ( โˆช dom ๐‘‚ โˆˆ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โ†” ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ๐‘‚ โ€˜ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) ) )
72 f1ocnvfv2 โŠข ( ( ๐‘‚ : dom ๐‘‚ โ€“1-1-ontoโ†’ ( ๐น supp โˆ… ) โˆง ๐‘‹ โˆˆ ( ๐น supp โˆ… ) ) โ†’ ( ๐‘‚ โ€˜ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) = ๐‘‹ )
73 30 50 72 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€˜ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) = ๐‘‹ )
74 73 eleq2d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ๐‘‚ โ€˜ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) ) โ†” ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ ) )
75 71 74 bitrd โŠข ( ๐œ‘ โ†’ ( โˆช dom ๐‘‚ โˆˆ ( โ—ก ๐‘‚ โ€˜ ๐‘‹ ) โ†” ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ ) )
76 61 75 mtbid โŠข ( ๐œ‘ โ†’ ยฌ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ )
77 7 sseld โŠข ( ๐œ‘ โ†’ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ๐บ supp โˆ… ) โ†’ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ ) )
78 suppssdm โŠข ( ๐น supp โˆ… ) โŠ† dom ๐น
79 78 44 fssdm โŠข ( ๐œ‘ โ†’ ( ๐น supp โˆ… ) โŠ† ๐ต )
80 onss โŠข ( ๐ต โˆˆ On โ†’ ๐ต โŠ† On )
81 3 80 syl โŠข ( ๐œ‘ โ†’ ๐ต โŠ† On )
82 79 81 sstrd โŠข ( ๐œ‘ โ†’ ( ๐น supp โˆ… ) โŠ† On )
83 10 oif โŠข ๐‘‚ : dom ๐‘‚ โŸถ ( ๐น supp โˆ… )
84 83 ffvelrni โŠข ( โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ๐น supp โˆ… ) )
85 64 84 syl โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ๐น supp โˆ… ) )
86 82 85 sseldd โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ On )
87 eloni โŠข ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ On โ†’ Ord ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) )
88 86 87 syl โŠข ( ๐œ‘ โ†’ Ord ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) )
89 ordn2lp โŠข ( Ord ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โ†’ ยฌ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โˆง ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) )
90 88 89 syl โŠข ( ๐œ‘ โ†’ ยฌ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โˆง ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) )
91 imnan โŠข ( ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) โ†” ยฌ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โˆง ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) )
92 90 91 sylibr โŠข ( ๐œ‘ โ†’ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) )
93 77 92 syld โŠข ( ๐œ‘ โ†’ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ๐บ supp โˆ… ) โ†’ ยฌ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) )
94 onelon โŠข ( ( ๐ต โˆˆ On โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ๐‘‹ โˆˆ On )
95 3 5 94 syl2anc โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ On )
96 eloni โŠข ( ๐‘‹ โˆˆ On โ†’ Ord ๐‘‹ )
97 95 96 syl โŠข ( ๐œ‘ โ†’ Ord ๐‘‹ )
98 ordirr โŠข ( Ord ๐‘‹ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹ )
99 97 98 syl โŠข ( ๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ ๐‘‹ )
100 elsni โŠข ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ { ๐‘‹ } โ†’ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) = ๐‘‹ )
101 100 eleq2d โŠข ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ { ๐‘‹ } โ†’ ( ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โ†” ๐‘‹ โˆˆ ๐‘‹ ) )
102 101 notbid โŠข ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ { ๐‘‹ } โ†’ ( ยฌ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โ†” ยฌ ๐‘‹ โˆˆ ๐‘‹ ) )
103 99 102 syl5ibrcom โŠข ( ๐œ‘ โ†’ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ { ๐‘‹ } โ†’ ยฌ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) )
104 eqeq1 โŠข ( ๐‘ก = ๐‘˜ โ†’ ( ๐‘ก = ๐‘‹ โ†” ๐‘˜ = ๐‘‹ ) )
105 fveq2 โŠข ( ๐‘ก = ๐‘˜ โ†’ ( ๐บ โ€˜ ๐‘ก ) = ( ๐บ โ€˜ ๐‘˜ ) )
106 104 105 ifbieq2d โŠข ( ๐‘ก = ๐‘˜ โ†’ if ( ๐‘ก = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘ก ) ) = if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) )
107 eldifi โŠข ( ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) โ†’ ๐‘˜ โˆˆ ๐ต )
108 107 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) ) โ†’ ๐‘˜ โˆˆ ๐ต )
109 6 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) ) โ†’ ๐‘Œ โˆˆ ๐ด )
110 fvex โŠข ( ๐บ โ€˜ ๐‘˜ ) โˆˆ V
111 ifexg โŠข ( ( ๐‘Œ โˆˆ ๐ด โˆง ( ๐บ โ€˜ ๐‘˜ ) โˆˆ V ) โ†’ if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) โˆˆ V )
112 109 110 111 sylancl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) ) โ†’ if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) โˆˆ V )
113 8 106 108 112 fvmptd3 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) ) โ†’ ( ๐น โ€˜ ๐‘˜ ) = if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) )
114 eldifn โŠข ( ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) โ†’ ยฌ ๐‘˜ โˆˆ ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) )
115 114 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) ) โ†’ ยฌ ๐‘˜ โˆˆ ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) )
116 velsn โŠข ( ๐‘˜ โˆˆ { ๐‘‹ } โ†” ๐‘˜ = ๐‘‹ )
117 elun2 โŠข ( ๐‘˜ โˆˆ { ๐‘‹ } โ†’ ๐‘˜ โˆˆ ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) )
118 116 117 sylbir โŠข ( ๐‘˜ = ๐‘‹ โ†’ ๐‘˜ โˆˆ ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) )
119 115 118 nsyl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) ) โ†’ ยฌ ๐‘˜ = ๐‘‹ )
120 119 iffalsed โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) ) โ†’ if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) = ( ๐บ โ€˜ ๐‘˜ ) )
121 ssun1 โŠข ( ๐บ supp โˆ… ) โŠ† ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } )
122 sscon โŠข ( ( ๐บ supp โˆ… ) โŠ† ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) โ†’ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) โŠ† ( ๐ต โˆ– ( ๐บ supp โˆ… ) ) )
123 121 122 ax-mp โŠข ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) โŠ† ( ๐ต โˆ– ( ๐บ supp โˆ… ) )
124 123 sseli โŠข ( ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) โ†’ ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐บ supp โˆ… ) ) )
125 ssidd โŠข ( ๐œ‘ โ†’ ( ๐บ supp โˆ… ) โŠ† ( ๐บ supp โˆ… ) )
126 41 125 3 9 suppssr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐บ supp โˆ… ) ) ) โ†’ ( ๐บ โ€˜ ๐‘˜ ) = โˆ… )
127 124 126 sylan2 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) ) โ†’ ( ๐บ โ€˜ ๐‘˜ ) = โˆ… )
128 113 120 127 3eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) ) ) โ†’ ( ๐น โ€˜ ๐‘˜ ) = โˆ… )
129 44 128 suppss โŠข ( ๐œ‘ โ†’ ( ๐น supp โˆ… ) โŠ† ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) )
130 129 85 sseldd โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) )
131 elun โŠข ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) โ†” ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ๐บ supp โˆ… ) โˆจ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ { ๐‘‹ } ) )
132 130 131 sylib โŠข ( ๐œ‘ โ†’ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ( ๐บ supp โˆ… ) โˆจ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ { ๐‘‹ } ) )
133 93 103 132 mpjaod โŠข ( ๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) )
134 ioran โŠข ( ยฌ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) โ†” ( ยฌ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โˆง ยฌ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) )
135 76 133 134 sylanbrc โŠข ( ๐œ‘ โ†’ ยฌ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) )
136 ordtri3 โŠข ( ( Ord ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆง Ord ๐‘‹ ) โ†’ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) = ๐‘‹ โ†” ยฌ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ) )
137 88 97 136 syl2anc โŠข ( ๐œ‘ โ†’ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) = ๐‘‹ โ†” ยฌ ( ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) โˆˆ ๐‘‹ โˆจ ๐‘‹ โˆˆ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ) )
138 135 137 mpbird โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) = ๐‘‹ )
139 138 oveq2d โŠข ( ๐œ‘ โ†’ ( ๐ด โ†‘o ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) = ( ๐ด โ†‘o ๐‘‹ ) )
140 138 fveq2d โŠข ( ๐œ‘ โ†’ ( ๐น โ€˜ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) = ( ๐น โ€˜ ๐‘‹ ) )
141 140 35 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐น โ€˜ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) = ๐‘Œ )
142 139 141 oveq12d โŠข ( ๐œ‘ โ†’ ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ) = ( ( ๐ด โ†‘o ๐‘‹ ) ยทo ๐‘Œ ) )
143 nnord โŠข ( โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ Ord โˆช dom ๐‘‚ )
144 22 143 syl โŠข ( ๐œ‘ โ†’ Ord โˆช dom ๐‘‚ )
145 sssucid โŠข โˆช dom ๐‘‚ โŠ† suc โˆช dom ๐‘‚
146 145 16 sseqtrrid โŠข ( ๐œ‘ โ†’ โˆช dom ๐‘‚ โŠ† dom ๐‘‚ )
147 f1ofo โŠข ( ๐‘‚ : dom ๐‘‚ โ€“1-1-ontoโ†’ ( ๐น supp โˆ… ) โ†’ ๐‘‚ : dom ๐‘‚ โ€“ontoโ†’ ( ๐น supp โˆ… ) )
148 30 147 syl โŠข ( ๐œ‘ โ†’ ๐‘‚ : dom ๐‘‚ โ€“ontoโ†’ ( ๐น supp โˆ… ) )
149 foima โŠข ( ๐‘‚ : dom ๐‘‚ โ€“ontoโ†’ ( ๐น supp โˆ… ) โ†’ ( ๐‘‚ โ€œ dom ๐‘‚ ) = ( ๐น supp โˆ… ) )
150 148 149 syl โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€œ dom ๐‘‚ ) = ( ๐น supp โˆ… ) )
151 ffn โŠข ( ๐‘‚ : dom ๐‘‚ โŸถ ( ๐น supp โˆ… ) โ†’ ๐‘‚ Fn dom ๐‘‚ )
152 83 151 ax-mp โŠข ๐‘‚ Fn dom ๐‘‚
153 fnsnfv โŠข ( ( ๐‘‚ Fn dom ๐‘‚ โˆง โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ ) โ†’ { ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) } = ( ๐‘‚ โ€œ { โˆช dom ๐‘‚ } ) )
154 152 64 153 sylancr โŠข ( ๐œ‘ โ†’ { ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) } = ( ๐‘‚ โ€œ { โˆช dom ๐‘‚ } ) )
155 138 sneqd โŠข ( ๐œ‘ โ†’ { ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) } = { ๐‘‹ } )
156 154 155 eqtr3d โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€œ { โˆช dom ๐‘‚ } ) = { ๐‘‹ } )
157 150 156 difeq12d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‚ โ€œ dom ๐‘‚ ) โˆ– ( ๐‘‚ โ€œ { โˆช dom ๐‘‚ } ) ) = ( ( ๐น supp โˆ… ) โˆ– { ๐‘‹ } ) )
158 ordirr โŠข ( Ord โˆช dom ๐‘‚ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚ )
159 144 158 syl โŠข ( ๐œ‘ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚ )
160 disjsn โŠข ( ( โˆช dom ๐‘‚ โˆฉ { โˆช dom ๐‘‚ } ) = โˆ… โ†” ยฌ โˆช dom ๐‘‚ โˆˆ โˆช dom ๐‘‚ )
161 159 160 sylibr โŠข ( ๐œ‘ โ†’ ( โˆช dom ๐‘‚ โˆฉ { โˆช dom ๐‘‚ } ) = โˆ… )
162 disj3 โŠข ( ( โˆช dom ๐‘‚ โˆฉ { โˆช dom ๐‘‚ } ) = โˆ… โ†” โˆช dom ๐‘‚ = ( โˆช dom ๐‘‚ โˆ– { โˆช dom ๐‘‚ } ) )
163 161 162 sylib โŠข ( ๐œ‘ โ†’ โˆช dom ๐‘‚ = ( โˆช dom ๐‘‚ โˆ– { โˆช dom ๐‘‚ } ) )
164 difun2 โŠข ( ( โˆช dom ๐‘‚ โˆช { โˆช dom ๐‘‚ } ) โˆ– { โˆช dom ๐‘‚ } ) = ( โˆช dom ๐‘‚ โˆ– { โˆช dom ๐‘‚ } )
165 163 164 eqtr4di โŠข ( ๐œ‘ โ†’ โˆช dom ๐‘‚ = ( ( โˆช dom ๐‘‚ โˆช { โˆช dom ๐‘‚ } ) โˆ– { โˆช dom ๐‘‚ } ) )
166 df-suc โŠข suc โˆช dom ๐‘‚ = ( โˆช dom ๐‘‚ โˆช { โˆช dom ๐‘‚ } )
167 16 166 eqtrdi โŠข ( ๐œ‘ โ†’ dom ๐‘‚ = ( โˆช dom ๐‘‚ โˆช { โˆช dom ๐‘‚ } ) )
168 167 difeq1d โŠข ( ๐œ‘ โ†’ ( dom ๐‘‚ โˆ– { โˆช dom ๐‘‚ } ) = ( ( โˆช dom ๐‘‚ โˆช { โˆช dom ๐‘‚ } ) โˆ– { โˆช dom ๐‘‚ } ) )
169 165 168 eqtr4d โŠข ( ๐œ‘ โ†’ โˆช dom ๐‘‚ = ( dom ๐‘‚ โˆ– { โˆช dom ๐‘‚ } ) )
170 169 imaeq2d โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€œ โˆช dom ๐‘‚ ) = ( ๐‘‚ โ€œ ( dom ๐‘‚ โˆ– { โˆช dom ๐‘‚ } ) ) )
171 dff1o3 โŠข ( ๐‘‚ : dom ๐‘‚ โ€“1-1-ontoโ†’ ( ๐น supp โˆ… ) โ†” ( ๐‘‚ : dom ๐‘‚ โ€“ontoโ†’ ( ๐น supp โˆ… ) โˆง Fun โ—ก ๐‘‚ ) )
172 171 simprbi โŠข ( ๐‘‚ : dom ๐‘‚ โ€“1-1-ontoโ†’ ( ๐น supp โˆ… ) โ†’ Fun โ—ก ๐‘‚ )
173 imadif โŠข ( Fun โ—ก ๐‘‚ โ†’ ( ๐‘‚ โ€œ ( dom ๐‘‚ โˆ– { โˆช dom ๐‘‚ } ) ) = ( ( ๐‘‚ โ€œ dom ๐‘‚ ) โˆ– ( ๐‘‚ โ€œ { โˆช dom ๐‘‚ } ) ) )
174 30 172 173 3syl โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€œ ( dom ๐‘‚ โˆ– { โˆช dom ๐‘‚ } ) ) = ( ( ๐‘‚ โ€œ dom ๐‘‚ ) โˆ– ( ๐‘‚ โ€œ { โˆช dom ๐‘‚ } ) ) )
175 170 174 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ€œ โˆช dom ๐‘‚ ) = ( ( ๐‘‚ โ€œ dom ๐‘‚ ) โˆ– ( ๐‘‚ โ€œ { โˆช dom ๐‘‚ } ) ) )
176 7 99 ssneldd โŠข ( ๐œ‘ โ†’ ยฌ ๐‘‹ โˆˆ ( ๐บ supp โˆ… ) )
177 disjsn โŠข ( ( ( ๐บ supp โˆ… ) โˆฉ { ๐‘‹ } ) = โˆ… โ†” ยฌ ๐‘‹ โˆˆ ( ๐บ supp โˆ… ) )
178 176 177 sylibr โŠข ( ๐œ‘ โ†’ ( ( ๐บ supp โˆ… ) โˆฉ { ๐‘‹ } ) = โˆ… )
179 fvex โŠข ( ๐บ โ€˜ ๐‘‹ ) โˆˆ V
180 dif1o โŠข ( ( ๐บ โ€˜ ๐‘‹ ) โˆˆ ( V โˆ– 1o ) โ†” ( ( ๐บ โ€˜ ๐‘‹ ) โˆˆ V โˆง ( ๐บ โ€˜ ๐‘‹ ) โ‰  โˆ… ) )
181 179 180 mpbiran โŠข ( ( ๐บ โ€˜ ๐‘‹ ) โˆˆ ( V โˆ– 1o ) โ†” ( ๐บ โ€˜ ๐‘‹ ) โ‰  โˆ… )
182 41 ffnd โŠข ( ๐œ‘ โ†’ ๐บ Fn ๐ต )
183 elsuppfn โŠข ( ( ๐บ Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V ) โ†’ ( ๐‘‹ โˆˆ ( ๐บ supp โˆ… ) โ†” ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐บ โ€˜ ๐‘‹ ) โ‰  โˆ… ) ) )
184 182 3 47 183 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ ( ๐บ supp โˆ… ) โ†” ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐บ โ€˜ ๐‘‹ ) โ‰  โˆ… ) ) )
185 181 a1i โŠข ( ๐œ‘ โ†’ ( ( ๐บ โ€˜ ๐‘‹ ) โˆˆ ( V โˆ– 1o ) โ†” ( ๐บ โ€˜ ๐‘‹ ) โ‰  โˆ… ) )
186 185 bicomd โŠข ( ๐œ‘ โ†’ ( ( ๐บ โ€˜ ๐‘‹ ) โ‰  โˆ… โ†” ( ๐บ โ€˜ ๐‘‹ ) โˆˆ ( V โˆ– 1o ) ) )
187 186 anbi2d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐บ โ€˜ ๐‘‹ ) โ‰  โˆ… ) โ†” ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐บ โ€˜ ๐‘‹ ) โˆˆ ( V โˆ– 1o ) ) ) )
188 184 187 bitrd โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ ( ๐บ supp โˆ… ) โ†” ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐บ โ€˜ ๐‘‹ ) โˆˆ ( V โˆ– 1o ) ) ) )
189 7 sseld โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ ( ๐บ supp โˆ… ) โ†’ ๐‘‹ โˆˆ ๐‘‹ ) )
190 188 189 sylbird โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ( ๐บ โ€˜ ๐‘‹ ) โˆˆ ( V โˆ– 1o ) ) โ†’ ๐‘‹ โˆˆ ๐‘‹ ) )
191 5 190 mpand โŠข ( ๐œ‘ โ†’ ( ( ๐บ โ€˜ ๐‘‹ ) โˆˆ ( V โˆ– 1o ) โ†’ ๐‘‹ โˆˆ ๐‘‹ ) )
192 181 191 syl5bir โŠข ( ๐œ‘ โ†’ ( ( ๐บ โ€˜ ๐‘‹ ) โ‰  โˆ… โ†’ ๐‘‹ โˆˆ ๐‘‹ ) )
193 192 necon1bd โŠข ( ๐œ‘ โ†’ ( ยฌ ๐‘‹ โˆˆ ๐‘‹ โ†’ ( ๐บ โ€˜ ๐‘‹ ) = โˆ… ) )
194 99 193 mpd โŠข ( ๐œ‘ โ†’ ( ๐บ โ€˜ ๐‘‹ ) = โˆ… )
195 194 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ ( ๐บ โ€˜ ๐‘‹ ) = โˆ… )
196 fveqeq2 โŠข ( ๐‘˜ = ๐‘‹ โ†’ ( ( ๐บ โ€˜ ๐‘˜ ) = โˆ… โ†” ( ๐บ โ€˜ ๐‘‹ ) = โˆ… ) )
197 195 196 syl5ibrcom โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ ( ๐‘˜ = ๐‘‹ โ†’ ( ๐บ โ€˜ ๐‘˜ ) = โˆ… ) )
198 eldifi โŠข ( ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) โ†’ ๐‘˜ โˆˆ ๐ต )
199 198 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ ๐‘˜ โˆˆ ๐ต )
200 6 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ ๐‘Œ โˆˆ ๐ด )
201 200 110 111 sylancl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) โˆˆ V )
202 8 106 199 201 fvmptd3 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ ( ๐น โ€˜ ๐‘˜ ) = if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) )
203 ssidd โŠข ( ๐œ‘ โ†’ ( ๐น supp โˆ… ) โŠ† ( ๐น supp โˆ… ) )
204 44 203 3 9 suppssr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ ( ๐น โ€˜ ๐‘˜ ) = โˆ… )
205 202 204 eqtr3d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) = โˆ… )
206 iffalse โŠข ( ยฌ ๐‘˜ = ๐‘‹ โ†’ if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) = ( ๐บ โ€˜ ๐‘˜ ) )
207 206 eqeq1d โŠข ( ยฌ ๐‘˜ = ๐‘‹ โ†’ ( if ( ๐‘˜ = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘˜ ) ) = โˆ… โ†” ( ๐บ โ€˜ ๐‘˜ ) = โˆ… ) )
208 205 207 syl5ibcom โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ ( ยฌ ๐‘˜ = ๐‘‹ โ†’ ( ๐บ โ€˜ ๐‘˜ ) = โˆ… ) )
209 197 208 pm2.61d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( ๐ต โˆ– ( ๐น supp โˆ… ) ) ) โ†’ ( ๐บ โ€˜ ๐‘˜ ) = โˆ… )
210 41 209 suppss โŠข ( ๐œ‘ โ†’ ( ๐บ supp โˆ… ) โŠ† ( ๐น supp โˆ… ) )
211 reldisj โŠข ( ( ๐บ supp โˆ… ) โŠ† ( ๐น supp โˆ… ) โ†’ ( ( ( ๐บ supp โˆ… ) โˆฉ { ๐‘‹ } ) = โˆ… โ†” ( ๐บ supp โˆ… ) โŠ† ( ( ๐น supp โˆ… ) โˆ– { ๐‘‹ } ) ) )
212 210 211 syl โŠข ( ๐œ‘ โ†’ ( ( ( ๐บ supp โˆ… ) โˆฉ { ๐‘‹ } ) = โˆ… โ†” ( ๐บ supp โˆ… ) โŠ† ( ( ๐น supp โˆ… ) โˆ– { ๐‘‹ } ) ) )
213 178 212 mpbid โŠข ( ๐œ‘ โ†’ ( ๐บ supp โˆ… ) โŠ† ( ( ๐น supp โˆ… ) โˆ– { ๐‘‹ } ) )
214 uncom โŠข ( ( ๐บ supp โˆ… ) โˆช { ๐‘‹ } ) = ( { ๐‘‹ } โˆช ( ๐บ supp โˆ… ) )
215 129 214 sseqtrdi โŠข ( ๐œ‘ โ†’ ( ๐น supp โˆ… ) โŠ† ( { ๐‘‹ } โˆช ( ๐บ supp โˆ… ) ) )
216 ssundif โŠข ( ( ๐น supp โˆ… ) โŠ† ( { ๐‘‹ } โˆช ( ๐บ supp โˆ… ) ) โ†” ( ( ๐น supp โˆ… ) โˆ– { ๐‘‹ } ) โŠ† ( ๐บ supp โˆ… ) )
217 215 216 sylib โŠข ( ๐œ‘ โ†’ ( ( ๐น supp โˆ… ) โˆ– { ๐‘‹ } ) โŠ† ( ๐บ supp โˆ… ) )
218 213 217 eqssd โŠข ( ๐œ‘ โ†’ ( ๐บ supp โˆ… ) = ( ( ๐น supp โˆ… ) โˆ– { ๐‘‹ } ) )
219 157 175 218 3eqtr4rd โŠข ( ๐œ‘ โ†’ ( ๐บ supp โˆ… ) = ( ๐‘‚ โ€œ โˆช dom ๐‘‚ ) )
220 isores3 โŠข ( ( ๐‘‚ Isom E , E ( dom ๐‘‚ , ( ๐น supp โˆ… ) ) โˆง โˆช dom ๐‘‚ โŠ† dom ๐‘‚ โˆง ( ๐บ supp โˆ… ) = ( ๐‘‚ โ€œ โˆช dom ๐‘‚ ) ) โ†’ ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) Isom E , E ( โˆช dom ๐‘‚ , ( ๐บ supp โˆ… ) ) )
221 28 146 219 220 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) Isom E , E ( โˆช dom ๐‘‚ , ( ๐บ supp โˆ… ) ) )
222 1 2 3 12 4 cantnfcl โŠข ( ๐œ‘ โ†’ ( E We ( ๐บ supp โˆ… ) โˆง dom ๐พ โˆˆ ฯ‰ ) )
223 222 simpld โŠข ( ๐œ‘ โ†’ E We ( ๐บ supp โˆ… ) )
224 epse โŠข E Se ( ๐บ supp โˆ… )
225 12 oieu โŠข ( ( E We ( ๐บ supp โˆ… ) โˆง E Se ( ๐บ supp โˆ… ) ) โ†’ ( ( Ord โˆช dom ๐‘‚ โˆง ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) Isom E , E ( โˆช dom ๐‘‚ , ( ๐บ supp โˆ… ) ) ) โ†” ( โˆช dom ๐‘‚ = dom ๐พ โˆง ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) = ๐พ ) ) )
226 223 224 225 sylancl โŠข ( ๐œ‘ โ†’ ( ( Ord โˆช dom ๐‘‚ โˆง ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) Isom E , E ( โˆช dom ๐‘‚ , ( ๐บ supp โˆ… ) ) ) โ†” ( โˆช dom ๐‘‚ = dom ๐พ โˆง ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) = ๐พ ) ) )
227 144 221 226 mpbi2and โŠข ( ๐œ‘ โ†’ ( โˆช dom ๐‘‚ = dom ๐พ โˆง ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) = ๐พ ) )
228 227 simpld โŠข ( ๐œ‘ โ†’ โˆช dom ๐‘‚ = dom ๐พ )
229 228 fveq2d โŠข ( ๐œ‘ โ†’ ( ๐‘€ โ€˜ โˆช dom ๐‘‚ ) = ( ๐‘€ โ€˜ dom ๐พ ) )
230 eleq1 โŠข ( ๐‘ฅ = โˆ… โ†’ ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†” โˆ… โˆˆ dom ๐‘‚ ) )
231 fveq2 โŠข ( ๐‘ฅ = โˆ… โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐ป โ€˜ โˆ… ) )
232 fveq2 โŠข ( ๐‘ฅ = โˆ… โ†’ ( ๐‘€ โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ โˆ… ) )
233 13 seqom0g โŠข ( โˆ… โˆˆ V โ†’ ( ๐‘€ โ€˜ โˆ… ) = โˆ… )
234 46 233 ax-mp โŠข ( ๐‘€ โ€˜ โˆ… ) = โˆ…
235 232 234 eqtrdi โŠข ( ๐‘ฅ = โˆ… โ†’ ( ๐‘€ โ€˜ ๐‘ฅ ) = โˆ… )
236 231 235 eqeq12d โŠข ( ๐‘ฅ = โˆ… โ†’ ( ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) โ†” ( ๐ป โ€˜ โˆ… ) = โˆ… ) )
237 230 236 imbi12d โŠข ( ๐‘ฅ = โˆ… โ†’ ( ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) ) โ†” ( โˆ… โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ โˆ… ) = โˆ… ) ) )
238 237 imbi2d โŠข ( ๐‘ฅ = โˆ… โ†’ ( ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) ) ) โ†” ( ๐œ‘ โ†’ ( โˆ… โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ โˆ… ) = โˆ… ) ) ) )
239 eleq1 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†” ๐‘ฆ โˆˆ dom ๐‘‚ ) )
240 fveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐ป โ€˜ ๐‘ฆ ) )
241 fveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘€ โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) )
242 240 241 eqeq12d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) โ†” ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) ) )
243 239 242 imbi12d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) ) โ†” ( ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) ) ) )
244 243 imbi2d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) ) ) โ†” ( ๐œ‘ โ†’ ( ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) ) ) ) )
245 eleq1 โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ dom ๐‘‚ ) )
246 fveq2 โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐ป โ€˜ suc ๐‘ฆ ) )
247 fveq2 โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ๐‘€ โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) )
248 246 247 eqeq12d โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) โ†” ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) ) )
249 245 248 imbi12d โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) ) โ†” ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) ) ) )
250 249 imbi2d โŠข ( ๐‘ฅ = suc ๐‘ฆ โ†’ ( ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) ) ) โ†” ( ๐œ‘ โ†’ ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) ) ) ) )
251 eleq1 โŠข ( ๐‘ฅ = โˆช dom ๐‘‚ โ†’ ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†” โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ ) )
252 fveq2 โŠข ( ๐‘ฅ = โˆช dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐ป โ€˜ โˆช dom ๐‘‚ ) )
253 fveq2 โŠข ( ๐‘ฅ = โˆช dom ๐‘‚ โ†’ ( ๐‘€ โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ โˆช dom ๐‘‚ ) )
254 252 253 eqeq12d โŠข ( ๐‘ฅ = โˆช dom ๐‘‚ โ†’ ( ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) โ†” ( ๐ป โ€˜ โˆช dom ๐‘‚ ) = ( ๐‘€ โ€˜ โˆช dom ๐‘‚ ) ) )
255 251 254 imbi12d โŠข ( ๐‘ฅ = โˆช dom ๐‘‚ โ†’ ( ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) ) โ†” ( โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ โˆช dom ๐‘‚ ) = ( ๐‘€ โ€˜ โˆช dom ๐‘‚ ) ) ) )
256 255 imbi2d โŠข ( ๐‘ฅ = โˆช dom ๐‘‚ โ†’ ( ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฅ ) = ( ๐‘€ โ€˜ ๐‘ฅ ) ) ) โ†” ( ๐œ‘ โ†’ ( โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ โˆช dom ๐‘‚ ) = ( ๐‘€ โ€˜ โˆช dom ๐‘‚ ) ) ) ) )
257 11 seqom0g โŠข ( โˆ… โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ โˆ… ) = โˆ… )
258 257 a1i โŠข ( ๐œ‘ โ†’ ( โˆ… โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ โˆ… ) = โˆ… ) )
259 nnord โŠข ( dom ๐‘‚ โˆˆ ฯ‰ โ†’ Ord dom ๐‘‚ )
260 19 259 syl โŠข ( ๐œ‘ โ†’ Ord dom ๐‘‚ )
261 ordtr โŠข ( Ord dom ๐‘‚ โ†’ Tr dom ๐‘‚ )
262 260 261 syl โŠข ( ๐œ‘ โ†’ Tr dom ๐‘‚ )
263 trsuc โŠข ( ( Tr dom ๐‘‚ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ๐‘ฆ โˆˆ dom ๐‘‚ )
264 262 263 sylan โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ๐‘ฆ โˆˆ dom ๐‘‚ )
265 264 ex โŠข ( ๐œ‘ โ†’ ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ๐‘ฆ โˆˆ dom ๐‘‚ ) )
266 265 imim1d โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) ) โ†’ ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) ) ) )
267 oveq2 โŠข ( ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) โ†’ ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ) +o ( ๐ป โ€˜ ๐‘ฆ ) ) = ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ) +o ( ๐‘€ โ€˜ ๐‘ฆ ) ) )
268 elnn โŠข ( ( ๐‘ฆ โˆˆ dom ๐‘‚ โˆง dom ๐‘‚ โˆˆ ฯ‰ ) โ†’ ๐‘ฆ โˆˆ ฯ‰ )
269 268 ancoms โŠข ( ( dom ๐‘‚ โˆˆ ฯ‰ โˆง ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ๐‘ฆ โˆˆ ฯ‰ )
270 19 264 269 syl2an2r โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ๐‘ฆ โˆˆ ฯ‰ )
271 1 2 3 10 14 11 cantnfsuc โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ) +o ( ๐ป โ€˜ ๐‘ฆ ) ) )
272 270 271 syldan โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ) +o ( ๐ป โ€˜ ๐‘ฆ ) ) )
273 1 2 3 12 4 13 cantnfsuc โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ฯ‰ ) โ†’ ( ๐‘€ โ€˜ suc ๐‘ฆ ) = ( ( ( ๐ด โ†‘o ( ๐พ โ€˜ ๐‘ฆ ) ) ยทo ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) ) +o ( ๐‘€ โ€˜ ๐‘ฆ ) ) )
274 270 273 syldan โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐‘€ โ€˜ suc ๐‘ฆ ) = ( ( ( ๐ด โ†‘o ( ๐พ โ€˜ ๐‘ฆ ) ) ยทo ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) ) +o ( ๐‘€ โ€˜ ๐‘ฆ ) ) )
275 227 simprd โŠข ( ๐œ‘ โ†’ ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) = ๐พ )
276 275 fveq1d โŠข ( ๐œ‘ โ†’ ( ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) โ€˜ ๐‘ฆ ) = ( ๐พ โ€˜ ๐‘ฆ ) )
277 276 adantr โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) โ€˜ ๐‘ฆ ) = ( ๐พ โ€˜ ๐‘ฆ ) )
278 16 eleq2d โŠข ( ๐œ‘ โ†’ ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚ ) )
279 278 biimpa โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚ )
280 144 adantr โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ Ord โˆช dom ๐‘‚ )
281 ordsucelsuc โŠข ( Ord โˆช dom ๐‘‚ โ†’ ( ๐‘ฆ โˆˆ โˆช dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚ ) )
282 280 281 syl โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐‘ฆ โˆˆ โˆช dom ๐‘‚ โ†” suc ๐‘ฆ โˆˆ suc โˆช dom ๐‘‚ ) )
283 279 282 mpbird โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ๐‘ฆ โˆˆ โˆช dom ๐‘‚ )
284 283 fvresd โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ( ๐‘‚ โ†พ โˆช dom ๐‘‚ ) โ€˜ ๐‘ฆ ) = ( ๐‘‚ โ€˜ ๐‘ฆ ) )
285 277 284 eqtr3d โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐พ โ€˜ ๐‘ฆ ) = ( ๐‘‚ โ€˜ ๐‘ฆ ) )
286 285 oveq2d โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐ด โ†‘o ( ๐พ โ€˜ ๐‘ฆ ) ) = ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) )
287 eqeq1 โŠข ( ๐‘ก = ( ๐พ โ€˜ ๐‘ฆ ) โ†’ ( ๐‘ก = ๐‘‹ โ†” ( ๐พ โ€˜ ๐‘ฆ ) = ๐‘‹ ) )
288 fveq2 โŠข ( ๐‘ก = ( ๐พ โ€˜ ๐‘ฆ ) โ†’ ( ๐บ โ€˜ ๐‘ก ) = ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) )
289 287 288 ifbieq2d โŠข ( ๐‘ก = ( ๐พ โ€˜ ๐‘ฆ ) โ†’ if ( ๐‘ก = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ๐‘ก ) ) = if ( ( ๐พ โ€˜ ๐‘ฆ ) = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) ) )
290 suppssdm โŠข ( ๐บ supp โˆ… ) โŠ† dom ๐บ
291 290 41 fssdm โŠข ( ๐œ‘ โ†’ ( ๐บ supp โˆ… ) โŠ† ๐ต )
292 291 adantr โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐บ supp โˆ… ) โŠ† ๐ต )
293 228 adantr โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ โˆช dom ๐‘‚ = dom ๐พ )
294 283 293 eleqtrd โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ๐‘ฆ โˆˆ dom ๐พ )
295 12 oif โŠข ๐พ : dom ๐พ โŸถ ( ๐บ supp โˆ… )
296 295 ffvelrni โŠข ( ๐‘ฆ โˆˆ dom ๐พ โ†’ ( ๐พ โ€˜ ๐‘ฆ ) โˆˆ ( ๐บ supp โˆ… ) )
297 294 296 syl โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐พ โ€˜ ๐‘ฆ ) โˆˆ ( ๐บ supp โˆ… ) )
298 292 297 sseldd โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐พ โ€˜ ๐‘ฆ ) โˆˆ ๐ต )
299 6 adantr โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ๐‘Œ โˆˆ ๐ด )
300 fvex โŠข ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) โˆˆ V
301 ifexg โŠข ( ( ๐‘Œ โˆˆ ๐ด โˆง ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) โˆˆ V ) โ†’ if ( ( ๐พ โ€˜ ๐‘ฆ ) = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) ) โˆˆ V )
302 299 300 301 sylancl โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ if ( ( ๐พ โ€˜ ๐‘ฆ ) = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) ) โˆˆ V )
303 8 289 298 302 fvmptd3 โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐น โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) = if ( ( ๐พ โ€˜ ๐‘ฆ ) = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) ) )
304 285 fveq2d โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐น โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) = ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) )
305 176 adantr โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ยฌ ๐‘‹ โˆˆ ( ๐บ supp โˆ… ) )
306 nelneq โŠข ( ( ( ๐พ โ€˜ ๐‘ฆ ) โˆˆ ( ๐บ supp โˆ… ) โˆง ยฌ ๐‘‹ โˆˆ ( ๐บ supp โˆ… ) ) โ†’ ยฌ ( ๐พ โ€˜ ๐‘ฆ ) = ๐‘‹ )
307 297 305 306 syl2anc โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ยฌ ( ๐พ โ€˜ ๐‘ฆ ) = ๐‘‹ )
308 307 iffalsed โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ if ( ( ๐พ โ€˜ ๐‘ฆ ) = ๐‘‹ , ๐‘Œ , ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) ) = ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) )
309 303 304 308 3eqtr3rd โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) = ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) )
310 286 309 oveq12d โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ( ๐ด โ†‘o ( ๐พ โ€˜ ๐‘ฆ ) ) ยทo ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) ) = ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ) )
311 310 oveq1d โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ( ( ๐ด โ†‘o ( ๐พ โ€˜ ๐‘ฆ ) ) ยทo ( ๐บ โ€˜ ( ๐พ โ€˜ ๐‘ฆ ) ) ) +o ( ๐‘€ โ€˜ ๐‘ฆ ) ) = ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ) +o ( ๐‘€ โ€˜ ๐‘ฆ ) ) )
312 274 311 eqtrd โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ๐‘€ โ€˜ suc ๐‘ฆ ) = ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ) +o ( ๐‘€ โ€˜ ๐‘ฆ ) ) )
313 272 312 eqeq12d โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) โ†” ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ) +o ( ๐ป โ€˜ ๐‘ฆ ) ) = ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ ๐‘ฆ ) ) ) +o ( ๐‘€ โ€˜ ๐‘ฆ ) ) ) )
314 267 313 syl5ibr โŠข ( ( ๐œ‘ โˆง suc ๐‘ฆ โˆˆ dom ๐‘‚ ) โ†’ ( ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) ) )
315 314 ex โŠข ( ๐œ‘ โ†’ ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) ) ) )
316 315 a2d โŠข ( ๐œ‘ โ†’ ( ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) ) โ†’ ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) ) ) )
317 266 316 syld โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) ) โ†’ ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) ) ) )
318 317 a2i โŠข ( ( ๐œ‘ โ†’ ( ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) ) ) โ†’ ( ๐œ‘ โ†’ ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) ) ) )
319 318 a1i โŠข ( ๐‘ฆ โˆˆ ฯ‰ โ†’ ( ( ๐œ‘ โ†’ ( ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ ๐‘ฆ ) = ( ๐‘€ โ€˜ ๐‘ฆ ) ) ) โ†’ ( ๐œ‘ โ†’ ( suc ๐‘ฆ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ suc ๐‘ฆ ) = ( ๐‘€ โ€˜ suc ๐‘ฆ ) ) ) ) )
320 238 244 250 256 258 319 finds โŠข ( โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ ( ๐œ‘ โ†’ ( โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ โˆช dom ๐‘‚ ) = ( ๐‘€ โ€˜ โˆช dom ๐‘‚ ) ) ) )
321 22 320 mpcom โŠข ( ๐œ‘ โ†’ ( โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ ( ๐ป โ€˜ โˆช dom ๐‘‚ ) = ( ๐‘€ โ€˜ โˆช dom ๐‘‚ ) ) )
322 64 321 mpd โŠข ( ๐œ‘ โ†’ ( ๐ป โ€˜ โˆช dom ๐‘‚ ) = ( ๐‘€ โ€˜ โˆช dom ๐‘‚ ) )
323 1 2 3 12 4 13 cantnfval โŠข ( ๐œ‘ โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐บ ) = ( ๐‘€ โ€˜ dom ๐พ ) )
324 229 322 323 3eqtr4d โŠข ( ๐œ‘ โ†’ ( ๐ป โ€˜ โˆช dom ๐‘‚ ) = ( ( ๐ด CNF ๐ต ) โ€˜ ๐บ ) )
325 142 324 oveq12d โŠข ( ๐œ‘ โ†’ ( ( ( ๐ด โ†‘o ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ยทo ( ๐น โ€˜ ( ๐‘‚ โ€˜ โˆช dom ๐‘‚ ) ) ) +o ( ๐ป โ€˜ โˆช dom ๐‘‚ ) ) = ( ( ( ๐ด โ†‘o ๐‘‹ ) ยทo ๐‘Œ ) +o ( ( ๐ด CNF ๐ต ) โ€˜ ๐บ ) ) )
326 24 325 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐ป โ€˜ suc โˆช dom ๐‘‚ ) = ( ( ( ๐ด โ†‘o ๐‘‹ ) ยทo ๐‘Œ ) +o ( ( ๐ด CNF ๐ต ) โ€˜ ๐บ ) ) )
327 15 17 326 3eqtrd โŠข ( ๐œ‘ โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐น ) = ( ( ( ๐ด โ†‘o ๐‘‹ ) ยทo ๐‘Œ ) +o ( ( ๐ด CNF ๐ต ) โ€˜ ๐บ ) ) )