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

Theorem cantnflem1 9625
Description: Lemma for cantnf 9629. This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation ๐‘‡ is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct ๐น, ๐บ are ๐‘‡ -related as ๐น < ๐บ or ๐บ < ๐น, and WLOG assuming that ๐น < ๐บ, we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 2-Jul-2019.)
Hypotheses
Ref Expression
cantnfs.s ๐‘† = dom (๐ด CNF ๐ต)
cantnfs.a (๐œ‘ โ†’ ๐ด โˆˆ On)
cantnfs.b (๐œ‘ โ†’ ๐ต โˆˆ On)
oemapval.t ๐‘‡ = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))}
oemapval.f (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
oemapval.g (๐œ‘ โ†’ ๐บ โˆˆ ๐‘†)
oemapvali.r (๐œ‘ โ†’ ๐น๐‘‡๐บ)
oemapvali.x ๐‘‹ = โˆช {๐‘ โˆˆ ๐ต โˆฃ (๐นโ€˜๐‘) โˆˆ (๐บโ€˜๐‘)}
cantnflem1.o ๐‘‚ = OrdIso( E , (๐บ supp โˆ…))
cantnflem1.h ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐‘‚โ€˜๐‘˜)) ยทo (๐บโ€˜(๐‘‚โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
Assertion
Ref Expression
cantnflem1 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) โˆˆ ((๐ด CNF ๐ต)โ€˜๐บ))
Distinct variable groups:   ๐‘˜,๐‘,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง,๐ต   ๐ด,๐‘,๐‘˜,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘‡,๐‘,๐‘˜   ๐‘˜,๐น,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘†,๐‘,๐‘˜,๐‘ฅ,๐‘ฆ,๐‘ง   ๐บ,๐‘,๐‘˜,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘ฅ,๐ป,๐‘ฆ   ๐‘˜,๐‘‚,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง   ๐œ‘,๐‘˜,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘˜,๐‘‹,๐‘ค,๐‘ฅ,๐‘ฆ,๐‘ง   ๐น,๐‘   ๐œ‘,๐‘
Allowed substitution hints:   ๐œ‘(๐‘ค)   ๐‘†(๐‘ค)   ๐‘‡(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐ป(๐‘ง,๐‘ค,๐‘˜,๐‘)   ๐‘‚(๐‘)   ๐‘‹(๐‘)

Proof of Theorem cantnflem1
Dummy variable ๐‘ข is distinct from all other variables.
StepHypRef Expression
1 ovex 7390 . . . . . 6 (๐บ supp โˆ…) โˆˆ V
2 cantnflem1.o . . . . . . 7 ๐‘‚ = OrdIso( E , (๐บ supp โˆ…))
32oion 9472 . . . . . 6 ((๐บ supp โˆ…) โˆˆ V โ†’ dom ๐‘‚ โˆˆ On)
41, 3mp1i 13 . . . . 5 (๐œ‘ โ†’ dom ๐‘‚ โˆˆ On)
5 uniexg 7677 . . . . 5 (dom ๐‘‚ โˆˆ On โ†’ โˆช dom ๐‘‚ โˆˆ V)
6 sucidg 6398 . . . . 5 (โˆช dom ๐‘‚ โˆˆ V โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚)
74, 5, 63syl 18 . . . 4 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ suc โˆช dom ๐‘‚)
8 cantnfs.s . . . . . . . . . 10 ๐‘† = dom (๐ด CNF ๐ต)
9 cantnfs.a . . . . . . . . . 10 (๐œ‘ โ†’ ๐ด โˆˆ On)
10 cantnfs.b . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โˆˆ On)
11 oemapval.t . . . . . . . . . 10 ๐‘‡ = {โŸจ๐‘ฅ, ๐‘ฆโŸฉ โˆฃ โˆƒ๐‘ง โˆˆ ๐ต ((๐‘ฅโ€˜๐‘ง) โˆˆ (๐‘ฆโ€˜๐‘ง) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘ง โˆˆ ๐‘ค โ†’ (๐‘ฅโ€˜๐‘ค) = (๐‘ฆโ€˜๐‘ค)))}
12 oemapval.f . . . . . . . . . 10 (๐œ‘ โ†’ ๐น โˆˆ ๐‘†)
13 oemapval.g . . . . . . . . . 10 (๐œ‘ โ†’ ๐บ โˆˆ ๐‘†)
14 oemapvali.r . . . . . . . . . 10 (๐œ‘ โ†’ ๐น๐‘‡๐บ)
15 oemapvali.x . . . . . . . . . 10 ๐‘‹ = โˆช {๐‘ โˆˆ ๐ต โˆฃ (๐นโ€˜๐‘) โˆˆ (๐บโ€˜๐‘)}
168, 9, 10, 11, 12, 13, 14, 15cantnflem1a 9621 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘‹ โˆˆ (๐บ supp โˆ…))
17 n0i 4293 . . . . . . . . 9 (๐‘‹ โˆˆ (๐บ supp โˆ…) โ†’ ยฌ (๐บ supp โˆ…) = โˆ…)
1816, 17syl 17 . . . . . . . 8 (๐œ‘ โ†’ ยฌ (๐บ supp โˆ…) = โˆ…)
19 ovexd 7392 . . . . . . . . . 10 (๐œ‘ โ†’ (๐บ supp โˆ…) โˆˆ V)
208, 9, 10, 2, 13cantnfcl 9603 . . . . . . . . . . 11 (๐œ‘ โ†’ ( E We (๐บ supp โˆ…) โˆง dom ๐‘‚ โˆˆ ฯ‰))
2120simpld 495 . . . . . . . . . 10 (๐œ‘ โ†’ E We (๐บ supp โˆ…))
222oien 9474 . . . . . . . . . 10 (((๐บ supp โˆ…) โˆˆ V โˆง E We (๐บ supp โˆ…)) โ†’ dom ๐‘‚ โ‰ˆ (๐บ supp โˆ…))
2319, 21, 22syl2anc 584 . . . . . . . . 9 (๐œ‘ โ†’ dom ๐‘‚ โ‰ˆ (๐บ supp โˆ…))
24 breq1 5108 . . . . . . . . . 10 (dom ๐‘‚ = โˆ… โ†’ (dom ๐‘‚ โ‰ˆ (๐บ supp โˆ…) โ†” โˆ… โ‰ˆ (๐บ supp โˆ…)))
25 ensymb 8942 . . . . . . . . . . 11 (โˆ… โ‰ˆ (๐บ supp โˆ…) โ†” (๐บ supp โˆ…) โ‰ˆ โˆ…)
26 en0 8957 . . . . . . . . . . 11 ((๐บ supp โˆ…) โ‰ˆ โˆ… โ†” (๐บ supp โˆ…) = โˆ…)
2725, 26bitri 274 . . . . . . . . . 10 (โˆ… โ‰ˆ (๐บ supp โˆ…) โ†” (๐บ supp โˆ…) = โˆ…)
2824, 27bitrdi 286 . . . . . . . . 9 (dom ๐‘‚ = โˆ… โ†’ (dom ๐‘‚ โ‰ˆ (๐บ supp โˆ…) โ†” (๐บ supp โˆ…) = โˆ…))
2923, 28syl5ibcom 244 . . . . . . . 8 (๐œ‘ โ†’ (dom ๐‘‚ = โˆ… โ†’ (๐บ supp โˆ…) = โˆ…))
3018, 29mtod 197 . . . . . . 7 (๐œ‘ โ†’ ยฌ dom ๐‘‚ = โˆ…)
3120simprd 496 . . . . . . . 8 (๐œ‘ โ†’ dom ๐‘‚ โˆˆ ฯ‰)
32 nnlim 7816 . . . . . . . 8 (dom ๐‘‚ โˆˆ ฯ‰ โ†’ ยฌ Lim dom ๐‘‚)
3331, 32syl 17 . . . . . . 7 (๐œ‘ โ†’ ยฌ Lim dom ๐‘‚)
34 ioran 982 . . . . . . 7 (ยฌ (dom ๐‘‚ = โˆ… โˆจ Lim dom ๐‘‚) โ†” (ยฌ dom ๐‘‚ = โˆ… โˆง ยฌ Lim dom ๐‘‚))
3530, 33, 34sylanbrc 583 . . . . . 6 (๐œ‘ โ†’ ยฌ (dom ๐‘‚ = โˆ… โˆจ Lim dom ๐‘‚))
362oicl 9465 . . . . . . 7 Ord dom ๐‘‚
37 unizlim 6440 . . . . . . 7 (Ord dom ๐‘‚ โ†’ (dom ๐‘‚ = โˆช dom ๐‘‚ โ†” (dom ๐‘‚ = โˆ… โˆจ Lim dom ๐‘‚)))
3836, 37mp1i 13 . . . . . 6 (๐œ‘ โ†’ (dom ๐‘‚ = โˆช dom ๐‘‚ โ†” (dom ๐‘‚ = โˆ… โˆจ Lim dom ๐‘‚)))
3935, 38mtbird 324 . . . . 5 (๐œ‘ โ†’ ยฌ dom ๐‘‚ = โˆช dom ๐‘‚)
40 orduniorsuc 7765 . . . . . . 7 (Ord dom ๐‘‚ โ†’ (dom ๐‘‚ = โˆช dom ๐‘‚ โˆจ dom ๐‘‚ = suc โˆช dom ๐‘‚))
4136, 40mp1i 13 . . . . . 6 (๐œ‘ โ†’ (dom ๐‘‚ = โˆช dom ๐‘‚ โˆจ dom ๐‘‚ = suc โˆช dom ๐‘‚))
4241ord 862 . . . . 5 (๐œ‘ โ†’ (ยฌ dom ๐‘‚ = โˆช dom ๐‘‚ โ†’ dom ๐‘‚ = suc โˆช dom ๐‘‚))
4339, 42mpd 15 . . . 4 (๐œ‘ โ†’ dom ๐‘‚ = suc โˆช dom ๐‘‚)
447, 43eleqtrrd 2840 . . 3 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ dom ๐‘‚)
452oiiso 9473 . . . . . . . 8 (((๐บ supp โˆ…) โˆˆ V โˆง E We (๐บ supp โˆ…)) โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)))
4619, 21, 45syl2anc 584 . . . . . . 7 (๐œ‘ โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)))
47 isof1o 7268 . . . . . . 7 (๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)) โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐บ supp โˆ…))
4846, 47syl 17 . . . . . 6 (๐œ‘ โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐บ supp โˆ…))
49 f1ocnv 6796 . . . . . 6 (๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐บ supp โˆ…) โ†’ โ—ก๐‘‚:(๐บ supp โˆ…)โ€“1-1-ontoโ†’dom ๐‘‚)
50 f1of 6784 . . . . . 6 (โ—ก๐‘‚:(๐บ supp โˆ…)โ€“1-1-ontoโ†’dom ๐‘‚ โ†’ โ—ก๐‘‚:(๐บ supp โˆ…)โŸถdom ๐‘‚)
5148, 49, 503syl 18 . . . . 5 (๐œ‘ โ†’ โ—ก๐‘‚:(๐บ supp โˆ…)โŸถdom ๐‘‚)
5251, 16ffvelcdmd 7036 . . . 4 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚)
53 elssuni 4898 . . . 4 ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚)
5452, 53syl 17 . . 3 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚)
5543, 31eqeltrrd 2838 . . . . 5 (๐œ‘ โ†’ suc โˆช dom ๐‘‚ โˆˆ ฯ‰)
56 peano2b 7819 . . . . 5 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†” suc โˆช dom ๐‘‚ โˆˆ ฯ‰)
5755, 56sylibr 233 . . . 4 (๐œ‘ โ†’ โˆช dom ๐‘‚ โˆˆ ฯ‰)
58 eleq1 2825 . . . . . . . 8 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ (๐‘ฆ โˆˆ dom ๐‘‚ โ†” โˆช dom ๐‘‚ โˆˆ dom ๐‘‚))
59 sseq2 3970 . . . . . . . 8 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ โ†” (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚))
6058, 59anbi12d 631 . . . . . . 7 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ ((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†” (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚)))
61 fveq2 6842 . . . . . . . . . . . 12 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ (๐‘‚โ€˜๐‘ฆ) = (๐‘‚โ€˜โˆช dom ๐‘‚))
6261sseq2d 3976 . . . . . . . . . . 11 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ) โ†” ๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚)))
6362ifbid 4509 . . . . . . . . . 10 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))
6463mpteq2dv 5207 . . . . . . . . 9 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…)))
6564fveq2d 6846 . . . . . . . 8 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) = ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))))
66 suceq 6383 . . . . . . . . 9 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ suc ๐‘ฆ = suc โˆช dom ๐‘‚)
6766fveq2d 6846 . . . . . . . 8 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐ปโ€˜suc โˆช dom ๐‘‚))
6865, 67eleq12d 2831 . . . . . . 7 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ) โ†” ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆช dom ๐‘‚)))
6960, 68imbi12d 344 . . . . . 6 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ (((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ)) โ†” ((โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆช dom ๐‘‚))))
7069imbi2d 340 . . . . 5 (๐‘ฆ = โˆช dom ๐‘‚ โ†’ ((๐œ‘ โ†’ ((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ))) โ†” (๐œ‘ โ†’ ((โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆช dom ๐‘‚)))))
71 eleq1 2825 . . . . . . . 8 (๐‘ฆ = โˆ… โ†’ (๐‘ฆ โˆˆ dom ๐‘‚ โ†” โˆ… โˆˆ dom ๐‘‚))
72 sseq2 3970 . . . . . . . 8 (๐‘ฆ = โˆ… โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ โ†” (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ…))
7371, 72anbi12d 631 . . . . . . 7 (๐‘ฆ = โˆ… โ†’ ((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†” (โˆ… โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ…)))
74 fveq2 6842 . . . . . . . . . . . 12 (๐‘ฆ = โˆ… โ†’ (๐‘‚โ€˜๐‘ฆ) = (๐‘‚โ€˜โˆ…))
7574sseq2d 3976 . . . . . . . . . . 11 (๐‘ฆ = โˆ… โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ) โ†” ๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…)))
7675ifbid 4509 . . . . . . . . . 10 (๐‘ฆ = โˆ… โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…))
7776mpteq2dv 5207 . . . . . . . . 9 (๐‘ฆ = โˆ… โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…)))
7877fveq2d 6846 . . . . . . . 8 (๐‘ฆ = โˆ… โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) = ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…))))
79 suceq 6383 . . . . . . . . 9 (๐‘ฆ = โˆ… โ†’ suc ๐‘ฆ = suc โˆ…)
8079fveq2d 6846 . . . . . . . 8 (๐‘ฆ = โˆ… โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐ปโ€˜suc โˆ…))
8178, 80eleq12d 2831 . . . . . . 7 (๐‘ฆ = โˆ… โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ) โ†” ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆ…)))
8273, 81imbi12d 344 . . . . . 6 (๐‘ฆ = โˆ… โ†’ (((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ)) โ†” ((โˆ… โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ…) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆ…))))
83 eleq1 2825 . . . . . . . 8 (๐‘ฆ = ๐‘ข โ†’ (๐‘ฆ โˆˆ dom ๐‘‚ โ†” ๐‘ข โˆˆ dom ๐‘‚))
84 sseq2 3970 . . . . . . . 8 (๐‘ฆ = ๐‘ข โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ โ†” (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข))
8583, 84anbi12d 631 . . . . . . 7 (๐‘ฆ = ๐‘ข โ†’ ((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†” (๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)))
86 fveq2 6842 . . . . . . . . . . . 12 (๐‘ฆ = ๐‘ข โ†’ (๐‘‚โ€˜๐‘ฆ) = (๐‘‚โ€˜๐‘ข))
8786sseq2d 3976 . . . . . . . . . . 11 (๐‘ฆ = ๐‘ข โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ) โ†” ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)))
8887ifbid 4509 . . . . . . . . . 10 (๐‘ฆ = ๐‘ข โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))
8988mpteq2dv 5207 . . . . . . . . 9 (๐‘ฆ = ๐‘ข โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))
9089fveq2d 6846 . . . . . . . 8 (๐‘ฆ = ๐‘ข โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) = ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))))
91 suceq 6383 . . . . . . . . 9 (๐‘ฆ = ๐‘ข โ†’ suc ๐‘ฆ = suc ๐‘ข)
9291fveq2d 6846 . . . . . . . 8 (๐‘ฆ = ๐‘ข โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐ปโ€˜suc ๐‘ข))
9390, 92eleq12d 2831 . . . . . . 7 (๐‘ฆ = ๐‘ข โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ) โ†” ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)))
9485, 93imbi12d 344 . . . . . 6 (๐‘ฆ = ๐‘ข โ†’ (((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ)) โ†” ((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข))))
95 eleq1 2825 . . . . . . . 8 (๐‘ฆ = suc ๐‘ข โ†’ (๐‘ฆ โˆˆ dom ๐‘‚ โ†” suc ๐‘ข โˆˆ dom ๐‘‚))
96 sseq2 3970 . . . . . . . 8 (๐‘ฆ = suc ๐‘ข โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ โ†” (โ—ก๐‘‚โ€˜๐‘‹) โŠ† suc ๐‘ข))
9795, 96anbi12d 631 . . . . . . 7 (๐‘ฆ = suc ๐‘ข โ†’ ((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†” (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† suc ๐‘ข)))
98 fveq2 6842 . . . . . . . . . . . 12 (๐‘ฆ = suc ๐‘ข โ†’ (๐‘‚โ€˜๐‘ฆ) = (๐‘‚โ€˜suc ๐‘ข))
9998sseq2d 3976 . . . . . . . . . . 11 (๐‘ฆ = suc ๐‘ข โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ) โ†” ๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข)))
10099ifbid 4509 . . . . . . . . . 10 (๐‘ฆ = suc ๐‘ข โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))
101100mpteq2dv 5207 . . . . . . . . 9 (๐‘ฆ = suc ๐‘ข โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))
102101fveq2d 6846 . . . . . . . 8 (๐‘ฆ = suc ๐‘ข โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) = ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))))
103 suceq 6383 . . . . . . . . 9 (๐‘ฆ = suc ๐‘ข โ†’ suc ๐‘ฆ = suc suc ๐‘ข)
104103fveq2d 6846 . . . . . . . 8 (๐‘ฆ = suc ๐‘ข โ†’ (๐ปโ€˜suc ๐‘ฆ) = (๐ปโ€˜suc suc ๐‘ข))
105102, 104eleq12d 2831 . . . . . . 7 (๐‘ฆ = suc ๐‘ข โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ) โ†” ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข)))
10697, 105imbi12d 344 . . . . . 6 (๐‘ฆ = suc ๐‘ข โ†’ (((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ)) โ†” ((suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† suc ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข))))
107 f1ocnvfv2 7223 . . . . . . . . . . . . 13 ((๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐บ supp โˆ…) โˆง ๐‘‹ โˆˆ (๐บ supp โˆ…)) โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) = ๐‘‹)
10848, 16, 107syl2anc 584 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) = ๐‘‹)
109108sseq2d 3976 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” ๐‘ฅ โŠ† ๐‘‹))
110109ifbid 4509 . . . . . . . . . 10 (๐œ‘ โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† ๐‘‹, (๐นโ€˜๐‘ฅ), โˆ…))
111110mpteq2dv 5207 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† ๐‘‹, (๐นโ€˜๐‘ฅ), โˆ…)))
112111fveq2d 6846 . . . . . . . 8 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…))) = ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† ๐‘‹, (๐นโ€˜๐‘ฅ), โˆ…))))
113 cantnflem1.h . . . . . . . . 9 ๐ป = seqฯ‰((๐‘˜ โˆˆ V, ๐‘ง โˆˆ V โ†ฆ (((๐ด โ†‘o (๐‘‚โ€˜๐‘˜)) ยทo (๐บโ€˜(๐‘‚โ€˜๐‘˜))) +o ๐‘ง)), โˆ…)
1148, 9, 10, 11, 12, 13, 14, 15, 2, 113cantnflem1d 9624 . . . . . . . 8 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† ๐‘‹, (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc (โ—ก๐‘‚โ€˜๐‘‹)))
115112, 114eqeltrd 2837 . . . . . . 7 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc (โ—ก๐‘‚โ€˜๐‘‹)))
116 ss0 4358 . . . . . . . . . . . . . 14 ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ… โ†’ (โ—ก๐‘‚โ€˜๐‘‹) = โˆ…)
117116fveq2d 6846 . . . . . . . . . . . . 13 ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ… โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) = (๐‘‚โ€˜โˆ…))
118117sseq2d 3976 . . . . . . . . . . . 12 ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ… โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” ๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…)))
119118ifbid 4509 . . . . . . . . . . 11 ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ… โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…))
120119mpteq2dv 5207 . . . . . . . . . 10 ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ… โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…)))
121120fveq2d 6846 . . . . . . . . 9 ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ… โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…))) = ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…))))
122 suceq 6383 . . . . . . . . . . 11 ((โ—ก๐‘‚โ€˜๐‘‹) = โˆ… โ†’ suc (โ—ก๐‘‚โ€˜๐‘‹) = suc โˆ…)
123116, 122syl 17 . . . . . . . . . 10 ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ… โ†’ suc (โ—ก๐‘‚โ€˜๐‘‹) = suc โˆ…)
124123fveq2d 6846 . . . . . . . . 9 ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ… โ†’ (๐ปโ€˜suc (โ—ก๐‘‚โ€˜๐‘‹)) = (๐ปโ€˜suc โˆ…))
125121, 124eleq12d 2831 . . . . . . . 8 ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ… โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc (โ—ก๐‘‚โ€˜๐‘‹)) โ†” ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆ…)))
126125adantl 482 . . . . . . 7 ((โˆ… โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ…) โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc (โ—ก๐‘‚โ€˜๐‘‹)) โ†” ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆ…)))
127115, 126syl5ibcom 244 . . . . . 6 (๐œ‘ โ†’ ((โˆ… โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆ…) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆ…), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆ…)))
128 ordelon 6341 . . . . . . . . . . . 12 ((Ord dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚) โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On)
12936, 52, 128sylancr 587 . . . . . . . . . . 11 (๐œ‘ โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On)
13036a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ Ord dom ๐‘‚)
131 ordelon 6341 . . . . . . . . . . . 12 ((Ord dom ๐‘‚ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ suc ๐‘ข โˆˆ On)
132130, 131sylan 580 . . . . . . . . . . 11 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ suc ๐‘ข โˆˆ On)
133 onsseleq 6358 . . . . . . . . . . 11 (((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On โˆง suc ๐‘ข โˆˆ On) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† suc ๐‘ข โ†” ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข โˆจ (โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข)))
134129, 132, 133syl2an2r 683 . . . . . . . . . 10 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† suc ๐‘ข โ†” ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข โˆจ (โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข)))
135 onsucb 7752 . . . . . . . . . . . . . . 15 (๐‘ข โˆˆ On โ†” suc ๐‘ข โˆˆ On)
136132, 135sylibr 233 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ ๐‘ข โˆˆ On)
137 eloni 6327 . . . . . . . . . . . . . 14 (๐‘ข โˆˆ On โ†’ Ord ๐‘ข)
138136, 137syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ Ord ๐‘ข)
139 ordsssuc 6406 . . . . . . . . . . . . 13 (((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On โˆง Ord ๐‘ข) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข โ†” (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข))
140129, 138, 139syl2an2r 683 . . . . . . . . . . . 12 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข โ†” (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข))
141 ordtr 6331 . . . . . . . . . . . . . . . . 17 (Ord dom ๐‘‚ โ†’ Tr dom ๐‘‚)
14236, 141mp1i 13 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ Tr dom ๐‘‚)
143 simprl 769 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ suc ๐‘ข โˆˆ dom ๐‘‚)
144 trsuc 6404 . . . . . . . . . . . . . . . 16 ((Tr dom ๐‘‚ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ ๐‘ข โˆˆ dom ๐‘‚)
145142, 143, 144syl2anc 584 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ๐‘ข โˆˆ dom ๐‘‚)
146 simprr 771 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)
147145, 146jca 512 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข))
14810adantr 481 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ๐ต โˆˆ On)
149 oecl 8483 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ On โˆง ๐ต โˆˆ On) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
1509, 148, 149syl2an2r 683 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐ด โ†‘o ๐ต) โˆˆ On)
1519adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ๐ด โˆˆ On)
1528, 151, 148cantnff 9610 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐ด CNF ๐ต):๐‘†โŸถ(๐ด โ†‘o ๐ต))
1538, 9, 10cantnfs 9602 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ (๐น โˆˆ ๐‘† โ†” (๐น:๐ตโŸถ๐ด โˆง ๐น finSupp โˆ…)))
15412, 153mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐œ‘ โ†’ (๐น:๐ตโŸถ๐ด โˆง ๐น finSupp โˆ…))
155154simpld 495 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ ๐น:๐ตโŸถ๐ด)
156155ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐นโ€˜๐‘ฅ) โˆˆ ๐ด)
1578, 9, 10cantnfs 9602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐œ‘ โ†’ (๐บ โˆˆ ๐‘† โ†” (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…)))
15813, 157mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ (๐บ:๐ตโŸถ๐ด โˆง ๐บ finSupp โˆ…))
159158simpld 495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐œ‘ โ†’ ๐บ:๐ตโŸถ๐ด)
1608, 9, 10, 11, 12, 13, 14, 15oemapvali 9620 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ (๐‘‹ โˆˆ ๐ต โˆง (๐นโ€˜๐‘‹) โˆˆ (๐บโ€˜๐‘‹) โˆง โˆ€๐‘ค โˆˆ ๐ต (๐‘‹ โˆˆ ๐‘ค โ†’ (๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค))))
161160simp1d 1142 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
162159, 161ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ (๐บโ€˜๐‘‹) โˆˆ ๐ด)
163162ne0d 4295 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐œ‘ โ†’ ๐ด โ‰  โˆ…)
164 on0eln0 6373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐ด โˆˆ On โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
1659, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐œ‘ โ†’ (โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ…))
166163, 165mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ โˆ… โˆˆ ๐ด)
167166adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ โˆ… โˆˆ ๐ด)
168156, 167ifcld 4532 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ ๐ด)
169168fmpttd 7063 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)):๐ตโŸถ๐ด)
17010mptexd 7174 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) โˆˆ V)
171 funmpt 6539 . . . . . . . . . . . . . . . . . . . . . . 23 Fun (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))
172171a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ Fun (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))
173154simprd 496 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ๐น finSupp โˆ…)
174 ssidd 3967 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ (๐น supp โˆ…) โŠ† (๐น supp โˆ…))
175 0ex 5264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 โˆ… โˆˆ V
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐œ‘ โ†’ โˆ… โˆˆ V)
177155, 174, 10, 176suppssr 8127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ (๐นโ€˜๐‘ฅ) = โˆ…)
178177ifeq1d 4505 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), โˆ…, โˆ…))
179 ifid 4526 . . . . . . . . . . . . . . . . . . . . . . . 24 if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), โˆ…, โˆ…) = โˆ…
180178, 179eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐ต โˆ– (๐น supp โˆ…))) โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = โˆ…)
181180, 10suppss2 8131 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) supp โˆ…) โŠ† (๐น supp โˆ…))
182 fsuppsssupp 9321 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) โˆˆ V โˆง Fun (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆง (๐น finSupp โˆ… โˆง ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) supp โˆ…) โŠ† (๐น supp โˆ…))) โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) finSupp โˆ…)
183170, 172, 173, 181, 182syl22anc 837 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) finSupp โˆ…)
1848, 9, 10cantnfs 9602 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) โˆˆ ๐‘† โ†” ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)):๐ตโŸถ๐ด โˆง (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) finSupp โˆ…)))
185169, 183, 184mpbir2and 711 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) โˆˆ ๐‘†)
186185adantr 481 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) โˆˆ ๐‘†)
187152, 186ffvelcdmd 7036 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ด โ†‘o ๐ต))
188 onelon 6342 . . . . . . . . . . . . . . . . . 18 (((๐ด โ†‘o ๐ต) โˆˆ On โˆง ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ด โ†‘o ๐ต)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ On)
189150, 187, 188syl2anc 584 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ On)
19031adantr 481 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ dom ๐‘‚ โˆˆ ฯ‰)
191 elnn 7813 . . . . . . . . . . . . . . . . . . 19 ((suc ๐‘ข โˆˆ dom ๐‘‚ โˆง dom ๐‘‚ โˆˆ ฯ‰) โ†’ suc ๐‘ข โˆˆ ฯ‰)
192143, 190, 191syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ suc ๐‘ข โˆˆ ฯ‰)
193113cantnfvalf 9601 . . . . . . . . . . . . . . . . . . 19 ๐ป:ฯ‰โŸถOn
194193ffvelcdmi 7034 . . . . . . . . . . . . . . . . . 18 (suc ๐‘ข โˆˆ ฯ‰ โ†’ (๐ปโ€˜suc ๐‘ข) โˆˆ On)
195192, 194syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐ปโ€˜suc ๐‘ข) โˆˆ On)
196 suppssdm 8108 . . . . . . . . . . . . . . . . . . . . . . 23 (๐บ supp โˆ…) โŠ† dom ๐บ
197196, 159fssdm 6688 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
198197adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐บ supp โˆ…) โŠ† ๐ต)
1992oif 9466 . . . . . . . . . . . . . . . . . . . . . . 23 ๐‘‚:dom ๐‘‚โŸถ(๐บ supp โˆ…)
200199ffvelcdmi 7034 . . . . . . . . . . . . . . . . . . . . . 22 (suc ๐‘ข โˆˆ dom ๐‘‚ โ†’ (๐‘‚โ€˜suc ๐‘ข) โˆˆ (๐บ supp โˆ…))
201143, 200syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘‚โ€˜suc ๐‘ข) โˆˆ (๐บ supp โˆ…))
202198, 201sseldd 3945 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘‚โ€˜suc ๐‘ข) โˆˆ ๐ต)
203 onelon 6342 . . . . . . . . . . . . . . . . . . . 20 ((๐ต โˆˆ On โˆง (๐‘‚โ€˜suc ๐‘ข) โˆˆ ๐ต) โ†’ (๐‘‚โ€˜suc ๐‘ข) โˆˆ On)
20410, 202, 203syl2an2r 683 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘‚โ€˜suc ๐‘ข) โˆˆ On)
205 oecl 8483 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ On โˆง (๐‘‚โ€˜suc ๐‘ข) โˆˆ On) โ†’ (๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) โˆˆ On)
2069, 204, 205syl2an2r 683 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) โˆˆ On)
207155adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ๐น:๐ตโŸถ๐ด)
208207, 202ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)) โˆˆ ๐ด)
209 onelon 6342 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ On โˆง (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)) โˆˆ ๐ด) โ†’ (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)) โˆˆ On)
2109, 208, 209syl2an2r 683 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)) โˆˆ On)
211 omcl 8482 . . . . . . . . . . . . . . . . . 18 (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) โˆˆ On โˆง (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)) โˆˆ On) โ†’ ((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) โˆˆ On)
212206, 210, 211syl2anc 584 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) โˆˆ On)
213 oaord 8494 . . . . . . . . . . . . . . . . 17 ((((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ On โˆง (๐ปโ€˜suc ๐‘ข) โˆˆ On โˆง ((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) โˆˆ On) โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข) โ†” (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))) โˆˆ (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o (๐ปโ€˜suc ๐‘ข))))
214189, 195, 212, 213syl3anc 1371 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข) โ†” (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))) โˆˆ (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o (๐ปโ€˜suc ๐‘ข))))
215 ifeq1 4490 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐นโ€˜๐‘ฅ) = โˆ… โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), โˆ…, โˆ…))
216 ifid 4526 . . . . . . . . . . . . . . . . . . . . . . 23 if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), โˆ…, โˆ…) = โˆ…
217215, 216eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . 22 ((๐นโ€˜๐‘ฅ) = โˆ… โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = โˆ…)
218 ifeq1 4490 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐นโ€˜๐‘ฅ) = โˆ… โ†’ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…) = if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), โˆ…, โˆ…))
219 ifid 4526 . . . . . . . . . . . . . . . . . . . . . . 23 if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), โˆ…, โˆ…) = โˆ…
220218, 219eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . 22 ((๐นโ€˜๐‘ฅ) = โˆ… โ†’ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…) = โˆ…)
221217, 220eqeq12d 2752 . . . . . . . . . . . . . . . . . . . . 21 ((๐นโ€˜๐‘ฅ) = โˆ… โ†’ (if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…) โ†” โˆ… = โˆ…))
222 onss 7719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐ต โˆˆ On โ†’ ๐ต โŠ† On)
22310, 222syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐œ‘ โ†’ ๐ต โŠ† On)
224223sselda 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
225224adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ๐‘ฅ โˆˆ On)
226204adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘‚โ€˜suc ๐‘ข) โˆˆ On)
227 onsseleq 6358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฅ โˆˆ On โˆง (๐‘‚โ€˜suc ๐‘ข) โˆˆ On) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข) โ†” (๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข))))
228225, 226, 227syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข) โ†” (๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข))))
229228adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข) โ†” (๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข))))
230199ffvelcdmi 7034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ข โˆˆ dom ๐‘‚ โ†’ (๐‘‚โ€˜๐‘ข) โˆˆ (๐บ supp โˆ…))
231145, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘‚โ€˜๐‘ข) โˆˆ (๐บ supp โˆ…))
232198, 231sseldd 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘‚โ€˜๐‘ข) โˆˆ ๐ต)
233 onelon 6342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐ต โˆˆ On โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐ต) โ†’ (๐‘‚โ€˜๐‘ข) โˆˆ On)
23410, 232, 233syl2an2r 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘‚โ€˜๐‘ข) โˆˆ On)
235234ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘‚โ€˜๐‘ข) โˆˆ On)
236 onsssuc 6407 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘ฅ โˆˆ On โˆง (๐‘‚โ€˜๐‘ข) โˆˆ On) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โ†” ๐‘ฅ โˆˆ suc (๐‘‚โ€˜๐‘ข)))
237225, 235, 236syl2an2r 683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โ†” ๐‘ฅ โˆˆ suc (๐‘‚โ€˜๐‘ข)))
238 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ๐‘ข โˆˆ V
239238sucid 6399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ๐‘ข โˆˆ suc ๐‘ข
24046adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)))
241 isorel 7271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)) โˆง (๐‘ข โˆˆ dom ๐‘‚ โˆง suc ๐‘ข โˆˆ dom ๐‘‚)) โ†’ (๐‘ข E suc ๐‘ข โ†” (๐‘‚โ€˜๐‘ข) E (๐‘‚โ€˜suc ๐‘ข)))
242240, 145, 143, 241syl12anc 835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘ข E suc ๐‘ข โ†” (๐‘‚โ€˜๐‘ข) E (๐‘‚โ€˜suc ๐‘ข)))
243238sucex 7741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 suc ๐‘ข โˆˆ V
244243epeli 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ข E suc ๐‘ข โ†” ๐‘ข โˆˆ suc ๐‘ข)
245 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘‚โ€˜suc ๐‘ข) โˆˆ V
246245epeli 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐‘‚โ€˜๐‘ข) E (๐‘‚โ€˜suc ๐‘ข) โ†” (๐‘‚โ€˜๐‘ข) โˆˆ (๐‘‚โ€˜suc ๐‘ข))
247242, 244, 2463bitr3g 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘ข โˆˆ suc ๐‘ข โ†” (๐‘‚โ€˜๐‘ข) โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
248239, 247mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘‚โ€˜๐‘ข) โˆˆ (๐‘‚โ€˜suc ๐‘ข))
249 eloni 6327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐‘‚โ€˜suc ๐‘ข) โˆˆ On โ†’ Ord (๐‘‚โ€˜suc ๐‘ข))
250204, 249syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ Ord (๐‘‚โ€˜suc ๐‘ข))
251 ordelsuc 7755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((๐‘‚โ€˜๐‘ข) โˆˆ On โˆง Ord (๐‘‚โ€˜suc ๐‘ข)) โ†’ ((๐‘‚โ€˜๐‘ข) โˆˆ (๐‘‚โ€˜suc ๐‘ข) โ†” suc (๐‘‚โ€˜๐‘ข) โŠ† (๐‘‚โ€˜suc ๐‘ข)))
252234, 250, 251syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐‘‚โ€˜๐‘ข) โˆˆ (๐‘‚โ€˜suc ๐‘ข) โ†” suc (๐‘‚โ€˜๐‘ข) โŠ† (๐‘‚โ€˜suc ๐‘ข)))
253248, 252mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ suc (๐‘‚โ€˜๐‘ข) โŠ† (๐‘‚โ€˜suc ๐‘ข))
254253ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ suc (๐‘‚โ€˜๐‘ข) โŠ† (๐‘‚โ€˜suc ๐‘ข))
255254sseld 3943 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โˆˆ suc (๐‘‚โ€˜๐‘ข) โ†’ ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
256237, 255sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โ†’ ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
257 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)
258240ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)))
259258, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐บ supp โˆ…))
2608, 9, 10, 11, 12, 13, 14, 15, 2cantnflem1c 9623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ (๐บ supp โˆ…))
261 f1ocnvfv2 7223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐บ supp โˆ…) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) = ๐‘ฅ)
262259, 260, 261syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) = ๐‘ฅ)
263257, 262eleqtrrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ (๐‘‚โ€˜๐‘ข) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)))
264145ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ๐‘ข โˆˆ dom ๐‘‚)
265259, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ โ—ก๐‘‚:(๐บ supp โˆ…)โŸถdom ๐‘‚)
266265, 260ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ dom ๐‘‚)
267 isorel 7271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)) โˆง (๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ dom ๐‘‚)) โ†’ (๐‘ข E (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” (๐‘‚โ€˜๐‘ข) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ))))
268258, 264, 266, 267syl12anc 835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ (๐‘ข E (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” (๐‘‚โ€˜๐‘ข) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ))))
269 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ V
270269epeli 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (๐‘ข E (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” ๐‘ข โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ))
271 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) โˆˆ V
272271epeli 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((๐‘‚โ€˜๐‘ข) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) โ†” (๐‘‚โ€˜๐‘ข) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)))
273268, 270, 2723bitr3g 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ (๐‘ข โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” (๐‘‚โ€˜๐‘ข) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ))))
274263, 273mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ๐‘ข โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ))
275 ordelon 6341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((Ord dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ dom ๐‘‚) โ†’ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ On)
27636, 266, 275sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ On)
277 eloni 6327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ On โ†’ Ord (โ—ก๐‘‚โ€˜๐‘ฅ))
278276, 277syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ Ord (โ—ก๐‘‚โ€˜๐‘ฅ))
279 ordelsuc 7755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((๐‘ข โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆง Ord (โ—ก๐‘‚โ€˜๐‘ฅ)) โ†’ (๐‘ข โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” suc ๐‘ข โŠ† (โ—ก๐‘‚โ€˜๐‘ฅ)))
280274, 278, 279syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ (๐‘ข โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” suc ๐‘ข โŠ† (โ—ก๐‘‚โ€˜๐‘ฅ)))
281274, 280mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ suc ๐‘ข โŠ† (โ—ก๐‘‚โ€˜๐‘ฅ))
282143ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ suc ๐‘ข โˆˆ dom ๐‘‚)
28336, 282, 131sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ suc ๐‘ข โˆˆ On)
284 ontri1 6351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((suc ๐‘ข โˆˆ On โˆง (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ On) โ†’ (suc ๐‘ข โŠ† (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” ยฌ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ suc ๐‘ข))
285283, 276, 284syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ (suc ๐‘ข โŠ† (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” ยฌ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ suc ๐‘ข))
286281, 285mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ยฌ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ suc ๐‘ข)
287 isorel 7271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)) โˆง ((โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ dom ๐‘‚ โˆง suc ๐‘ข โˆˆ dom ๐‘‚)) โ†’ ((โ—ก๐‘‚โ€˜๐‘ฅ) E suc ๐‘ข โ†” (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) E (๐‘‚โ€˜suc ๐‘ข)))
288258, 266, 282, 287syl12anc 835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ((โ—ก๐‘‚โ€˜๐‘ฅ) E suc ๐‘ข โ†” (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) E (๐‘‚โ€˜suc ๐‘ข)))
289243epeli 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((โ—ก๐‘‚โ€˜๐‘ฅ) E suc ๐‘ข โ†” (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ suc ๐‘ข)
290245epeli 5539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) E (๐‘‚โ€˜suc ๐‘ข) โ†” (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) โˆˆ (๐‘‚โ€˜suc ๐‘ข))
291288, 289, 2903bitr3g 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ((โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ suc ๐‘ข โ†” (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
292262eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ((๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) โˆˆ (๐‘‚โ€˜suc ๐‘ข) โ†” ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
293291, 292bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ((โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ suc ๐‘ข โ†” ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
294286, 293mtbid 323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ)) โ†’ ยฌ ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข))
295294expr 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ ((๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ โ†’ ยฌ ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
296295con2d 134 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข) โ†’ ยฌ (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ))
297 ontri1 6351 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘ฅ โˆˆ On โˆง (๐‘‚โ€˜๐‘ข) โˆˆ On) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โ†” ยฌ (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ))
298225, 235, 297syl2an2r 683 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โ†” ยฌ (๐‘‚โ€˜๐‘ข) โˆˆ ๐‘ฅ))
299296, 298sylibrd 258 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข) โ†’ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)))
300256, 299impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โ†” ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
301300orbi1d 915 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ ((๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โˆจ ๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข)) โ†” (๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข))))
302229, 301bitr4d 281 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข) โ†” (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โˆจ ๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข))))
303 orcom 868 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โˆจ ๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข)) โ†” (๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)))
304302, 303bitrdi 286 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข) โ†” (๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข))))
305304ifbid 4509 . . . . . . . . . . . . . . . . . . . . 21 ((((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โˆง (๐นโ€˜๐‘ฅ) โ‰  โˆ…) โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…))
306 eqidd 2737 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ โˆ… = โˆ…)
307221, 305, 306pm2.61ne 3030 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…))
308307mpteq2dva 5205 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…)))
309308fveq2d 6846 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) = ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…))))
310 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐นโ€˜๐‘ฅ) โˆˆ V
311310, 175ifex 4536 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ V
312311a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ V)
313312ralrimivw 3147 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ โˆ€๐‘ฅ โˆˆ ๐ต if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ V)
314 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))
315314fnmpt 6641 . . . . . . . . . . . . . . . . . . . . . . . 24 (โˆ€๐‘ฅ โˆˆ ๐ต if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ V โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) Fn ๐ต)
316313, 315syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) Fn ๐ต)
317175a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ โˆ… โˆˆ V)
318 suppvalfn 8100 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) supp โˆ…) = {๐‘ฆ โˆˆ ๐ต โˆฃ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ) โ‰  โˆ…})
319 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . 25 โ„ฒ๐‘ฆ๐ต
320 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . 25 โ„ฒ๐‘ฅ๐ต
321 nffvmpt1 6853 . . . . . . . . . . . . . . . . . . . . . . . . . 26 โ„ฒ๐‘ฅ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ)
322 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 โ„ฒ๐‘ฅโˆ…
323321, 322nfne 3045 . . . . . . . . . . . . . . . . . . . . . . . . 25 โ„ฒ๐‘ฅ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ) โ‰  โˆ…
324 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . . . 25 โ„ฒ๐‘ฆ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ) โ‰  โˆ…
325 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ = ๐‘ฅ โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ) = ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ))
326325neeq1d 3003 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ = ๐‘ฅ โ†’ (((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ) โ‰  โˆ… โ†” ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ) โ‰  โˆ…))
327319, 320, 323, 324, 326cbvrabw 3439 . . . . . . . . . . . . . . . . . . . . . . . 24 {๐‘ฆ โˆˆ ๐ต โˆฃ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ) โ‰  โˆ…} = {๐‘ฅ โˆˆ ๐ต โˆฃ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ) โ‰  โˆ…}
328318, 327eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) Fn ๐ต โˆง ๐ต โˆˆ On โˆง โˆ… โˆˆ V) โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) supp โˆ…) = {๐‘ฅ โˆˆ ๐ต โˆฃ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ) โ‰  โˆ…})
329316, 148, 317, 328syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) supp โˆ…) = {๐‘ฅ โˆˆ ๐ต โˆฃ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ) โ‰  โˆ…})
330 eqidd 2737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))
331311a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ V)
332330, 331fvmpt2d 6961 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ) = if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))
333332neeq1d 3003 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ) โ‰  โˆ… โ†” if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ…))
334331biantrurd 533 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ… โ†” (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ V โˆง if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ…)))
335 dif1o 8446 . . . . . . . . . . . . . . . . . . . . . . . . 25 (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ (V โˆ– 1o) โ†” (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ V โˆง if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ…))
336334, 335bitr4di 288 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ… โ†” if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ (V โˆ– 1o)))
337333, 336bitrd 278 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ) โ‰  โˆ… โ†” if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ (V โˆ– 1o)))
338337rabbidva 3414 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ {๐‘ฅ โˆˆ ๐ต โˆฃ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฅ) โ‰  โˆ…} = {๐‘ฅ โˆˆ ๐ต โˆฃ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ (V โˆ– 1o)})
339329, 338eqtrd 2776 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) supp โˆ…) = {๐‘ฅ โˆˆ ๐ต โˆฃ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ (V โˆ– 1o)})
340311, 335mpbiran 707 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ (V โˆ– 1o) โ†” if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ…)
341 ifeq1 4490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐นโ€˜๐‘ฅ) = โˆ… โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), โˆ…, โˆ…))
342341, 179eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐นโ€˜๐‘ฅ) = โˆ… โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = โˆ…)
343342necon3i 2976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ… โ†’ (๐นโ€˜๐‘ฅ) โ‰  โˆ…)
344 iffalse 4495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ยฌ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = โˆ…)
345344necon1ai 2971 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ… โ†’ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข))
346343, 345jca 512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ… โ†’ ((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)))
347256expimpd 454 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (((๐นโ€˜๐‘ฅ) โ‰  โˆ… โˆง ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)) โ†’ ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
348346, 347syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โ‰  โˆ… โ†’ ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
349340, 348biimtrid 241 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ (V โˆ– 1o) โ†’ ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
3503493impia 1117 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โˆง ๐‘ฅ โˆˆ ๐ต โˆง if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ (V โˆ– 1o)) โ†’ ๐‘ฅ โˆˆ (๐‘‚โ€˜suc ๐‘ข))
351350rabssdv 4032 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ {๐‘ฅ โˆˆ ๐ต โˆฃ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) โˆˆ (V โˆ– 1o)} โŠ† (๐‘‚โ€˜suc ๐‘ข))
352339, 351eqsstrd 3982 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)) supp โˆ…) โŠ† (๐‘‚โ€˜suc ๐‘ข))
353 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โ†” ๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข)))
354 sseq1 3969 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข) โ†” ๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข)))
355353, 354orbi12d 917 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)) โ†” (๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข))))
356 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ = ๐‘ฆ โ†’ (๐นโ€˜๐‘ฅ) = (๐นโ€˜๐‘ฆ))
357355, 356ifbieq1d 4510 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ = ๐‘ฆ โ†’ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…) = if((๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฆ), โˆ…))
358357cbvmptv 5218 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ ๐ต โ†ฆ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฆ โˆˆ ๐ต โ†ฆ if((๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฆ), โˆ…))
359 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข) โ†’ (๐นโ€˜๐‘ฆ) = (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)))
360359adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฆ โˆˆ ๐ต โˆง ๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข)) โ†’ (๐นโ€˜๐‘ฆ) = (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)))
361360ifeq1da 4517 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ ๐ต โ†’ if(๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฆ), ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ)) = if(๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)), ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ)))
362354, 356ifbieq1d 4510 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ = ๐‘ฆ โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฆ), โˆ…))
363 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐นโ€˜๐‘ฆ) โˆˆ V
364363, 175ifex 4536 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฆ), โˆ…) โˆˆ V
365362, 314, 364fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ โˆˆ ๐ต โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ) = if(๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฆ), โˆ…))
366365ifeq2d 4506 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ โˆˆ ๐ต โ†’ if(๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฆ), ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ)) = if(๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฆ), if(๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฆ), โˆ…)))
367 ifor 4540 . . . . . . . . . . . . . . . . . . . . . . . 24 if((๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฆ), โˆ…) = if(๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฆ), if(๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฆ), โˆ…))
368366, 367eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ ๐ต โ†’ if(๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฆ), ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ)) = if((๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฆ), โˆ…))
369361, 368eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ ๐ต โ†’ if(๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)), ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ)) = if((๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฆ), โˆ…))
370369mpteq2ia 5208 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ ๐ต โ†ฆ if(๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)), ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ))) = (๐‘ฆ โˆˆ ๐ต โ†ฆ if((๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฆ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฆ), โˆ…))
371358, 370eqtr4i 2767 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โˆˆ ๐ต โ†ฆ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฆ โˆˆ ๐ต โ†ฆ if(๐‘ฆ = (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)), ((๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))โ€˜๐‘ฆ)))
3728, 151, 148, 186, 202, 208, 352, 371cantnfp1 9617 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐‘ฅ โˆˆ ๐ต โ†ฆ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…)) โˆˆ ๐‘† โˆง ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…))) = (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))))))
373372simprd 496 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if((๐‘ฅ = (๐‘‚โ€˜suc ๐‘ข) โˆจ ๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข)), (๐นโ€˜๐‘ฅ), โˆ…))) = (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))))
374309, 373eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) = (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))))
3758, 9, 10, 2, 13, 113cantnfsuc 9606 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง suc ๐‘ข โˆˆ ฯ‰) โ†’ (๐ปโ€˜suc suc ๐‘ข) = (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐บโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o (๐ปโ€˜suc ๐‘ข)))
376192, 375syldan 591 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐ปโ€˜suc suc ๐‘ข) = (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐บโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o (๐ปโ€˜suc ๐‘ข)))
377160simp3d 1144 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ โˆ€๐‘ค โˆˆ ๐ต (๐‘‹ โˆˆ ๐‘ค โ†’ (๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค)))
378377adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ โˆ€๐‘ค โˆˆ ๐ต (๐‘‹ โˆˆ ๐‘ค โ†’ (๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค)))
379108adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) = ๐‘‹)
380136adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ๐‘ข โˆˆ On)
381 onsssuc 6407 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On โˆง ๐‘ข โˆˆ On) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข โ†” (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข))
382129, 380, 381syl2an2r 683 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข โ†” (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข))
383146, 382mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข)
38452adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚)
385 isorel 7271 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)) โˆง ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚ โˆง suc ๐‘ข โˆˆ dom ๐‘‚)) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) E suc ๐‘ข โ†” (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) E (๐‘‚โ€˜suc ๐‘ข)))
386240, 384, 143, 385syl12anc 835 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) E suc ๐‘ข โ†” (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) E (๐‘‚โ€˜suc ๐‘ข)))
387243epeli 5539 . . . . . . . . . . . . . . . . . . . . . . . 24 ((โ—ก๐‘‚โ€˜๐‘‹) E suc ๐‘ข โ†” (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข)
388245epeli 5539 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) E (๐‘‚โ€˜suc ๐‘ข) โ†” (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โˆˆ (๐‘‚โ€˜suc ๐‘ข))
389386, 387, 3883bitr3g 312 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข โ†” (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
390383, 389mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โˆˆ (๐‘‚โ€˜suc ๐‘ข))
391379, 390eqeltrrd 2838 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ๐‘‹ โˆˆ (๐‘‚โ€˜suc ๐‘ข))
392 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ค = (๐‘‚โ€˜suc ๐‘ข) โ†’ (๐‘‹ โˆˆ ๐‘ค โ†” ๐‘‹ โˆˆ (๐‘‚โ€˜suc ๐‘ข)))
393 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ค = (๐‘‚โ€˜suc ๐‘ข) โ†’ (๐นโ€˜๐‘ค) = (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)))
394 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ค = (๐‘‚โ€˜suc ๐‘ข) โ†’ (๐บโ€˜๐‘ค) = (๐บโ€˜(๐‘‚โ€˜suc ๐‘ข)))
395393, 394eqeq12d 2752 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ค = (๐‘‚โ€˜suc ๐‘ข) โ†’ ((๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค) โ†” (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)) = (๐บโ€˜(๐‘‚โ€˜suc ๐‘ข))))
396392, 395imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ค = (๐‘‚โ€˜suc ๐‘ข) โ†’ ((๐‘‹ โˆˆ ๐‘ค โ†’ (๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค)) โ†” (๐‘‹ โˆˆ (๐‘‚โ€˜suc ๐‘ข) โ†’ (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)) = (๐บโ€˜(๐‘‚โ€˜suc ๐‘ข)))))
397396rspcv 3577 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘‚โ€˜suc ๐‘ข) โˆˆ ๐ต โ†’ (โˆ€๐‘ค โˆˆ ๐ต (๐‘‹ โˆˆ ๐‘ค โ†’ (๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค)) โ†’ (๐‘‹ โˆˆ (๐‘‚โ€˜suc ๐‘ข) โ†’ (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)) = (๐บโ€˜(๐‘‚โ€˜suc ๐‘ข)))))
398202, 378, 391, 397syl3c 66 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข)) = (๐บโ€˜(๐‘‚โ€˜suc ๐‘ข)))
399398oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ ((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) = ((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐บโ€˜(๐‘‚โ€˜suc ๐‘ข))))
400399oveq1d 7372 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o (๐ปโ€˜suc ๐‘ข)) = (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐บโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o (๐ปโ€˜suc ๐‘ข)))
401376, 400eqtr4d 2779 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (๐ปโ€˜suc suc ๐‘ข) = (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o (๐ปโ€˜suc ๐‘ข)))
402374, 401eleq12d 2831 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข) โ†” (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))) โˆˆ (((๐ด โ†‘o (๐‘‚โ€˜suc ๐‘ข)) ยทo (๐นโ€˜(๐‘‚โ€˜suc ๐‘ข))) +o (๐ปโ€˜suc ๐‘ข))))
403214, 402bitr4d 281 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข) โ†” ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข)))
404403biimpd 228 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข)))
405147, 404embantd 59 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข)) โ†’ (((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข)))
406405expr 457 . . . . . . . . . . . 12 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข โ†’ (((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข))))
407140, 406sylbird 259 . . . . . . . . . . 11 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข โ†’ (((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข))))
408 fveq2 6842 . . . . . . . . . . . . . . . . . . 19 ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) = (๐‘‚โ€˜suc ๐‘ข))
409408sseq2d 3976 . . . . . . . . . . . . . . . . . 18 ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” ๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข)))
410409ifbid 4509 . . . . . . . . . . . . . . . . 17 ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…) = if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))
411410mpteq2dv 5207 . . . . . . . . . . . . . . . 16 ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…)))
412411fveq2d 6846 . . . . . . . . . . . . . . 15 ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…))) = ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))))
413 suceq 6383 . . . . . . . . . . . . . . . 16 ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ suc (โ—ก๐‘‚โ€˜๐‘‹) = suc suc ๐‘ข)
414413fveq2d 6846 . . . . . . . . . . . . . . 15 ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ (๐ปโ€˜suc (โ—ก๐‘‚โ€˜๐‘‹)) = (๐ปโ€˜suc suc ๐‘ข))
415412, 414eleq12d 2831 . . . . . . . . . . . . . 14 ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ (((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc (โ—ก๐‘‚โ€˜๐‘‹)) โ†” ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข)))
416115, 415syl5ibcom 244 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข)))
417416adantr 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข)))
418417a1dd 50 . . . . . . . . . . 11 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข โ†’ (((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข))))
419407, 418jaod 857 . . . . . . . . . 10 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ (((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ suc ๐‘ข โˆจ (โ—ก๐‘‚โ€˜๐‘‹) = suc ๐‘ข) โ†’ (((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข))))
420134, 419sylbid 239 . . . . . . . . 9 ((๐œ‘ โˆง suc ๐‘ข โˆˆ dom ๐‘‚) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† suc ๐‘ข โ†’ (((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข))))
421420expimpd 454 . . . . . . . 8 (๐œ‘ โ†’ ((suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† suc ๐‘ข) โ†’ (((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข))))
422421com23 86 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)) โ†’ ((suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† suc ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข))))
423422a1i 11 . . . . . 6 (๐‘ข โˆˆ ฯ‰ โ†’ (๐œ‘ โ†’ (((๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ข)) โ†’ ((suc ๐‘ข โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† suc ๐‘ข) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜suc ๐‘ข), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc suc ๐‘ข)))))
42482, 94, 106, 127, 423finds2 7837 . . . . 5 (๐‘ฆ โˆˆ ฯ‰ โ†’ (๐œ‘ โ†’ ((๐‘ฆ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† ๐‘ฆ) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜๐‘ฆ), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc ๐‘ฆ))))
42570, 424vtoclga 3534 . . . 4 (โˆช dom ๐‘‚ โˆˆ ฯ‰ โ†’ (๐œ‘ โ†’ ((โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆช dom ๐‘‚))))
42657, 425mpcom 38 . . 3 (๐œ‘ โ†’ ((โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚) โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆช dom ๐‘‚)))
42744, 54, 426mp2and 697 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))) โˆˆ (๐ปโ€˜suc โˆช dom ๐‘‚))
428155feqmptd 6910 . . . 4 (๐œ‘ โ†’ ๐น = (๐‘ฅ โˆˆ ๐ต โ†ฆ (๐นโ€˜๐‘ฅ)))
429 eqeq2 2748 . . . . . 6 ((๐นโ€˜๐‘ฅ) = if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…) โ†’ ((๐นโ€˜๐‘ฅ) = (๐นโ€˜๐‘ฅ) โ†” (๐นโ€˜๐‘ฅ) = if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…)))
430 eqeq2 2748 . . . . . 6 (โˆ… = if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…) โ†’ ((๐นโ€˜๐‘ฅ) = โˆ… โ†” (๐นโ€˜๐‘ฅ) = if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…)))
431 eqidd 2737 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚)) โ†’ (๐นโ€˜๐‘ฅ) = (๐นโ€˜๐‘ฅ))
432199ffvelcdmi 7034 . . . . . . . . . . . . . 14 (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…))
43344, 432syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐บ supp โˆ…))
434197, 433sseldd 3945 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐ต)
435 onelon 6342 . . . . . . . . . . . 12 ((๐ต โˆˆ On โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐ต) โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On)
43610, 434, 435syl2anc 584 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On)
437436adantr 481 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On)
438 ontri1 6351 . . . . . . . . . 10 ((๐‘ฅ โˆˆ On โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚) โ†” ยฌ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ))
439224, 437, 438syl2anc 584 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚) โ†” ยฌ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ))
440439con2bid 354 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ โ†” ยฌ ๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚)))
441 simprl 769 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ ๐ต)
442377adantr 481 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ โˆ€๐‘ค โˆˆ ๐ต (๐‘‹ โˆˆ ๐‘ค โ†’ (๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค)))
443 eloni 6327 . . . . . . . . . . . . . . . . . 18 ((โ—ก๐‘‚โ€˜๐‘‹) โˆˆ On โ†’ Ord (โ—ก๐‘‚โ€˜๐‘‹))
444129, 443syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ Ord (โ—ก๐‘‚โ€˜๐‘‹))
445 orduni 7724 . . . . . . . . . . . . . . . . . 18 (Ord dom ๐‘‚ โ†’ Ord โˆช dom ๐‘‚)
44636, 445ax-mp 5 . . . . . . . . . . . . . . . . 17 Ord โˆช dom ๐‘‚
447 ordtri1 6350 . . . . . . . . . . . . . . . . 17 ((Ord (โ—ก๐‘‚โ€˜๐‘‹) โˆง Ord โˆช dom ๐‘‚) โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹)))
448444, 446, 447sylancl 586 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ—ก๐‘‚โ€˜๐‘‹) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹)))
44954, 448mpbid 231 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹))
450 isorel 7271 . . . . . . . . . . . . . . . . . 18 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)) โˆง (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ dom ๐‘‚)) โ†’ (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
45146, 44, 52, 450syl12anc 835 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
452 fvex 6855 . . . . . . . . . . . . . . . . . 18 (โ—ก๐‘‚โ€˜๐‘‹) โˆˆ V
453452epeli 5539 . . . . . . . . . . . . . . . . 17 (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘‹) โ†” โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹))
454 fvex 6855 . . . . . . . . . . . . . . . . . 18 (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โˆˆ V
455454epeli 5539 . . . . . . . . . . . . . . . . 17 ((๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)))
456451, 453, 4553bitr3g 312 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹))))
457108eleq2d 2823 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘‹)) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
458456, 457bitrd 278 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘‹) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
459449, 458mtbid 323 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ยฌ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹)
460 onelon 6342 . . . . . . . . . . . . . . . 16 ((๐ต โˆˆ On โˆง ๐‘‹ โˆˆ ๐ต) โ†’ ๐‘‹ โˆˆ On)
46110, 161, 460syl2anc 584 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘‹ โˆˆ On)
462 ontri1 6351 . . . . . . . . . . . . . . 15 ((๐‘‹ โˆˆ On โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ On) โ†’ (๐‘‹ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚) โ†” ยฌ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
463461, 436, 462syl2anc 584 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘‹ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚) โ†” ยฌ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘‹))
464459, 463mpbird 256 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘‹ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚))
465464adantr 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ ๐‘‹ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚))
466 simprr 771 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)
467224adantrr 715 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ On)
468 ontr2 6364 . . . . . . . . . . . . 13 ((๐‘‹ โˆˆ On โˆง ๐‘ฅ โˆˆ On) โ†’ ((๐‘‹ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚) โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ) โ†’ ๐‘‹ โˆˆ ๐‘ฅ))
469461, 467, 468syl2an2r 683 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ ((๐‘‹ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚) โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ) โ†’ ๐‘‹ โˆˆ ๐‘ฅ))
470465, 466, 469mp2and 697 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ ๐‘‹ โˆˆ ๐‘ฅ)
471 eleq2 2826 . . . . . . . . . . . . 13 (๐‘ค = ๐‘ฅ โ†’ (๐‘‹ โˆˆ ๐‘ค โ†” ๐‘‹ โˆˆ ๐‘ฅ))
472 fveq2 6842 . . . . . . . . . . . . . 14 (๐‘ค = ๐‘ฅ โ†’ (๐นโ€˜๐‘ค) = (๐นโ€˜๐‘ฅ))
473 fveq2 6842 . . . . . . . . . . . . . 14 (๐‘ค = ๐‘ฅ โ†’ (๐บโ€˜๐‘ค) = (๐บโ€˜๐‘ฅ))
474472, 473eqeq12d 2752 . . . . . . . . . . . . 13 (๐‘ค = ๐‘ฅ โ†’ ((๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค) โ†” (๐นโ€˜๐‘ฅ) = (๐บโ€˜๐‘ฅ)))
475471, 474imbi12d 344 . . . . . . . . . . . 12 (๐‘ค = ๐‘ฅ โ†’ ((๐‘‹ โˆˆ ๐‘ค โ†’ (๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค)) โ†” (๐‘‹ โˆˆ ๐‘ฅ โ†’ (๐นโ€˜๐‘ฅ) = (๐บโ€˜๐‘ฅ))))
476475rspcv 3577 . . . . . . . . . . 11 (๐‘ฅ โˆˆ ๐ต โ†’ (โˆ€๐‘ค โˆˆ ๐ต (๐‘‹ โˆˆ ๐‘ค โ†’ (๐นโ€˜๐‘ค) = (๐บโ€˜๐‘ค)) โ†’ (๐‘‹ โˆˆ ๐‘ฅ โ†’ (๐นโ€˜๐‘ฅ) = (๐บโ€˜๐‘ฅ))))
477441, 442, 470, 476syl3c 66 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ (๐นโ€˜๐‘ฅ) = (๐บโ€˜๐‘ฅ))
478466adantr 481 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)
47946ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)))
48044ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ โˆช dom ๐‘‚ โˆˆ dom ๐‘‚)
48151ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ โ—ก๐‘‚:(๐บ supp โˆ…)โŸถdom ๐‘‚)
482 ffvelcdm 7032 . . . . . . . . . . . . . . . . . 18 ((โ—ก๐‘‚:(๐บ supp โˆ…)โŸถdom ๐‘‚ โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ dom ๐‘‚)
483481, 482sylancom 588 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ dom ๐‘‚)
484 isorel 7271 . . . . . . . . . . . . . . . . 17 ((๐‘‚ Isom E , E (dom ๐‘‚, (๐บ supp โˆ…)) โˆง (โˆช dom ๐‘‚ โˆˆ dom ๐‘‚ โˆง (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ dom ๐‘‚)) โ†’ (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ))))
485479, 480, 483, 484syl12anc 835 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ))))
486269epeli 5539 . . . . . . . . . . . . . . . 16 (โˆช dom ๐‘‚ E (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ))
487271epeli 5539 . . . . . . . . . . . . . . . 16 ((๐‘‚โ€˜โˆช dom ๐‘‚) E (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)))
488485, 486, 4873bitr3g 312 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ))))
48948ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ๐‘‚:dom ๐‘‚โ€“1-1-ontoโ†’(๐บ supp โˆ…))
490489, 261sylancom 588 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) = ๐‘ฅ)
491490eleq2d 2823 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ (๐‘‚โ€˜(โ—ก๐‘‚โ€˜๐‘ฅ)) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ))
492488, 491bitrd 278 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ) โ†” (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ))
493478, 492mpbird 256 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ))
494 elssuni 4898 . . . . . . . . . . . . . . 15 ((โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ dom ๐‘‚ โ†’ (โ—ก๐‘‚โ€˜๐‘ฅ) โŠ† โˆช dom ๐‘‚)
495483, 494syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โ—ก๐‘‚โ€˜๐‘ฅ) โŠ† โˆช dom ๐‘‚)
49636, 483, 275sylancr 587 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ (โ—ก๐‘‚โ€˜๐‘ฅ) โˆˆ On)
497496, 277syl 17 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ Ord (โ—ก๐‘‚โ€˜๐‘ฅ))
498 ordtri1 6350 . . . . . . . . . . . . . . 15 ((Ord (โ—ก๐‘‚โ€˜๐‘ฅ) โˆง Ord โˆช dom ๐‘‚) โ†’ ((โ—ก๐‘‚โ€˜๐‘ฅ) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ)))
499497, 446, 498sylancl 586 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ((โ—ก๐‘‚โ€˜๐‘ฅ) โŠ† โˆช dom ๐‘‚ โ†” ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ)))
500495, 499mpbid 231 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โˆง ๐‘ฅ โˆˆ (๐บ supp โˆ…)) โ†’ ยฌ โˆช dom ๐‘‚ โˆˆ (โ—ก๐‘‚โ€˜๐‘ฅ))
501493, 500pm2.65da 815 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ ยฌ ๐‘ฅ โˆˆ (๐บ supp โˆ…))
502441, 501eldifd 3921 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ ๐‘ฅ โˆˆ (๐ต โˆ– (๐บ supp โˆ…)))
503 ssidd 3967 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐บ supp โˆ…) โŠ† (๐บ supp โˆ…))
504159, 503, 10, 176suppssr 8127 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (๐ต โˆ– (๐บ supp โˆ…))) โ†’ (๐บโ€˜๐‘ฅ) = โˆ…)
505502, 504syldan 591 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ (๐บโ€˜๐‘ฅ) = โˆ…)
506477, 505eqtrd 2776 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง (๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ)) โ†’ (๐นโ€˜๐‘ฅ) = โˆ…)
507506expr 457 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ((๐‘‚โ€˜โˆช dom ๐‘‚) โˆˆ ๐‘ฅ โ†’ (๐นโ€˜๐‘ฅ) = โˆ…))
508440, 507sylbird 259 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (ยฌ ๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚) โ†’ (๐นโ€˜๐‘ฅ) = โˆ…))
509508imp 407 . . . . . 6 (((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โˆง ยฌ ๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚)) โ†’ (๐นโ€˜๐‘ฅ) = โˆ…)
510429, 430, 431, 509ifbothda 4524 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ (๐นโ€˜๐‘ฅ) = if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))
511510mpteq2dva 5205 . . . 4 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ๐ต โ†ฆ (๐นโ€˜๐‘ฅ)) = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…)))
512428, 511eqtrd 2776 . . 3 (๐œ‘ โ†’ ๐น = (๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…)))
513512fveq2d 6846 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) = ((๐ด CNF ๐ต)โ€˜(๐‘ฅ โˆˆ ๐ต โ†ฆ if(๐‘ฅ โŠ† (๐‘‚โ€˜โˆช dom ๐‘‚), (๐นโ€˜๐‘ฅ), โˆ…))))
5148, 9, 10, 2, 13, 113cantnfval 9604 . . 3 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = (๐ปโ€˜dom ๐‘‚))
51543fveq2d 6846 . . 3 (๐œ‘ โ†’ (๐ปโ€˜dom ๐‘‚) = (๐ปโ€˜suc โˆช dom ๐‘‚))
516514, 515eqtrd 2776 . 2 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐บ) = (๐ปโ€˜suc โˆช dom ๐‘‚))
517427, 513, 5163eltr4d 2852 1 (๐œ‘ โ†’ ((๐ด CNF ๐ต)โ€˜๐น) โˆˆ ((๐ด CNF ๐ต)โ€˜๐บ))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2943  โˆ€wral 3064  โˆƒwrex 3073  {crab 3407  Vcvv 3445   โˆ– cdif 3907   โŠ† wss 3910  โˆ…c0 4282  ifcif 4486  โˆช cuni 4865   class class class wbr 5105  {copab 5167   โ†ฆ cmpt 5188  Tr wtr 5222   E cep 5536   We wwe 5587  โ—กccnv 5632  dom cdm 5633  Ord word 6316  Oncon0 6317  Lim wlim 6318  suc csuc 6319  Fun wfun 6490   Fn wfn 6491  โŸถwf 6492  โ€“1-1-ontoโ†’wf1o 6495  โ€˜cfv 6496   Isom wiso 6497  (class class class)co 7357   โˆˆ cmpo 7359  ฯ‰com 7802   supp csupp 8092  seqฯ‰cseqom 8393  1oc1o 8405   +o coa 8409   ยทo comu 8410   โ†‘o coe 8411   โ‰ˆ cen 8880   finSupp cfsupp 9305  OrdIsocoi 9445   CNF ccnf 9597
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-seqom 8394  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-oexp 8418  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-oi 9446  df-cnf 9598
This theorem is referenced by:  cantnf  9629
  Copyright terms: Public domain W3C validator