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 ⁡ A CNF B → A CNF B ⁡ F ∈ A ↑ 𝑜 C ↔ ∀ x ∈ B ∖ C F ⁡ x = ∅

Proof

Step Hyp Ref Expression
1 eqid ⊢ dom ⁡ A CNF B = dom ⁡ A CNF B
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 ⊢ a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x = a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x
6 1 3 4 5 cantnf ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → A CNF B Isom a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x , E dom ⁡ A CNF B A ↑ 𝑜 B
7 6 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ F ∈ dom ⁡ A CNF B → A CNF B Isom a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x , E dom ⁡ A CNF B A ↑ 𝑜 B
8 simpr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ F ∈ dom ⁡ A CNF B → F ∈ dom ⁡ A CNF B
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 𝑜 → if y = C 1 𝑜 ∅ ∈ A
13 12 ad2antrr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ y ∈ B → if y = C 1 𝑜 ∅ ∈ A
14 13 fmpttd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → y ∈ B ⟼ if y = C 1 𝑜 ∅ : B ⟶ A
15 11 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → ∅ ∈ A
16 eqid ⊢ y ∈ B ⟼ if y = C 1 𝑜 ∅ = y ∈ B ⟼ if y = C 1 𝑜 ∅
17 4 15 16 sniffsupp ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → finSupp ∅⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅
18 1 3 4 cantnfs ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → y ∈ B ⟼ if y = C 1 𝑜 ∅ ∈ dom ⁡ A CNF B ↔ y ∈ B ⟼ if y = C 1 𝑜 ∅ : B ⟶ A ∧ finSupp ∅⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅
19 14 17 18 mpbir2and ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → y ∈ B ⟼ if y = C 1 𝑜 ∅ ∈ dom ⁡ A CNF B
20 19 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ F ∈ dom ⁡ A CNF B → y ∈ B ⟼ if y = C 1 𝑜 ∅ ∈ dom ⁡ A CNF B
21 isorel ⊢ A CNF B Isom a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x , E dom ⁡ A CNF B A ↑ 𝑜 B ∧ F ∈ dom ⁡ A CNF B ∧ y ∈ B ⟼ if y = C 1 𝑜 ∅ ∈ dom ⁡ A CNF B → F a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F E A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅
22 7 8 20 21 syl12anc ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ F ∈ dom ⁡ A CNF B → F a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F E A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅
23 22 adantrl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B → F a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F E A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅
24 23 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ C ∈ B → F a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F E A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅
25 fvexd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ C ∈ B → A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ ∈ V
26 epelg ⊢ A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ ∈ V → A CNF B ⁡ F E A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F ∈ A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅
27 25 26 syl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ C ∈ B → A CNF B ⁡ F E A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F ∈ A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅
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 ⁡ A CNF B ↔ B × ∅ : B ⟶ A ∧ finSupp ∅⁡ B × ∅
35 32 33 34 mpbir2and ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → B × ∅ ∈ dom ⁡ A CNF B
36 35 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ B → B × ∅ ∈ dom ⁡ A CNF B
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 → if y = C 1 𝑜 B × ∅ ⁡ y = if y = C 1 𝑜 ∅
46 45 mpteq2ia ⊢ y ∈ B ⟼ if y = C 1 𝑜 B × ∅ ⁡ y = y ∈ B ⟼ if y = C 1 𝑜 ∅
47 46 eqcomi ⊢ y ∈ B ⟼ if y = C 1 𝑜 ∅ = y ∈ B ⟼ if y = C 1 𝑜 B × ∅ ⁡ y
48 1 28 29 36 37 38 42 47 cantnfp1 ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ B → y ∈ B ⟼ if y = C 1 𝑜 ∅ ∈ dom ⁡ A CNF B ∧ A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ = A ↑ 𝑜 C ⋅ 𝑜 1 𝑜 + 𝑜 A CNF B ⁡ B × ∅
49 48 simprd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ B → A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ = A ↑ 𝑜 C ⋅ 𝑜 1 𝑜 + 𝑜 A CNF B ⁡ B × ∅
50 49 adantrl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ = A ↑ 𝑜 C ⋅ 𝑜 1 𝑜 + 𝑜 A CNF B ⁡ 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 → A CNF B ⁡ B × ∅ = ∅
56 55 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On → A CNF B ⁡ B × ∅ = ∅
57 54 56 oveq12d ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On → A ↑ 𝑜 C ⋅ 𝑜 1 𝑜 + 𝑜 A CNF B ⁡ 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 𝑜 + 𝑜 A CNF B ⁡ B × ∅ = A ↑ 𝑜 C
61 60 adantrr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → A ↑ 𝑜 C ⋅ 𝑜 1 𝑜 + 𝑜 A CNF B ⁡ B × ∅ = A ↑ 𝑜 C
62 50 61 eqtrd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ = A ↑ 𝑜 C
63 62 eleq2d ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → A CNF B ⁡ F ∈ A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F ∈ A ↑ 𝑜 C
64 63 exp32 ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → C ∈ On → C ∈ B → A CNF B ⁡ F ∈ A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F ∈ A ↑ 𝑜 C
65 64 adantrd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → C ∈ On ∧ F ∈ dom ⁡ A CNF B → C ∈ B → A CNF B ⁡ F ∈ A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F ∈ A ↑ 𝑜 C
66 65 imp31 ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ C ∈ B → A CNF B ⁡ F ∈ A CNF B ⁡ y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ A CNF B ⁡ F ∈ A ↑ 𝑜 C
67 24 27 66 3bitrrd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ C ∈ B → A CNF B ⁡ F ∈ A ↑ 𝑜 C ↔ F a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x y ∈ B ⟼ if y = C 1 𝑜 ∅
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 ∈ B c ∈ x → a ⁡ x = b ⁡ x ↔ ∀ x ∈ B c ∈ x → F ⁡ x = b ⁡ x
74 69 73 anbi12d ⊢ a = F → a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x ↔ F ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = b ⁡ x
75 74 rexbidv ⊢ a = F → ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x ↔ ∃ c ∈ B F ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = b ⁡ x
76 fveq1 ⊢ b = y ∈ B ⟼ if y = C 1 𝑜 ∅ → b ⁡ c = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c
77 76 eleq2d ⊢ b = y ∈ B ⟼ if y = C 1 𝑜 ∅ → F ⁡ c ∈ b ⁡ c ↔ F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c
78 fveq1 ⊢ b = y ∈ B ⟼ if y = C 1 𝑜 ∅ → b ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x
79 78 eqeq2d ⊢ b = y ∈ B ⟼ if y = C 1 𝑜 ∅ → F ⁡ x = b ⁡ x ↔ F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x
80 79 imbi2d ⊢ b = y ∈ B ⟼ if y = C 1 𝑜 ∅ → c ∈ x → F ⁡ x = b ⁡ x ↔ c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x
81 80 ralbidv ⊢ b = y ∈ B ⟼ if y = C 1 𝑜 ∅ → ∀ x ∈ B c ∈ x → F ⁡ x = b ⁡ x ↔ ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x
82 77 81 anbi12d ⊢ b = y ∈ B ⟼ if y = C 1 𝑜 ∅ → F ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = b ⁡ x ↔ F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x
83 82 rexbidv ⊢ b = y ∈ B ⟼ if y = C 1 𝑜 ∅ → ∃ c ∈ B F ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = b ⁡ x ↔ ∃ c ∈ B F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x
84 75 83 5 bropabg ⊢ F a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x y ∈ B ⟼ if y = C 1 𝑜 ∅ ↔ F ∈ V ∧ y ∈ B ⟼ if y = C 1 𝑜 ∅ ∈ V ∧ ∃ c ∈ B F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ 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 → if y = C 1 𝑜 ∅ = if c = C 1 𝑜 ∅
89 1oex ⊢ 1 𝑜 ∈ V
90 89 43 ifex ⊢ if c = C 1 𝑜 ∅ ∈ V
91 88 16 90 fvmpt ⊢ c ∈ B → y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c = if c = C 1 𝑜 ∅
92 iftrue ⊢ c = C → if c = C 1 𝑜 ∅ = 1 𝑜
93 91 92 sylan9eqr ⊢ c = C ∧ c ∈ B → y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c = 1 𝑜
94 86 93 eleq12d ⊢ c = C ∧ c ∈ B → F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ 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 ⟼ if y = C 1 𝑜 ∅ ⁡ c → c = C ∧ F ⁡ C = ∅
101 100 expimpd ⊢ c = C → c ∈ B ∧ F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c → c = C ∧ F ⁡ C = ∅
102 91 adantl ⊢ c ≠ C ∧ c ∈ B → y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c = if c = C 1 𝑜 ∅
103 simpl ⊢ c ≠ C ∧ c ∈ B → c ≠ C
104 103 neneqd ⊢ c ≠ C ∧ c ∈ B → ¬ c = C
105 104 iffalsed ⊢ c ≠ C ∧ c ∈ B → if c = C 1 𝑜 ∅ = ∅
106 102 105 eqtrd ⊢ c ≠ C ∧ c ∈ B → y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c = ∅
107 106 eleq2d ⊢ c ≠ C ∧ c ∈ B → F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c ↔ F ⁡ c ∈ ∅
108 107 biimpd ⊢ c ≠ C ∧ c ∈ B → F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c → F ⁡ c ∈ ∅
109 108 expimpd ⊢ c ≠ C → c ∈ B ∧ F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ 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 ⟼ if y = C 1 𝑜 ∅ ⁡ c → c = C ∧ F ⁡ C = ∅
113 101 112 pm2.61ine ⊢ c ∈ B ∧ F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c → c = C ∧ F ⁡ C = ∅
114 113 a1i ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → c ∈ B ∧ F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c → c = C ∧ F ⁡ C = ∅
115 fveqeq2 ⊢ x = C → F ⁡ x = ∅ ↔ F ⁡ C = ∅
116 115 ralsng ⊢ C ∈ B → ∀ x ∈ C F ⁡ x = ∅ ↔ F ⁡ C = ∅
117 116 anbi2d ⊢ C ∈ B → c = C ∧ ∀ x ∈ C F ⁡ x = ∅ ↔ c = C ∧ F ⁡ C = ∅
118 117 biimprd ⊢ C ∈ B → c = C ∧ F ⁡ C = ∅ → c = C ∧ ∀ x ∈ C F ⁡ x = ∅
119 118 adantl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → c = C ∧ F ⁡ C = ∅ → c = C ∧ ∀ x ∈ C F ⁡ 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 ⟼ if y = C 1 𝑜 ∅ ⁡ x → x ∈ B ∧ c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x
123 122 a1i ⊢ B ∈ On ∧ C ∈ On ∧ c = C → x ∈ B → c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → x ∈ B ∧ c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ 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 ⟼ if y = C 1 𝑜 ∅ ⁡ x → x ∈ B ∖ suc ⁡ C → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ 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 → if y = C 1 𝑜 ∅ = if x = C 1 𝑜 ∅
147 89 43 ifex ⊢ if x = C 1 𝑜 ∅ ∈ V
148 146 16 147 fvmpt ⊢ x ∈ B → y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x = if x = C 1 𝑜 ∅
149 144 148 syl ⊢ B ∈ On ∧ C ∈ On ∧ c = C ∧ x ∈ B ∖ suc ⁡ C → y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x = if x = C 1 𝑜 ∅
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 → if x = C 1 𝑜 ∅ = ∅
167 149 166 eqtrd ⊢ B ∈ On ∧ C ∈ On ∧ c = C ∧ x ∈ B ∖ suc ⁡ C → y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x = ∅
168 167 eqeq2d ⊢ B ∈ On ∧ C ∈ On ∧ c = C ∧ x ∈ B ∖ suc ⁡ C → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x ↔ F ⁡ x = ∅
169 168 biimpd ⊢ B ∈ On ∧ C ∈ On ∧ c = C ∧ x ∈ B ∖ suc ⁡ C → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → F ⁡ x = ∅
170 169 ex ⊢ B ∈ On ∧ C ∈ On ∧ c = C → x ∈ B ∖ suc ⁡ C → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → F ⁡ x = ∅
171 170 a2d ⊢ B ∈ On ∧ C ∈ On ∧ c = C → x ∈ B ∖ suc ⁡ C → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ 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 ⟼ if y = C 1 𝑜 ∅ ⁡ x → x ∈ B ∖ suc ⁡ C → F ⁡ x = ∅
173 172 ralimdv2 ⊢ B ∈ On ∧ C ∈ On ∧ c = C → ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ suc ⁡ C F ⁡ x = ∅
174 121 173 sylan ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B ∧ c = C → ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ suc ⁡ C F ⁡ x = ∅
175 174 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B ∧ c = C ∧ ∀ x ∈ C F ⁡ x = ∅ → ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ suc ⁡ C F ⁡ x = ∅
176 ralun ⊢ ∀ x ∈ C F ⁡ x = ∅ ∧ ∀ x ∈ B ∖ suc ⁡ C F ⁡ x = ∅ → ∀ x ∈ C ∪ B ∖ suc ⁡ C F ⁡ x = ∅
177 176 adantll ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B ∧ c = C ∧ ∀ x ∈ C F ⁡ x = ∅ ∧ ∀ x ∈ B ∖ suc ⁡ C F ⁡ x = ∅ → ∀ x ∈ C ∪ B ∖ suc ⁡ C F ⁡ 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 ⁡ C F ⁡ x = ∅ ↔ ∀ x ∈ B ∖ C F ⁡ x = ∅
193 192 ad2antrr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B ∧ c = C ∧ ∀ x ∈ C F ⁡ x = ∅ ∧ ∀ x ∈ B ∖ suc ⁡ C F ⁡ x = ∅ → ∀ x ∈ C ∪ B ∖ suc ⁡ C F ⁡ x = ∅ ↔ ∀ x ∈ B ∖ C F ⁡ x = ∅
194 177 193 mpbid ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B ∧ c = C ∧ ∀ x ∈ C F ⁡ x = ∅ ∧ ∀ x ∈ B ∖ suc ⁡ C F ⁡ x = ∅ → ∀ x ∈ B ∖ C F ⁡ x = ∅
195 194 ex ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B ∧ c = C ∧ ∀ x ∈ C F ⁡ x = ∅ → ∀ x ∈ B ∖ suc ⁡ C F ⁡ x = ∅ → ∀ x ∈ B ∖ C F ⁡ x = ∅
196 175 195 syld ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B ∧ c = C ∧ ∀ x ∈ C F ⁡ x = ∅ → ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ C F ⁡ x = ∅
197 196 expl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → c = C ∧ ∀ x ∈ C F ⁡ x = ∅ → ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ C F ⁡ x = ∅
198 114 119 197 3syld ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → c ∈ B ∧ F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c → ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ C F ⁡ x = ∅
199 198 expdimp ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B ∧ c ∈ B → F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c → ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ C F ⁡ x = ∅
200 199 impd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B ∧ c ∈ B → F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ C F ⁡ x = ∅
201 200 rexlimdva ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → ∃ c ∈ B F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ C F ⁡ x = ∅
202 201 adantld ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → F ∈ V ∧ y ∈ B ⟼ if y = C 1 𝑜 ∅ ∈ V ∧ ∃ c ∈ B F ⁡ c ∈ y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ c ∧ ∀ x ∈ B c ∈ x → F ⁡ x = y ∈ B ⟼ if y = C 1 𝑜 ∅ ⁡ x → ∀ x ∈ B ∖ C F ⁡ x = ∅
203 84 202 biimtrid ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ C ∈ B → F a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x y ∈ B ⟼ if y = C 1 𝑜 ∅ → ∀ x ∈ B ∖ C F ⁡ x = ∅
204 203 adantlrr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ C ∈ B → F a b | ∃ c ∈ B a ⁡ c ∈ b ⁡ c ∧ ∀ x ∈ B c ∈ x → a ⁡ x = b ⁡ x y ∈ B ⟼ if y = C 1 𝑜 ∅ → ∀ x ∈ B ∖ C F ⁡ x = ∅
205 67 204 sylbid ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ C ∈ B → A CNF B ⁡ F ∈ A ↑ 𝑜 C → ∀ x ∈ B ∖ C F ⁡ x = ∅
206 205 ex ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B → C ∈ B → A CNF B ⁡ F ∈ A ↑ 𝑜 C → ∀ x ∈ B ∖ C F ⁡ 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 ∖ C F ⁡ x = ∅ ↔ ∀ x ∈ ∅ F ⁡ x = ∅
211 207 210 mpbiri ⊢ B ⊆ C → ∀ x ∈ B ∖ C F ⁡ x = ∅
212 211 a1i13 ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B → B ⊆ C → A CNF B ⁡ F ∈ A ↑ 𝑜 C → ∀ x ∈ B ∖ C F ⁡ x = ∅
213 184 adantr ⊢ C ∈ On ∧ F ∈ dom ⁡ A CNF B → 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 ⁡ A CNF B → C ∈ B ∨ B ⊆ C
217 206 212 216 mpjaod ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B → A CNF B ⁡ F ∈ A ↑ 𝑜 C → ∀ x ∈ B ∖ C F ⁡ x = ∅
218 3 ad2antrr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ → A ∈ On
219 simpllr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ → B ∈ On
220 simplrr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ → F ∈ dom ⁡ A CNF B
221 15 ad2antrr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ → ∅ ∈ A
222 simplrl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ → C ∈ On
223 1 3 4 cantnfs ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → F ∈ dom ⁡ A CNF B ↔ F : B ⟶ A ∧ finSupp ∅⁡ F
224 223 biimpd ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → F ∈ dom ⁡ A CNF B → F : B ⟶ A ∧ finSupp ∅⁡ F
225 224 adantld ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On → C ∈ On ∧ F ∈ dom ⁡ A CNF B → F : B ⟶ A ∧ finSupp ∅⁡ F
226 225 imp ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B → F : B ⟶ A ∧ finSupp ∅⁡ F
227 226 simpld ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B → F : B ⟶ A
228 227 adantr ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ → F : B ⟶ A
229 fveqeq2 ⊢ x = y → F ⁡ x = ∅ ↔ F ⁡ y = ∅
230 229 rspccv ⊢ ∀ x ∈ B ∖ C F ⁡ x = ∅ → y ∈ B ∖ C → F ⁡ y = ∅
231 230 adantl ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ → y ∈ B ∖ C → F ⁡ y = ∅
232 231 imp ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ ∧ y ∈ B ∖ C → F ⁡ y = ∅
233 228 232 suppss ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ → F supp ∅ ⊆ C
234 1 218 219 220 221 222 233 cantnflt2 ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B ∧ ∀ x ∈ B ∖ C F ⁡ x = ∅ → A CNF B ⁡ F ∈ A ↑ 𝑜 C
235 234 ex ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B → ∀ x ∈ B ∖ C F ⁡ x = ∅ → A CNF B ⁡ F ∈ A ↑ 𝑜 C
236 217 235 impbid ⊢ A ∈ On ∖ 2 𝑜 ∧ B ∈ On ∧ C ∈ On ∧ F ∈ dom ⁡ A CNF B → A CNF B ⁡ F ∈ A ↑ 𝑜 C ↔ ∀ x ∈ B ∖ C F ⁡ x = ∅