Metamath Proof Explorer

Theorem cantnfresb

Description: A Cantor normal form which sums to less than a certain power has only zeros for larger components. (Contributed by RP, 3-Feb-2025)

Ref Expression
Assertion cantnfresb ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→ACNFB⁡F∈A↑𝑜C↔∀x∈B∖CF⁡x=∅

Proof

Step Hyp Ref Expression
1 eqid ⊢dom⁡ACNFB=dom⁡ACNFB
2 eldifi ⊢A∈On∖2𝑜→A∈On
3 2 adantr ⊢A∈On∖2𝑜∧B∈On→A∈On
4 simpr ⊢A∈On∖2𝑜∧B∈On→B∈On
5 eqid ⊢ab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡x=ab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡x
6 1 3 4 5 cantnf ⊢A∈On∖2𝑜∧B∈On→ACNFBIsomab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡x,Edom⁡ACNFBA↑𝑜B
7 6 adantr ⊢A∈On∖2𝑜∧B∈On∧F∈dom⁡ACNFB→ACNFBIsomab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡x,Edom⁡ACNFBA↑𝑜B
8 simpr ⊢A∈On∖2𝑜∧B∈On∧F∈dom⁡ACNFB→F∈dom⁡ACNFB
9 ondif2 ⊢A∈On∖2𝑜↔A∈On∧1𝑜∈A
10 9 simprbi ⊢A∈On∖2𝑜→1𝑜∈A
11 dif20el ⊢A∈On∖2𝑜→∅∈A
12 10 11 ifcld ⊢A∈On∖2𝑜→ify=C1𝑜∅∈A
13 12 ad2antrr ⊢A∈On∖2𝑜∧B∈On∧y∈B→ify=C1𝑜∅∈A
14 13 fmpttd ⊢A∈On∖2𝑜∧B∈On→y∈B⟼ify=C1𝑜∅:B⟶A
15 11 adantr ⊢A∈On∖2𝑜∧B∈On→∅∈A
16 eqid ⊢y∈B⟼ify=C1𝑜∅=y∈B⟼ify=C1𝑜∅
17 4 15 16 sniffsupp ⊢A∈On∖2𝑜∧B∈On→finSupp∅⁡y∈B⟼ify=C1𝑜∅
18 1 3 4 cantnfs ⊢A∈On∖2𝑜∧B∈On→y∈B⟼ify=C1𝑜∅∈dom⁡ACNFB↔y∈B⟼ify=C1𝑜∅:B⟶A∧finSupp∅⁡y∈B⟼ify=C1𝑜∅
19 14 17 18 mpbir2and ⊢A∈On∖2𝑜∧B∈On→y∈B⟼ify=C1𝑜∅∈dom⁡ACNFB
20 19 adantr ⊢A∈On∖2𝑜∧B∈On∧F∈dom⁡ACNFB→y∈B⟼ify=C1𝑜∅∈dom⁡ACNFB
21 isorel ⊢ACNFBIsomab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡x,Edom⁡ACNFBA↑𝑜B∧F∈dom⁡ACNFB∧y∈B⟼ify=C1𝑜∅∈dom⁡ACNFB→Fab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡xy∈B⟼ify=C1𝑜∅↔ACNFB⁡FEACNFB⁡y∈B⟼ify=C1𝑜∅
22 7 8 20 21 syl12anc ⊢A∈On∖2𝑜∧B∈On∧F∈dom⁡ACNFB→Fab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡xy∈B⟼ify=C1𝑜∅↔ACNFB⁡FEACNFB⁡y∈B⟼ify=C1𝑜∅
23 22 adantrl ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→Fab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡xy∈B⟼ify=C1𝑜∅↔ACNFB⁡FEACNFB⁡y∈B⟼ify=C1𝑜∅
24 23 adantr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧C∈B→Fab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡xy∈B⟼ify=C1𝑜∅↔ACNFB⁡FEACNFB⁡y∈B⟼ify=C1𝑜∅
25 fvexd ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧C∈B→ACNFB⁡y∈B⟼ify=C1𝑜∅∈V
26 epelg ⊢ACNFB⁡y∈B⟼ify=C1𝑜∅∈V→ACNFB⁡FEACNFB⁡y∈B⟼ify=C1𝑜∅↔ACNFB⁡F∈ACNFB⁡y∈B⟼ify=C1𝑜∅
27 25 26 syl ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧C∈B→ACNFB⁡FEACNFB⁡y∈B⟼ify=C1𝑜∅↔ACNFB⁡F∈ACNFB⁡y∈B⟼ify=C1𝑜∅
28 2 ad2antrr ⊢A∈On∖2𝑜∧B∈On∧C∈B→A∈On
29 simplr ⊢A∈On∖2𝑜∧B∈On∧C∈B→B∈On
30 fconst6g ⊢∅∈A→B×∅:B⟶A
31 11 30 syl ⊢A∈On∖2𝑜→B×∅:B⟶A
32 31 adantr ⊢A∈On∖2𝑜∧B∈On→B×∅:B⟶A
33 4 15 fczfsuppd ⊢A∈On∖2𝑜∧B∈On→finSupp∅⁡B×∅
34 1 3 4 cantnfs ⊢A∈On∖2𝑜∧B∈On→B×∅∈dom⁡ACNFB↔B×∅:B⟶A∧finSupp∅⁡B×∅
35 32 33 34 mpbir2and ⊢A∈On∖2𝑜∧B∈On→B×∅∈dom⁡ACNFB
36 35 adantr ⊢A∈On∖2𝑜∧B∈On∧C∈B→B×∅∈dom⁡ACNFB
37 simpr ⊢A∈On∖2𝑜∧B∈On∧C∈B→C∈B
38 10 ad2antrr ⊢A∈On∖2𝑜∧B∈On∧C∈B→1𝑜∈A
39 fczsupp0 ⊢B×∅supp∅=∅
40 0ss ⊢∅⊆C
41 39 40 eqsstri ⊢B×∅supp∅⊆C
42 41 a1i ⊢A∈On∖2𝑜∧B∈On∧C∈B→B×∅supp∅⊆C
43 0ex ⊢∅∈V
44 43 fvconst2 ⊢y∈B→B×∅⁡y=∅
45 44 ifeq2d ⊢y∈B→ify=C1𝑜B×∅⁡y=ify=C1𝑜∅
46 45 mpteq2ia ⊢y∈B⟼ify=C1𝑜B×∅⁡y=y∈B⟼ify=C1𝑜∅
47 46 eqcomi ⊢y∈B⟼ify=C1𝑜∅=y∈B⟼ify=C1𝑜B×∅⁡y
48 1 28 29 36 37 38 42 47 cantnfp1 ⊢A∈On∖2𝑜∧B∈On∧C∈B→y∈B⟼ify=C1𝑜∅∈dom⁡ACNFB∧ACNFB⁡y∈B⟼ify=C1𝑜∅=A↑𝑜C⋅𝑜1𝑜+𝑜ACNFB⁡B×∅
49 48 simprd ⊢A∈On∖2𝑜∧B∈On∧C∈B→ACNFB⁡y∈B⟼ify=C1𝑜∅=A↑𝑜C⋅𝑜1𝑜+𝑜ACNFB⁡B×∅
50 49 adantrl ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→ACNFB⁡y∈B⟼ify=C1𝑜∅=A↑𝑜C⋅𝑜1𝑜+𝑜ACNFB⁡B×∅
51 oecl ⊢A∈On∧C∈On→A↑𝑜C∈On
52 3 51 sylan ⊢A∈On∖2𝑜∧B∈On∧C∈On→A↑𝑜C∈On
53 om1 ⊢A↑𝑜C∈On→A↑𝑜C⋅𝑜1𝑜=A↑𝑜C
54 52 53 syl ⊢A∈On∖2𝑜∧B∈On∧C∈On→A↑𝑜C⋅𝑜1𝑜=A↑𝑜C
55 1 3 4 15 cantnf0 ⊢A∈On∖2𝑜∧B∈On→ACNFB⁡B×∅=∅
56 55 adantr ⊢A∈On∖2𝑜∧B∈On∧C∈On→ACNFB⁡B×∅=∅
57 54 56 oveq12d ⊢A∈On∖2𝑜∧B∈On∧C∈On→A↑𝑜C⋅𝑜1𝑜+𝑜ACNFB⁡B×∅=A↑𝑜C+𝑜∅
58 oa0 ⊢A↑𝑜C∈On→A↑𝑜C+𝑜∅=A↑𝑜C
59 52 58 syl ⊢A∈On∖2𝑜∧B∈On∧C∈On→A↑𝑜C+𝑜∅=A↑𝑜C
60 57 59 eqtrd ⊢A∈On∖2𝑜∧B∈On∧C∈On→A↑𝑜C⋅𝑜1𝑜+𝑜ACNFB⁡B×∅=A↑𝑜C
61 60 adantrr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→A↑𝑜C⋅𝑜1𝑜+𝑜ACNFB⁡B×∅=A↑𝑜C
62 50 61 eqtrd ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→ACNFB⁡y∈B⟼ify=C1𝑜∅=A↑𝑜C
63 62 eleq2d ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→ACNFB⁡F∈ACNFB⁡y∈B⟼ify=C1𝑜∅↔ACNFB⁡F∈A↑𝑜C
64 63 exp32 ⊢A∈On∖2𝑜∧B∈On→C∈On→C∈B→ACNFB⁡F∈ACNFB⁡y∈B⟼ify=C1𝑜∅↔ACNFB⁡F∈A↑𝑜C
65 64 adantrd ⊢A∈On∖2𝑜∧B∈On→C∈On∧F∈dom⁡ACNFB→C∈B→ACNFB⁡F∈ACNFB⁡y∈B⟼ify=C1𝑜∅↔ACNFB⁡F∈A↑𝑜C
66 65 imp31 ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧C∈B→ACNFB⁡F∈ACNFB⁡y∈B⟼ify=C1𝑜∅↔ACNFB⁡F∈A↑𝑜C
67 24 27 66 3bitrrd ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧C∈B→ACNFB⁡F∈A↑𝑜C↔Fab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡xy∈B⟼ify=C1𝑜∅
68 fveq1 ⊢a=F→a⁡c=F⁡c
69 68 eleq1d ⊢a=F→a⁡c∈b⁡c↔F⁡c∈b⁡c
70 fveq1 ⊢a=F→a⁡x=F⁡x
71 70 eqeq1d ⊢a=F→a⁡x=b⁡x↔F⁡x=b⁡x
72 71 imbi2d ⊢a=F→c∈x→a⁡x=b⁡x↔c∈x→F⁡x=b⁡x
73 72 ralbidv ⊢a=F→∀x∈Bc∈x→a⁡x=b⁡x↔∀x∈Bc∈x→F⁡x=b⁡x
74 69 73 anbi12d ⊢a=F→a⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡x↔F⁡c∈b⁡c∧∀x∈Bc∈x→F⁡x=b⁡x
75 74 rexbidv ⊢a=F→∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡x↔∃c∈BF⁡c∈b⁡c∧∀x∈Bc∈x→F⁡x=b⁡x
76 fveq1 ⊢b=y∈B⟼ify=C1𝑜∅→b⁡c=y∈B⟼ify=C1𝑜∅⁡c
77 76 eleq2d ⊢b=y∈B⟼ify=C1𝑜∅→F⁡c∈b⁡c↔F⁡c∈y∈B⟼ify=C1𝑜∅⁡c
78 fveq1 ⊢b=y∈B⟼ify=C1𝑜∅→b⁡x=y∈B⟼ify=C1𝑜∅⁡x
79 78 eqeq2d ⊢b=y∈B⟼ify=C1𝑜∅→F⁡x=b⁡x↔F⁡x=y∈B⟼ify=C1𝑜∅⁡x
80 79 imbi2d ⊢b=y∈B⟼ify=C1𝑜∅→c∈x→F⁡x=b⁡x↔c∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x
81 80 ralbidv ⊢b=y∈B⟼ify=C1𝑜∅→∀x∈Bc∈x→F⁡x=b⁡x↔∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x
82 77 81 anbi12d ⊢b=y∈B⟼ify=C1𝑜∅→F⁡c∈b⁡c∧∀x∈Bc∈x→F⁡x=b⁡x↔F⁡c∈y∈B⟼ify=C1𝑜∅⁡c∧∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x
83 82 rexbidv ⊢b=y∈B⟼ify=C1𝑜∅→∃c∈BF⁡c∈b⁡c∧∀x∈Bc∈x→F⁡x=b⁡x↔∃c∈BF⁡c∈y∈B⟼ify=C1𝑜∅⁡c∧∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x
84 75 83 5 bropabg ⊢Fab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡xy∈B⟼ify=C1𝑜∅↔F∈V∧y∈B⟼ify=C1𝑜∅∈V∧∃c∈BF⁡c∈y∈B⟼ify=C1𝑜∅⁡c∧∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x
85 fveq2 ⊢c=C→F⁡c=F⁡C
86 85 adantr ⊢c=C∧c∈B→F⁡c=F⁡C
87 eqeq1 ⊢y=c→y=C↔c=C
88 87 ifbid ⊢y=c→ify=C1𝑜∅=ifc=C1𝑜∅
89 1oex ⊢1𝑜∈V
90 89 43 ifex ⊢ifc=C1𝑜∅∈V
91 88 16 90 fvmpt ⊢c∈B→y∈B⟼ify=C1𝑜∅⁡c=ifc=C1𝑜∅
92 iftrue ⊢c=C→ifc=C1𝑜∅=1𝑜
93 91 92 sylan9eqr ⊢c=C∧c∈B→y∈B⟼ify=C1𝑜∅⁡c=1𝑜
94 86 93 eleq12d ⊢c=C∧c∈B→F⁡c∈y∈B⟼ify=C1𝑜∅⁡c↔F⁡C∈1𝑜
95 el1o ⊢F⁡C∈1𝑜↔F⁡C=∅
96 95 a1i ⊢c=C∧c∈B→F⁡C∈1𝑜↔F⁡C=∅
97 96 biimpd ⊢c=C∧c∈B→F⁡C∈1𝑜→F⁡C=∅
98 simpl ⊢c=C∧c∈B→c=C
99 97 98 jctild ⊢c=C∧c∈B→F⁡C∈1𝑜→c=C∧F⁡C=∅
100 94 99 sylbid ⊢c=C∧c∈B→F⁡c∈y∈B⟼ify=C1𝑜∅⁡c→c=C∧F⁡C=∅
101 100 expimpd ⊢c=C→c∈B∧F⁡c∈y∈B⟼ify=C1𝑜∅⁡c→c=C∧F⁡C=∅
102 91 adantl ⊢c≠C∧c∈B→y∈B⟼ify=C1𝑜∅⁡c=ifc=C1𝑜∅
103 simpl ⊢c≠C∧c∈B→c≠C
104 103 neneqd ⊢c≠C∧c∈B→¬c=C
105 104 iffalsed ⊢c≠C∧c∈B→ifc=C1𝑜∅=∅
106 102 105 eqtrd ⊢c≠C∧c∈B→y∈B⟼ify=C1𝑜∅⁡c=∅
107 106 eleq2d ⊢c≠C∧c∈B→F⁡c∈y∈B⟼ify=C1𝑜∅⁡c↔F⁡c∈∅
108 107 biimpd ⊢c≠C∧c∈B→F⁡c∈y∈B⟼ify=C1𝑜∅⁡c→F⁡c∈∅
109 108 expimpd ⊢c≠C→c∈B∧F⁡c∈y∈B⟼ify=C1𝑜∅⁡c→F⁡c∈∅
110 noel ⊢¬F⁡c∈∅
111 110 pm2.21i ⊢F⁡c∈∅→c=C∧F⁡C=∅
112 109 111 syl6 ⊢c≠C→c∈B∧F⁡c∈y∈B⟼ify=C1𝑜∅⁡c→c=C∧F⁡C=∅
113 101 112 pm2.61ine ⊢c∈B∧F⁡c∈y∈B⟼ify=C1𝑜∅⁡c→c=C∧F⁡C=∅
114 113 a1i ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→c∈B∧F⁡c∈y∈B⟼ify=C1𝑜∅⁡c→c=C∧F⁡C=∅
115 fveqeq2 ⊢x=C→F⁡x=∅↔F⁡C=∅
116 115 ralsng ⊢C∈B→∀x∈CF⁡x=∅↔F⁡C=∅
117 116 anbi2d ⊢C∈B→c=C∧∀x∈CF⁡x=∅↔c=C∧F⁡C=∅
118 117 biimprd ⊢C∈B→c=C∧F⁡C=∅→c=C∧∀x∈CF⁡x=∅
119 118 adantl ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→c=C∧F⁡C=∅→c=C∧∀x∈CF⁡x=∅
120 4 anim1i ⊢A∈On∖2𝑜∧B∈On∧C∈On→B∈On∧C∈On
121 120 adantr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→B∈On∧C∈On
122 pm3.31 ⊢x∈B→c∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→x∈B∧c∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x
123 122 a1i ⊢B∈On∧C∈On∧c=C→x∈B→c∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→x∈B∧c∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x
124 eldif ⊢x∈B∖suc⁡C↔x∈B∧¬x∈suc⁡C
125 simplr ⊢B∈On∧C∈On∧c=C∧x∈B→c=C
126 125 eleq1d ⊢B∈On∧C∈On∧c=C∧x∈B→c∈x↔C∈x
127 simpl ⊢B∈On∧C∈On→B∈On
128 127 adantr ⊢B∈On∧C∈On∧c=C→B∈On
129 onelon ⊢B∈On∧x∈B→x∈On
130 128 129 sylan ⊢B∈On∧C∈On∧c=C∧x∈B→x∈On
131 simpllr ⊢B∈On∧C∈On∧c=C∧x∈B→C∈On
132 ontri1 ⊢x∈On∧C∈On→x⊆C↔¬C∈x
133 130 131 132 syl2anc ⊢B∈On∧C∈On∧c=C∧x∈B→x⊆C↔¬C∈x
134 133 con2bid ⊢B∈On∧C∈On∧c=C∧x∈B→C∈x↔¬x⊆C
135 onsssuc ⊢x∈On∧C∈On→x⊆C↔x∈suc⁡C
136 130 131 135 syl2anc ⊢B∈On∧C∈On∧c=C∧x∈B→x⊆C↔x∈suc⁡C
137 136 notbid ⊢B∈On∧C∈On∧c=C∧x∈B→¬x⊆C↔¬x∈suc⁡C
138 126 134 137 3bitrrd ⊢B∈On∧C∈On∧c=C∧x∈B→¬x∈suc⁡C↔c∈x
139 138 pm5.32da ⊢B∈On∧C∈On∧c=C→x∈B∧¬x∈suc⁡C↔x∈B∧c∈x
140 124 139 bitrid ⊢B∈On∧C∈On∧c=C→x∈B∖suc⁡C↔x∈B∧c∈x
141 140 biimpd ⊢B∈On∧C∈On∧c=C→x∈B∖suc⁡C→x∈B∧c∈x
142 141 imim1d ⊢B∈On∧C∈On∧c=C→x∈B∧c∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→x∈B∖suc⁡C→F⁡x=y∈B⟼ify=C1𝑜∅⁡x
143 eldifi ⊢x∈B∖suc⁡C→x∈B
144 143 adantl ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→x∈B
145 eqeq1 ⊢y=x→y=C↔x=C
146 145 ifbid ⊢y=x→ify=C1𝑜∅=ifx=C1𝑜∅
147 89 43 ifex ⊢ifx=C1𝑜∅∈V
148 146 16 147 fvmpt ⊢x∈B→y∈B⟼ify=C1𝑜∅⁡x=ifx=C1𝑜∅
149 144 148 syl ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→y∈B⟼ify=C1𝑜∅⁡x=ifx=C1𝑜∅
150 128 143 129 syl2an ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→x∈On
151 eloni ⊢x∈On→Ord⁡x
152 150 151 syl ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→Ord⁡x
153 eloni ⊢B∈On→Ord⁡B
154 153 ad2antrr ⊢B∈On∧C∈On∧c=C→Ord⁡B
155 simplr ⊢B∈On∧C∈On∧c=C→C∈On
156 ordeldifsucon ⊢Ord⁡B∧C∈On→x∈B∖suc⁡C↔x∈B∧C∈x
157 154 155 156 syl2anc ⊢B∈On∧C∈On∧c=C→x∈B∖suc⁡C↔x∈B∧C∈x
158 157 biimpa ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→x∈B∧C∈x
159 ordirr ⊢Ord⁡x→¬x∈x
160 eleq1 ⊢x=C→x∈x↔C∈x
161 160 notbid ⊢x=C→¬x∈x↔¬C∈x
162 159 161 syl5ibcom ⊢Ord⁡x→x=C→¬C∈x
163 162 con2d ⊢Ord⁡x→C∈x→¬x=C
164 163 adantld ⊢Ord⁡x→x∈B∧C∈x→¬x=C
165 152 158 164 sylc ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→¬x=C
166 165 iffalsed ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→ifx=C1𝑜∅=∅
167 149 166 eqtrd ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→y∈B⟼ify=C1𝑜∅⁡x=∅
168 167 eqeq2d ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→F⁡x=y∈B⟼ify=C1𝑜∅⁡x↔F⁡x=∅
169 168 biimpd ⊢B∈On∧C∈On∧c=C∧x∈B∖suc⁡C→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→F⁡x=∅
170 169 ex ⊢B∈On∧C∈On∧c=C→x∈B∖suc⁡C→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→F⁡x=∅
171 170 a2d ⊢B∈On∧C∈On∧c=C→x∈B∖suc⁡C→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→x∈B∖suc⁡C→F⁡x=∅
172 123 142 171 3syld ⊢B∈On∧C∈On∧c=C→x∈B→c∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→x∈B∖suc⁡C→F⁡x=∅
173 172 ralimdv2 ⊢B∈On∧C∈On∧c=C→∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖suc⁡CF⁡x=∅
174 121 173 sylan ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c=C→∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖suc⁡CF⁡x=∅
175 174 adantr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c=C∧∀x∈CF⁡x=∅→∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖suc⁡CF⁡x=∅
176 ralun ⊢∀x∈CF⁡x=∅∧∀x∈B∖suc⁡CF⁡x=∅→∀x∈C∪B∖suc⁡CF⁡x=∅
177 176 adantll ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c=C∧∀x∈CF⁡x=∅∧∀x∈B∖suc⁡CF⁡x=∅→∀x∈C∪B∖suc⁡CF⁡x=∅
178 undif3 ⊢C∪B∖suc⁡C=C∪B∖suc⁡C∖C
179 simpr ⊢C∈On∧C∈B→C∈B
180 179 snssd ⊢C∈On∧C∈B→C⊆B
181 ssequn1 ⊢C⊆B↔C∪B=B
182 180 181 sylib ⊢C∈On∧C∈B→C∪B=B
183 simpl ⊢C∈On∧C∈B→C∈On
184 eloni ⊢C∈On→Ord⁡C
185 orddif ⊢Ord⁡C→C=suc⁡C∖C
186 183 184 185 3syl ⊢C∈On∧C∈B→C=suc⁡C∖C
187 186 eqcomd ⊢C∈On∧C∈B→suc⁡C∖C=C
188 182 187 difeq12d ⊢C∈On∧C∈B→C∪B∖suc⁡C∖C=B∖C
189 178 188 eqtrid ⊢C∈On∧C∈B→C∪B∖suc⁡C=B∖C
190 189 adantll ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→C∪B∖suc⁡C=B∖C
191 190 adantr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c=C→C∪B∖suc⁡C=B∖C
192 191 raleqdv ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c=C→∀x∈C∪B∖suc⁡CF⁡x=∅↔∀x∈B∖CF⁡x=∅
193 192 ad2antrr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c=C∧∀x∈CF⁡x=∅∧∀x∈B∖suc⁡CF⁡x=∅→∀x∈C∪B∖suc⁡CF⁡x=∅↔∀x∈B∖CF⁡x=∅
194 177 193 mpbid ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c=C∧∀x∈CF⁡x=∅∧∀x∈B∖suc⁡CF⁡x=∅→∀x∈B∖CF⁡x=∅
195 194 ex ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c=C∧∀x∈CF⁡x=∅→∀x∈B∖suc⁡CF⁡x=∅→∀x∈B∖CF⁡x=∅
196 175 195 syld ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c=C∧∀x∈CF⁡x=∅→∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖CF⁡x=∅
197 196 expl ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→c=C∧∀x∈CF⁡x=∅→∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖CF⁡x=∅
198 114 119 197 3syld ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→c∈B∧F⁡c∈y∈B⟼ify=C1𝑜∅⁡c→∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖CF⁡x=∅
199 198 expdimp ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c∈B→F⁡c∈y∈B⟼ify=C1𝑜∅⁡c→∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖CF⁡x=∅
200 199 impd ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B∧c∈B→F⁡c∈y∈B⟼ify=C1𝑜∅⁡c∧∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖CF⁡x=∅
201 200 rexlimdva ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→∃c∈BF⁡c∈y∈B⟼ify=C1𝑜∅⁡c∧∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖CF⁡x=∅
202 201 adantld ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→F∈V∧y∈B⟼ify=C1𝑜∅∈V∧∃c∈BF⁡c∈y∈B⟼ify=C1𝑜∅⁡c∧∀x∈Bc∈x→F⁡x=y∈B⟼ify=C1𝑜∅⁡x→∀x∈B∖CF⁡x=∅
203 84 202 biimtrid ⊢A∈On∖2𝑜∧B∈On∧C∈On∧C∈B→Fab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡xy∈B⟼ify=C1𝑜∅→∀x∈B∖CF⁡x=∅
204 203 adantlrr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧C∈B→Fab|∃c∈Ba⁡c∈b⁡c∧∀x∈Bc∈x→a⁡x=b⁡xy∈B⟼ify=C1𝑜∅→∀x∈B∖CF⁡x=∅
205 67 204 sylbid ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧C∈B→ACNFB⁡F∈A↑𝑜C→∀x∈B∖CF⁡x=∅
206 205 ex ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→C∈B→ACNFB⁡F∈A↑𝑜C→∀x∈B∖CF⁡x=∅
207 ral0 ⊢∀x∈∅F⁡x=∅
208 ssdif0 ⊢B⊆C↔B∖C=∅
209 208 biimpi ⊢B⊆C→B∖C=∅
210 209 raleqdv ⊢B⊆C→∀x∈B∖CF⁡x=∅↔∀x∈∅F⁡x=∅
211 207 210 mpbiri ⊢B⊆C→∀x∈B∖CF⁡x=∅
212 211 a1i13 ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→B⊆C→ACNFB⁡F∈A↑𝑜C→∀x∈B∖CF⁡x=∅
213 184 adantr ⊢C∈On∧F∈dom⁡ACNFB→Ord⁡C
214 153 adantl ⊢A∈On∖2𝑜∧B∈On→Ord⁡B
215 ordtri2or ⊢Ord⁡C∧Ord⁡B→C∈B∨B⊆C
216 213 214 215 syl2anr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→C∈B∨B⊆C
217 206 212 216 mpjaod ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→ACNFB⁡F∈A↑𝑜C→∀x∈B∖CF⁡x=∅
218 3 ad2antrr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅→A∈On
219 simpllr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅→B∈On
220 simplrr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅→F∈dom⁡ACNFB
221 15 ad2antrr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅→∅∈A
222 simplrl ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅→C∈On
223 1 3 4 cantnfs ⊢A∈On∖2𝑜∧B∈On→F∈dom⁡ACNFB↔F:B⟶A∧finSupp∅⁡F
224 223 biimpd ⊢A∈On∖2𝑜∧B∈On→F∈dom⁡ACNFB→F:B⟶A∧finSupp∅⁡F
225 224 adantld ⊢A∈On∖2𝑜∧B∈On→C∈On∧F∈dom⁡ACNFB→F:B⟶A∧finSupp∅⁡F
226 225 imp ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→F:B⟶A∧finSupp∅⁡F
227 226 simpld ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→F:B⟶A
228 227 adantr ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅→F:B⟶A
229 fveqeq2 ⊢x=y→F⁡x=∅↔F⁡y=∅
230 229 rspccv ⊢∀x∈B∖CF⁡x=∅→y∈B∖C→F⁡y=∅
231 230 adantl ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅→y∈B∖C→F⁡y=∅
232 231 imp ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅∧y∈B∖C→F⁡y=∅
233 228 232 suppss ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅→Fsupp∅⊆C
234 1 218 219 220 221 222 233 cantnflt2 ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB∧∀x∈B∖CF⁡x=∅→ACNFB⁡F∈A↑𝑜C
235 234 ex ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→∀x∈B∖CF⁡x=∅→ACNFB⁡F∈A↑𝑜C
236 217 235 impbid ⊢A∈On∖2𝑜∧B∈On∧C∈On∧F∈dom⁡ACNFB→ACNFB⁡F∈A↑𝑜C↔∀x∈B∖CF⁡x=∅