Theorem cantnfresb 44109

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.)

Assertion

Ref	Expression
cantnfresb	⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐹

Proof of Theorem cantnfresb

Dummy variables 𝑎 𝑏 𝑐 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2765	. . . . . . . . . . 11 ⊢ dom (𝐴 CNF 𝐵) = dom (𝐴 CNF 𝐵)
2		eldifi 4085	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
3	2	adantr 486	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → 𝐴 ∈ On)
4		simpr 490	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
5		eqid 2765	. . . . . . . . . . 11 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}
6	1, 3, 4, 5	cantnf 9669	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵)))
7	6	adantr 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵)))
8		simpr 490	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
9		ondif2 8493	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (On ∖ 2o) ↔ (𝐴 ∈ On ∧ 1o ∈ 𝐴))
10	9	simprbi 503	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (On ∖ 2o) → 1o ∈ 𝐴)
11		dif20el 8496	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
12	10, 11	ifcld 4536	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (On ∖ 2o) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴)
13	12	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ 𝐵) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴)
14	13	fmpttd 7114	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴)
15	11	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ∅ ∈ 𝐴)
16		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))
17	4, 15, 16	sniffsupp 9367	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp ∅)
18	1, 3, 4	cantnfs 9642	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴 ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp ∅)))
19	14, 17, 18	mpbir2and 726	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))
20	19	adantr 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))
21		isorel 7333	. . . . . . . . 9 ⊢ (((𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵)) ∧ (𝐹 ∈ dom (𝐴 CNF 𝐵) ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
22	7, 8, 20, 21	syl12anc 850	. . . . . . . 8 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
23	22	adantrl 729	. . . . . . 7 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
24	23	adantr 486	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
25		fvexd 6900	. . . . . . 7 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈ V)
26		epelg 5564	. . . . . . 7 ⊢ (((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈ V → (((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
27	25, 26	syl 18	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
28	2	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐴 ∈ On)
29		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐵 ∈ On)
30		fconst6g 6771	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ 𝐴 → (𝐵 × {∅}):𝐵⟶𝐴)
31	11, 30	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ (On ∖ 2o) → (𝐵 × {∅}):𝐵⟶𝐴)
32	31	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}):𝐵⟶𝐴)
33	4, 15	fczfsuppd 9353	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) finSupp ∅)
34	1, 3, 4	cantnfs 9642	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
35	32, 33, 34	mpbir2and 726	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
36	35	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
37		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵)
38	10	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 1o ∈ 𝐴)
39		fczsupp0 8195	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 × {∅}) supp ∅) = ∅
40		0ss 4357	. . . . . . . . . . . . . . . 16 ⊢ ∅ ⊆ 𝐶
41	39, 40	eqsstri 3984	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 × {∅}) supp ∅) ⊆ 𝐶
42	41	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝐵 × {∅}) supp ∅) ⊆ 𝐶)
43		0ex 5272	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
44	43	fvconst2 7209	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐵 → ((𝐵 × {∅})‘𝑦) = ∅)
45	44	ifeq2d 4510	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)) = if(𝑦 = 𝐶, 1o, ∅))
46	45	mpteq2ia 5208	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))
47	46	eqcomi 2774	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)))
48	1, 28, 29, 36, 37, 38, 42, 47	cantnfp1 9657	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ∧ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅})))))
49	48	simprd 501	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
50	49	adantrl 729	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
51		oecl 8528	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On)
52	3, 51	sylan 592	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On)
53		om1 8533	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) ·o 1o) = (𝐴 ↑o 𝐶))
54	52, 53	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐶) ·o 1o) = (𝐴 ↑o 𝐶))
55	1, 3, 4, 15	cantnf0 9651	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
56	55	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
57	54, 56	oveq12d 7437	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = ((𝐴 ↑o 𝐶) +o ∅))
58		oa0 8507	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) +o ∅) = (𝐴 ↑o 𝐶))
59	52, 58	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐶) +o ∅) = (𝐴 ↑o 𝐶))
60	57, 59	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶))
61	60	adantrr 730	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶))
62	50, 61	eqtrd 2800	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (𝐴 ↑o 𝐶))
63	62	eleq2d 2851	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))
64	63	exp32 426	. . . . . . . 8 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐶 ∈ On → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))))
65	64	adantrd 497	. . . . . . 7 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))))
66	65	imp31 423	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))
67	24, 27, 66	3bitrrd 309	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ 𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))))
68		fveq1 6884	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑐) = (𝐹‘𝑐))
69	68	eleq1d 2850	. . . . . . . . . 10 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ (𝑏‘𝑐)))
70		fveq1 6884	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑥) = (𝐹‘𝑥))
71	70	eqeq1d 2767	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = (𝑏‘𝑥)))
72	71	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐹 → ((𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))
73	72	ralbidv 3190	. . . . . . . . . 10 ⊢ (𝑎 = 𝐹 → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))
74	69, 73	anbi12d 644	. . . . . . . . 9 ⊢ (𝑎 = 𝐹 → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))))
75	74	rexbidv 3191	. . . . . . . 8 ⊢ (𝑎 = 𝐹 → (∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))))
76		fveq1 6884	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑐) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐))
77	76	eleq2d 2851	. . . . . . . . . 10 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)))
78		fveq1 6884	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))
79	78	eqeq2d 2776	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))
80	79	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
81	80	ralbidv 3190	. . . . . . . . . 10 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
82	77, 81	anbi12d 644	. . . . . . . . 9 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
83	82	rexbidv 3191	. . . . . . . 8 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
84	75, 83, 5	bropabg 44108	. . . . . . 7 ⊢ (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
85		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝐶 → (𝐹‘𝑐) = (𝐹‘𝐶))
86	85	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → (𝐹‘𝑐) = (𝐹‘𝐶))
87		eqeq1 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → (𝑦 = 𝐶 ↔ 𝑐 = 𝐶))
88	87	ifbid 4513	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑐 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑐 = 𝐶, 1o, ∅))
89		1oex 8469	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1o ∈ V
90	89, 43	ifex 4540	. . . . . . . . . . . . . . . . . . 19 ⊢ if(𝑐 = 𝐶, 1o, ∅) ∈ V
91	88, 16, 90	fvmpt 6993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅))
92		iftrue 4495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝐶 → if(𝑐 = 𝐶, 1o, ∅) = 1o)
93	91, 92	sylan9eqr 2822	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = 1o)
94	86, 93	eleq12d 2859	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝐶) ∈ 1o))
95		el1o 8486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅)
96	95	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅))
97	96	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝐹‘𝐶) = ∅))
98		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 = 𝐶)
99	97, 98	jctild 535	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
100	94, 99	sylbid 243	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
101	100	expimpd 459	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
102	91	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅))
103		simpl 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 ≠ 𝐶)
104	103	neneqd 2965	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ¬ 𝑐 = 𝐶)
105	104	iffalsed 4500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → if(𝑐 = 𝐶, 1o, ∅) = ∅)
106	102, 105	eqtrd 2800	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = ∅)
107	106	eleq2d 2851	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝑐) ∈ ∅))
108	107	biimpd 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝐹‘𝑐) ∈ ∅))
109	108	expimpd 459	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝐹‘𝑐) ∈ ∅))
110		noel 4291	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝐹‘𝑐) ∈ ∅
111	110	pm2.21i 120	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑐) ∈ ∅ → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))
112	109, 111	syl6 36	. . . . . . . . . . . . . 14 ⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
113	101, 112	pm2.61ine 3043	. . . . . . . . . . . . 13 ⊢ ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))
114	113	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
115		fveqeq2 6894	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅))
116	115	ralsng 4643	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ 𝐵 → (∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅))
117	116	anbi2d 642	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ↔ (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
118	117	biimprd 251	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅)))
119	118	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅)))
120	4	anim1i 627	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
121	120	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
122		pm3.31 455	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))
123	122	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
124		eldif 3916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶))
125		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑐 = 𝐶)
126	125	eleq1d 2850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑐 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥))
127		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
128	127	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐵 ∈ On)
129		onelon 6389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
130	128, 129	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
131		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ On)
132		ontri1 6399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥))
133	130, 131, 132	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥))
134	133	con2bid 357	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝑥 ↔ ¬ 𝑥 ⊆ 𝐶))
135		onsssuc 6457	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶))
136	130, 131, 135	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶))
137	136	notbid 321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ⊆ 𝐶 ↔ ¬ 𝑥 ∈ suc 𝐶))
138	126, 134, 137	3bitrrd 309	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ suc 𝐶 ↔ 𝑐 ∈ 𝑥))
139	138	pm5.32da 590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥)))
140	124, 139	bitrid 286	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥)))
141	140	biimpd 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥)))
142	141	imim1d 83	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
143		eldifi 4085	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) → 𝑥 ∈ 𝐵)
144	143	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ 𝐵)
145		eqeq1 2769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝐶 ↔ 𝑥 = 𝐶))
146	145	ifbid 4513	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑥 = 𝐶, 1o, ∅))
147	89, 43	ifex 4540	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(𝑥 = 𝐶, 1o, ∅) ∈ V
148	146, 16, 147	fvmpt 6993	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅))
149	144, 148	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅))
150	128, 143, 129	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ On)
151		eloni 6374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ On → Ord 𝑥)
152	150, 151	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → Ord 𝑥)
153		eloni 6374	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐵 ∈ On → Ord 𝐵)
154	153	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → Ord 𝐵)
155		simplr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐶 ∈ On)
156		ordeldifsucon 44044	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝐵 ∧ 𝐶 ∈ On) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)))
157	154, 155, 156	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)))
158	157	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥))
159		ordirr 6382	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥)
160		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥))
161	160	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝐶 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝐶 ∈ 𝑥))
162	159, 161	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Ord 𝑥 → (𝑥 = 𝐶 → ¬ 𝐶 ∈ 𝑥))
163	162	con2d 135	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝑥 → (𝐶 ∈ 𝑥 → ¬ 𝑥 = 𝐶))
164	163	adantld 496	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑥 → ((𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥) → ¬ 𝑥 = 𝐶))
165	152, 158, 164	sylc 66	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ¬ 𝑥 = 𝐶)
166	165	iffalsed 4500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → if(𝑥 = 𝐶, 1o, ∅) = ∅)
167	149, 166	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = ∅)
168	167	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) ↔ (𝐹‘𝑥) = ∅))
169	168	biimpd 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅))
170	169	ex 418	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅)))
171	170	a2d 30	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ∅)))
172	123, 142, 171	3syld 61	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ∅)))
173	172	ralimdv2 3176	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
174	121, 173	sylan 592	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
175	174	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
176		ralun 4151	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅)
177	176	adantll 727	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅)
178		undif3 4253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶}))
179		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵)
180	179	snssd 4754	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵)
181		ssequn1 4139	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∪ 𝐵) = 𝐵)
182	180, 181	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ 𝐵) = 𝐵)
183		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ On)
184		eloni 6374	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐶 ∈ On → Ord 𝐶)
185		orddif 6463	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Ord 𝐶 → 𝐶 = (suc 𝐶 ∖ {𝐶}))
186	183, 184, 185	3syl 19	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 = (suc 𝐶 ∖ {𝐶}))
187	186	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (suc 𝐶 ∖ {𝐶}) = 𝐶)
188	182, 187	difeq12d 4082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶})) = (𝐵 ∖ 𝐶))
189	178, 188	eqtrid 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
190	189	adantll 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
191	190	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
192	191	raleqdv 3325	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
193	192	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
194	177, 193	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)
195	194	ex 418	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
196	175, 195	syld 48	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
197	196	expl 463	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
198	114, 119, 197	3syld 61	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
199	198	expdimp 458	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
200	199	impd 416	. . . . . . . . 9 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
201	200	rexlimdva 3168	. . . . . . . 8 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
202	201	adantld 496	. . . . . . 7 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
203	84, 202	biimtrid 245	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
204	203	adantlrr 734	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
205	67, 204	sylbid 243	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
206	205	ex 418	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
207		ral0 4461	. . . . 5 ⊢ ∀𝑥 ∈ ∅ (𝐹‘𝑥) = ∅
208		ssdif0 4321	. . . . . . 7 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐵 ∖ 𝐶) = ∅)
209	208	biimpi 219	. . . . . 6 ⊢ (𝐵 ⊆ 𝐶 → (𝐵 ∖ 𝐶) = ∅)
210	209	raleqdv 3325	. . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ ∅ (𝐹‘𝑥) = ∅))
211	207, 210	mpbiri 261	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)
212	211	a1i13 28	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐵 ⊆ 𝐶 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
213	184	adantr 486	. . . 4 ⊢ ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → Ord 𝐶)
214	153	adantl 487	. . . 4 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → Ord 𝐵)
215		ordtri2or 6465	. . . 4 ⊢ ((Ord 𝐶 ∧ Ord 𝐵) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶))
216	213, 214, 215	syl2anr 609	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶))
217	206, 212, 216	mpjaod 874	. 2 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
218	3	ad2antrr 739	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐴 ∈ On)
219		simpllr 788	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐵 ∈ On)
220		simplrr 790	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
221	15	ad2antrr 739	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ∅ ∈ 𝐴)
222		simplrl 789	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐶 ∈ On)
223	1, 3, 4	cantnfs 9642	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
224	223	biimpd 232	. . . . . . . . 9 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
225	224	adantld 496	. . . . . . . 8 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
226	225	imp 412	. . . . . . 7 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
227	226	simpld 500	. . . . . 6 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → 𝐹:𝐵⟶𝐴)
228	227	adantr 486	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹:𝐵⟶𝐴)
229		fveqeq2 6894	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑦) = ∅))
230	229	rspccv 3580	. . . . . . 7 ⊢ (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅))
231	230	adantl 487	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅))
232	231	imp 412	. . . . 5 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) ∧ 𝑦 ∈ (𝐵 ∖ 𝐶)) → (𝐹‘𝑦) = ∅)
233	228, 232	suppss 8196	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝐹 supp ∅) ⊆ 𝐶)
234	1, 218, 219, 220, 221, 222, 233	cantnflt2 9649	. . 3 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))
235	234	ex 418	. 2 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))
236	217, 235	impbid 215	1 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  Vcvv 3457   ∖ cdif 3903   ∪ cun 3904   ⊆ wss 3906  ∅c0 4286  ifcif 4489  {csn 4591   class class class wbr 5111  {copab 5175   ↦ cmpt 5194   E cep 5562   × cxp 5661  dom cdm 5663  Ord word 6363  Oncon0 6364  suc csuc 6366  ⟶wf 6536  ‘cfv 6540   Isom wiso 6541  (class class class)co 7419   supp csupp 8162  1_oc1o 8452  2_oc2o 8453   +_o coa 8456   ·_o comu 8457   ↑_o coe 8458   finSupp cfsupp 9328   CNF ccnf 9637

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-supp 8163  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-seqom 8441  df-1o 8459  df-2o 8460  df-oadd 8463  df-omul 8464  df-oexp 8465  df-er 8700  df-map 8832  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-fsupp 9329  df-oi 9479  df-cnf 9638

This theorem is used by:  cantnf2  44110