Theorem cantnfresb 43898

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 2762	. . . . . . . . . . 11 ⊢ dom (𝐴 CNF 𝐵) = dom (𝐴 CNF 𝐵)
2		eldifi 4084	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
3	2	adantr 484	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → 𝐴 ∈ On)
4		simpr 488	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
5		eqid 2762	. . . . . . . . . . 11 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}
6	1, 3, 4, 5	cantnf 9648	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵)))
7	6	adantr 484	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵)))
8		simpr 488	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
9		ondif2 8471	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (On ∖ 2o) ↔ (𝐴 ∈ On ∧ 1o ∈ 𝐴))
10	9	simprbi 501	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (On ∖ 2o) → 1o ∈ 𝐴)
11		dif20el 8474	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
12	10, 11	ifcld 4527	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (On ∖ 2o) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴)
13	12	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ 𝐵) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴)
14	13	fmpttd 7096	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴)
15	11	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ∅ ∈ 𝐴)
16		eqid 2762	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))
17	4, 15, 16	sniffsupp 9346	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp ∅)
18	1, 3, 4	cantnfs 9621	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴 ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp ∅)))
19	14, 17, 18	mpbir2and 723	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))
20	19	adantr 484	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))
21		isorel 7310	. . . . . . . . 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 847	. . . . . . . 8 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
23	22	adantrl 726	. . . . . . 7 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
24	23	adantr 484	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
25		fvexd 6882	. . . . . . 7 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈ V)
26		epelg 5548	. . . . . . 7 ⊢ (((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈ V → (((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
27	25, 26	syl 17	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
28	2	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐴 ∈ On)
29		simplr 778	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐵 ∈ On)
30		fconst6g 6753	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ 𝐴 → (𝐵 × {∅}):𝐵⟶𝐴)
31	11, 30	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ (On ∖ 2o) → (𝐵 × {∅}):𝐵⟶𝐴)
32	31	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}):𝐵⟶𝐴)
33	4, 15	fczfsuppd 9332	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) finSupp ∅)
34	1, 3, 4	cantnfs 9621	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
35	32, 33, 34	mpbir2and 723	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
36	35	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
37		simpr 488	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵)
38	10	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 1o ∈ 𝐴)
39		fczsupp0 8173	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 × {∅}) supp ∅) = ∅
40		0ss 4354	. . . . . . . . . . . . . . . 16 ⊢ ∅ ⊆ 𝐶
41	39, 40	eqsstri 3982	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 × {∅}) supp ∅) ⊆ 𝐶
42	41	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝐵 × {∅}) supp ∅) ⊆ 𝐶)
43		0ex 5257	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
44	43	fvconst2 7188	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐵 → ((𝐵 × {∅})‘𝑦) = ∅)
45	44	ifeq2d 4501	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)) = if(𝑦 = 𝐶, 1o, ∅))
46	45	mpteq2ia 5195	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))
47	46	eqcomi 2771	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)))
48	1, 28, 29, 36, 37, 38, 42, 47	cantnfp1 9636	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ∧ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅})))))
49	48	simprd 499	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
50	49	adantrl 726	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
51		oecl 8506	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On)
52	3, 51	sylan 589	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On)
53		om1 8511	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) ·o 1o) = (𝐴 ↑o 𝐶))
54	52, 53	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐶) ·o 1o) = (𝐴 ↑o 𝐶))
55	1, 3, 4, 15	cantnf0 9630	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
56	55	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
57	54, 56	oveq12d 7414	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = ((𝐴 ↑o 𝐶) +o ∅))
58		oa0 8485	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) +o ∅) = (𝐴 ↑o 𝐶))
59	52, 58	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐶) +o ∅) = (𝐴 ↑o 𝐶))
60	57, 59	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶))
61	60	adantrr 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶))
62	50, 61	eqtrd 2797	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (𝐴 ↑o 𝐶))
63	62	eleq2d 2848	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))
64	63	exp32 424	. . . . . . . 8 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐶 ∈ On → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))))
65	64	adantrd 495	. . . . . . 7 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))))
66	65	imp31 421	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))
67	24, 27, 66	3bitrrd 308	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ 𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))))
68		fveq1 6866	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑐) = (𝐹‘𝑐))
69	68	eleq1d 2847	. . . . . . . . . 10 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ (𝑏‘𝑐)))
70		fveq1 6866	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑥) = (𝐹‘𝑥))
71	70	eqeq1d 2764	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = (𝑏‘𝑥)))
72	71	imbi2d 342	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐹 → ((𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))
73	72	ralbidv 3185	. . . . . . . . . 10 ⊢ (𝑎 = 𝐹 → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))
74	69, 73	anbi12d 641	. . . . . . . . 9 ⊢ (𝑎 = 𝐹 → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))))
75	74	rexbidv 3186	. . . . . . . 8 ⊢ (𝑎 = 𝐹 → (∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))))
76		fveq1 6866	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑐) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐))
77	76	eleq2d 2848	. . . . . . . . . 10 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)))
78		fveq1 6866	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))
79	78	eqeq2d 2773	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))
80	79	imbi2d 342	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
81	80	ralbidv 3185	. . . . . . . . . 10 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
82	77, 81	anbi12d 641	. . . . . . . . 9 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
83	82	rexbidv 3186	. . . . . . . 8 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
84	75, 83, 5	bropabg 43897	. . . . . . 7 ⊢ (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
85		fveq2 6867	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝐶 → (𝐹‘𝑐) = (𝐹‘𝐶))
86	85	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → (𝐹‘𝑐) = (𝐹‘𝐶))
87		eqeq1 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → (𝑦 = 𝐶 ↔ 𝑐 = 𝐶))
88	87	ifbid 4504	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑐 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑐 = 𝐶, 1o, ∅))
89		1oex 8447	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1o ∈ V
90	89, 43	ifex 4531	. . . . . . . . . . . . . . . . . . 19 ⊢ if(𝑐 = 𝐶, 1o, ∅) ∈ V
91	88, 16, 90	fvmpt 6975	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅))
92		iftrue 4486	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝐶 → if(𝑐 = 𝐶, 1o, ∅) = 1o)
93	91, 92	sylan9eqr 2819	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = 1o)
94	86, 93	eleq12d 2856	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝐶) ∈ 1o))
95		el1o 8464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅)
96	95	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅))
97	96	biimpd 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝐹‘𝐶) = ∅))
98		simpl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 = 𝐶)
99	97, 98	jctild 533	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
100	94, 99	sylbid 242	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
101	100	expimpd 457	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
102	91	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅))
103		simpl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 ≠ 𝐶)
104	103	neneqd 2962	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ¬ 𝑐 = 𝐶)
105	104	iffalsed 4491	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → if(𝑐 = 𝐶, 1o, ∅) = ∅)
106	102, 105	eqtrd 2797	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = ∅)
107	106	eleq2d 2848	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝑐) ∈ ∅))
108	107	biimpd 231	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝐹‘𝑐) ∈ ∅))
109	108	expimpd 457	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝐹‘𝑐) ∈ ∅))
110		noel 4290	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝐹‘𝑐) ∈ ∅
111	110	pm2.21i 119	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑐) ∈ ∅ → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))
112	109, 111	syl6 35	. . . . . . . . . . . . . 14 ⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
113	101, 112	pm2.61ine 3040	. . . . . . . . . . . . 13 ⊢ ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))
114	113	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
115		fveqeq2 6876	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅))
116	115	ralsng 4634	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ 𝐵 → (∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅))
117	116	anbi2d 639	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ↔ (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
118	117	biimprd 250	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅)))
119	118	adantl 485	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅)))
120	4	anim1i 624	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
121	120	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
122		pm3.31 453	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))
123	122	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
124		eldif 3914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶))
125		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑐 = 𝐶)
126	125	eleq1d 2847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑐 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥))
127		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
128	127	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐵 ∈ On)
129		onelon 6371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
130	128, 129	sylan 589	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
131		simpllr 785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ On)
132		ontri1 6380	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥))
133	130, 131, 132	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥))
134	133	con2bid 356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝑥 ↔ ¬ 𝑥 ⊆ 𝐶))
135		onsssuc 6438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶))
136	130, 131, 135	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶))
137	136	notbid 320	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ⊆ 𝐶 ↔ ¬ 𝑥 ∈ suc 𝐶))
138	126, 134, 137	3bitrrd 308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ suc 𝐶 ↔ 𝑐 ∈ 𝑥))
139	138	pm5.32da 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥)))
140	124, 139	bitrid 285	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥)))
141	140	biimpd 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥)))
142	141	imim1d 82	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
143		eldifi 4084	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) → 𝑥 ∈ 𝐵)
144	143	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ 𝐵)
145		eqeq1 2766	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝐶 ↔ 𝑥 = 𝐶))
146	145	ifbid 4504	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑥 = 𝐶, 1o, ∅))
147	89, 43	ifex 4531	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(𝑥 = 𝐶, 1o, ∅) ∈ V
148	146, 16, 147	fvmpt 6975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅))
149	144, 148	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅))
150	128, 143, 129	syl2an 605	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ On)
151		eloni 6356	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ On → Ord 𝑥)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → Ord 𝑥)
153		eloni 6356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐵 ∈ On → Ord 𝐵)
154	153	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → Ord 𝐵)
155		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐶 ∈ On)
156		ordeldifsucon 43833	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝐵 ∧ 𝐶 ∈ On) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)))
157	154, 155, 156	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)))
158	157	biimpa 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥))
159		ordirr 6364	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥)
160		eleq1 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥))
161	160	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝐶 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝐶 ∈ 𝑥))
162	159, 161	syl5ibcom 247	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Ord 𝑥 → (𝑥 = 𝐶 → ¬ 𝐶 ∈ 𝑥))
163	162	con2d 134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝑥 → (𝐶 ∈ 𝑥 → ¬ 𝑥 = 𝐶))
164	163	adantld 494	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑥 → ((𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥) → ¬ 𝑥 = 𝐶))
165	152, 158, 164	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ¬ 𝑥 = 𝐶)
166	165	iffalsed 4491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → if(𝑥 = 𝐶, 1o, ∅) = ∅)
167	149, 166	eqtrd 2797	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = ∅)
168	167	eqeq2d 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) ↔ (𝐹‘𝑥) = ∅))
169	168	biimpd 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅))
170	169	ex 416	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅)))
171	170	a2d 29	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ∅)))
172	123, 142, 171	3syld 60	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ∅)))
173	172	ralimdv2 3171	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
174	121, 173	sylan 589	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
175	174	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
176		ralun 4150	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅)
177	176	adantll 724	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅)
178		undif3 4252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶}))
179		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵)
180	179	snssd 4745	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵)
181		ssequn1 4138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∪ 𝐵) = 𝐵)
182	180, 181	sylib 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ 𝐵) = 𝐵)
183		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ On)
184		eloni 6356	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐶 ∈ On → Ord 𝐶)
185		orddif 6444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Ord 𝐶 → 𝐶 = (suc 𝐶 ∖ {𝐶}))
186	183, 184, 185	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 = (suc 𝐶 ∖ {𝐶}))
187	186	eqcomd 2768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (suc 𝐶 ∖ {𝐶}) = 𝐶)
188	182, 187	difeq12d 4081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶})) = (𝐵 ∖ 𝐶))
189	178, 188	eqtrid 2809	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
190	189	adantll 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
191	190	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
192	191	raleqdv 3320	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
193	192	ad2antrr 736	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
194	177, 193	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)
195	194	ex 416	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
196	175, 195	syld 47	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
197	196	expl 461	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
198	114, 119, 197	3syld 60	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
199	198	expdimp 456	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
200	199	impd 414	. . . . . . . . 9 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
201	200	rexlimdva 3163	. . . . . . . 8 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
202	201	adantld 494	. . . . . . 7 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
203	84, 202	biimtrid 244	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
204	203	adantlrr 731	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
205	67, 204	sylbid 242	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
206	205	ex 416	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
207		ral0 4452	. . . . 5 ⊢ ∀𝑥 ∈ ∅ (𝐹‘𝑥) = ∅
208		ssdif0 4319	. . . . . . 7 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐵 ∖ 𝐶) = ∅)
209	208	biimpi 218	. . . . . 6 ⊢ (𝐵 ⊆ 𝐶 → (𝐵 ∖ 𝐶) = ∅)
210	209	raleqdv 3320	. . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ ∅ (𝐹‘𝑥) = ∅))
211	207, 210	mpbiri 260	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)
212	211	a1i13 27	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐵 ⊆ 𝐶 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
213	184	adantr 484	. . . 4 ⊢ ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → Ord 𝐶)
214	153	adantl 485	. . . 4 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → Ord 𝐵)
215		ordtri2or 6446	. . . 4 ⊢ ((Ord 𝐶 ∧ Ord 𝐵) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶))
216	213, 214, 215	syl2anr 606	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶))
217	206, 212, 216	mpjaod 871	. 2 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
218	3	ad2antrr 736	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐴 ∈ On)
219		simpllr 785	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐵 ∈ On)
220		simplrr 787	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
221	15	ad2antrr 736	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ∅ ∈ 𝐴)
222		simplrl 786	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐶 ∈ On)
223	1, 3, 4	cantnfs 9621	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
224	223	biimpd 231	. . . . . . . . 9 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
225	224	adantld 494	. . . . . . . 8 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
226	225	imp 410	. . . . . . 7 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
227	226	simpld 498	. . . . . 6 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → 𝐹:𝐵⟶𝐴)
228	227	adantr 484	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹:𝐵⟶𝐴)
229		fveqeq2 6876	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑦) = ∅))
230	229	rspccv 3578	. . . . . . 7 ⊢ (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅))
231	230	adantl 485	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅))
232	231	imp 410	. . . . 5 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) ∧ 𝑦 ∈ (𝐵 ∖ 𝐶)) → (𝐹‘𝑦) = ∅)
233	228, 232	suppss 8174	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝐹 supp ∅) ⊆ 𝐶)
234	1, 218, 219, 220, 221, 222, 233	cantnflt2 9628	. . 3 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))
235	234	ex 416	. 2 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))
236	217, 235	impbid 214	1 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1560   ∈ wcel 2142   ≠ wne 2957  ∀wral 3076  ∃wrex 3086  Vcvv 3454   ∖ cdif 3901   ∪ cun 3902   ⊆ wss 3904  ∅c0 4285  ifcif 4480  {csn 4582   class class class wbr 5100  {copab 5162   ↦ cmpt 5181   E cep 5546   × cxp 5645  dom cdm 5647  Ord word 6345  Oncon0 6346  suc csuc 6348  ⟶wf 6517  ‘cfv 6521   Isom wiso 6522  (class class class)co 7396   supp csupp 8140  1_oc1o 8430  2_oc2o 8431   +_o coa 8434   ·_o comu 8435   ↑_o coe 8436   finSupp cfsupp 9307   CNF ccnf 9616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-isom 6530  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-supp 8141  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-seqom 8419  df-1o 8437  df-2o 8438  df-oadd 8441  df-omul 8442  df-oexp 8443  df-er 8678  df-map 8810  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fsupp 9308  df-oi 9458  df-cnf 9617

This theorem is referenced by:  cantnf2  43899