Theorem cantnfresb 42377

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 2731	. . . . . . . . . . 11 ⊢ dom (𝐴 CNF 𝐵) = dom (𝐴 CNF 𝐵)
2		eldifi 4126	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (On ∖ 2o) → 𝐴 ∈ On)
3	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → 𝐴 ∈ On)
4		simpr 484	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
5		eqid 2731	. . . . . . . . . . 11 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}
6	1, 3, 4, 5	cantnf 9692	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵)))
7	6	adantr 480	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵)))
8		simpr 484	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
9		ondif2 8506	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (On ∖ 2o) ↔ (𝐴 ∈ On ∧ 1o ∈ 𝐴))
10	9	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (On ∖ 2o) → 1o ∈ 𝐴)
11		dif20el 8509	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (On ∖ 2o) → ∅ ∈ 𝐴)
12	10, 11	ifcld 4574	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (On ∖ 2o) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴)
13	12	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ 𝐵) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴)
14	13	fmpttd 7116	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴)
15	11	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ∅ ∈ 𝐴)
16		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))
17	4, 15, 16	sniffsupp 9399	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp ∅)
18	1, 3, 4	cantnfs 9665	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴 ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp ∅)))
19	14, 17, 18	mpbir2and 710	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))
20	19	adantr 480	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))
21		isorel 7326	. . . . . . . . 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 834	. . . . . . . 8 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
23	22	adantrl 713	. . . . . . 7 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
24	23	adantr 480	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)))))
25		fvexd 6906	. . . . . . 7 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈ V)
26		epelg 5581	. . . . . . 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 723	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐴 ∈ On)
29		simplr 766	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐵 ∈ On)
30		fconst6g 6780	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ 𝐴 → (𝐵 × {∅}):𝐵⟶𝐴)
31	11, 30	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ (On ∖ 2o) → (𝐵 × {∅}):𝐵⟶𝐴)
32	31	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}):𝐵⟶𝐴)
33	4, 15	fczfsuppd 9385	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) finSupp ∅)
34	1, 3, 4	cantnfs 9665	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
35	32, 33, 34	mpbir2and 710	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
36	35	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
37		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵)
38	10	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 1o ∈ 𝐴)
39		fczsupp0 8182	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 × {∅}) supp ∅) = ∅
40		0ss 4396	. . . . . . . . . . . . . . . 16 ⊢ ∅ ⊆ 𝐶
41	39, 40	eqsstri 4016	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 × {∅}) supp ∅) ⊆ 𝐶
42	41	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝐵 × {∅}) supp ∅) ⊆ 𝐶)
43		0ex 5307	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
44	43	fvconst2 7207	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐵 → ((𝐵 × {∅})‘𝑦) = ∅)
45	44	ifeq2d 4548	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)) = if(𝑦 = 𝐶, 1o, ∅))
46	45	mpteq2ia 5251	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))
47	46	eqcomi 2740	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)))
48	1, 28, 29, 36, 37, 38, 42, 47	cantnfp1 9680	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ∧ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅})))))
49	48	simprd 495	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
50	49	adantrl 713	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
51		oecl 8541	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On)
52	3, 51	sylan 579	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On)
53		om1 8546	. . . . . . . . . . . . . . 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 9674	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
56	55	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
57	54, 56	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = ((𝐴 ↑o 𝐶) +o ∅))
58		oa0 8520	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) +o ∅) = (𝐴 ↑o 𝐶))
59	52, 58	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐶) +o ∅) = (𝐴 ↑o 𝐶))
60	57, 59	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶))
61	60	adantrr 714	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 ↑o 𝐶) ·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶))
62	50, 61	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (𝐴 ↑o 𝐶))
63	62	eleq2d 2818	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))
64	63	exp32 420	. . . . . . . 8 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐶 ∈ On → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))))
65	64	adantrd 491	. . . . . . 7 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))))
66	65	imp31 417	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))
67	24, 27, 66	3bitrrd 306	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ 𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))))
68		fveq1 6890	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑐) = (𝐹‘𝑐))
69	68	eleq1d 2817	. . . . . . . . . 10 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ (𝑏‘𝑐)))
70		fveq1 6890	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑥) = (𝐹‘𝑥))
71	70	eqeq1d 2733	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = (𝑏‘𝑥)))
72	71	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐹 → ((𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))
73	72	ralbidv 3176	. . . . . . . . . 10 ⊢ (𝑎 = 𝐹 → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))
74	69, 73	anbi12d 630	. . . . . . . . 9 ⊢ (𝑎 = 𝐹 → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))))
75	74	rexbidv 3177	. . . . . . . 8 ⊢ (𝑎 = 𝐹 → (∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))))
76		fveq1 6890	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑐) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐))
77	76	eleq2d 2818	. . . . . . . . . 10 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)))
78		fveq1 6890	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))
79	78	eqeq2d 2742	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))
80	79	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
81	80	ralbidv 3176	. . . . . . . . . 10 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
82	77, 81	anbi12d 630	. . . . . . . . 9 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
83	82	rexbidv 3177	. . . . . . . 8 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
84	75, 83, 5	bropabg 42376	. . . . . . 7 ⊢ (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))))
85		fveq2 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝐶 → (𝐹‘𝑐) = (𝐹‘𝐶))
86	85	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → (𝐹‘𝑐) = (𝐹‘𝐶))
87		eqeq1 2735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → (𝑦 = 𝐶 ↔ 𝑐 = 𝐶))
88	87	ifbid 4551	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑐 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑐 = 𝐶, 1o, ∅))
89		1oex 8480	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1o ∈ V
90	89, 43	ifex 4578	. . . . . . . . . . . . . . . . . . 19 ⊢ if(𝑐 = 𝐶, 1o, ∅) ∈ V
91	88, 16, 90	fvmpt 6998	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅))
92		iftrue 4534	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝐶 → if(𝑐 = 𝐶, 1o, ∅) = 1o)
93	91, 92	sylan9eqr 2793	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = 1o)
94	86, 93	eleq12d 2826	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝐶) ∈ 1o))
95		el1o 8499	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅)
96	95	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅))
97	96	biimpd 228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝐹‘𝐶) = ∅))
98		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 = 𝐶)
99	97, 98	jctild 525	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
100	94, 99	sylbid 239	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
101	100	expimpd 453	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
102	91	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅))
103		simpl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 ≠ 𝐶)
104	103	neneqd 2944	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ¬ 𝑐 = 𝐶)
105	104	iffalsed 4539	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → if(𝑐 = 𝐶, 1o, ∅) = ∅)
106	102, 105	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = ∅)
107	106	eleq2d 2818	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝑐) ∈ ∅))
108	107	biimpd 228	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝐹‘𝑐) ∈ ∅))
109	108	expimpd 453	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝐹‘𝑐) ∈ ∅))
110		noel 4330	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝐹‘𝑐) ∈ ∅
111	110	pm2.21i 119	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑐) ∈ ∅ → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))
112	109, 111	syl6 35	. . . . . . . . . . . . . 14 ⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
113	101, 112	pm2.61ine 3024	. . . . . . . . . . . . 13 ⊢ ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))
114	113	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
115		fveqeq2 6900	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅))
116	115	ralsng 4677	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ 𝐵 → (∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅))
117	116	anbi2d 628	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ↔ (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
118	117	biimprd 247	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅)))
119	118	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅)))
120	4	anim1i 614	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
121	120	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
122		pm3.31 449	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))
123	122	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
124		eldif 3958	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶))
125		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑐 = 𝐶)
126	125	eleq1d 2817	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑐 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥))
127		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
128	127	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐵 ∈ On)
129		onelon 6389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
130	128, 129	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
131		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ On)
132		ontri1 6398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥))
133	130, 131, 132	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥))
134	133	con2bid 354	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝑥 ↔ ¬ 𝑥 ⊆ 𝐶))
135		onsssuc 6454	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶))
136	130, 131, 135	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶))
137	136	notbid 318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ⊆ 𝐶 ↔ ¬ 𝑥 ∈ suc 𝐶))
138	126, 134, 137	3bitrrd 306	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ suc 𝐶 ↔ 𝑐 ∈ 𝑥))
139	138	pm5.32da 578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥)))
140	124, 139	bitrid 283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥)))
141	140	biimpd 228	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥)))
142	141	imim1d 82	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))
143		eldifi 4126	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) → 𝑥 ∈ 𝐵)
144	143	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ 𝐵)
145		eqeq1 2735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝐶 ↔ 𝑥 = 𝐶))
146	145	ifbid 4551	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑥 = 𝐶, 1o, ∅))
147	89, 43	ifex 4578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(𝑥 = 𝐶, 1o, ∅) ∈ V
148	146, 16, 147	fvmpt 6998	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅))
149	144, 148	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅))
150	128, 143, 129	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ On)
151		eloni 6374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ On → Ord 𝑥)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → Ord 𝑥)
153		eloni 6374	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐵 ∈ On → Ord 𝐵)
154	153	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → Ord 𝐵)
155		simplr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐶 ∈ On)
156		ordeldifsucon 42312	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝐵 ∧ 𝐶 ∈ On) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)))
157	154, 155, 156	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)))
158	157	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥))
159		ordirr 6382	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥)
160		eleq1 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥))
161	160	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝐶 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝐶 ∈ 𝑥))
162	159, 161	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Ord 𝑥 → (𝑥 = 𝐶 → ¬ 𝐶 ∈ 𝑥))
163	162	con2d 134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝑥 → (𝐶 ∈ 𝑥 → ¬ 𝑥 = 𝐶))
164	163	adantld 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑥 → ((𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥) → ¬ 𝑥 = 𝐶))
165	152, 158, 164	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ¬ 𝑥 = 𝐶)
166	165	iffalsed 4539	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → if(𝑥 = 𝐶, 1o, ∅) = ∅)
167	149, 166	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = ∅)
168	167	eqeq2d 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) ↔ (𝐹‘𝑥) = ∅))
169	168	biimpd 228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅))
170	169	ex 412	. . . . . . . . . . . . . . . . . . 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 3162	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
174	121, 173	sylan 579	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
175	174	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
176		ralun 4192	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅)
177	176	adantll 711	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅)
178		undif3 4290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶}))
179		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵)
180	179	snssd 4812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵)
181		ssequn1 4180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∪ 𝐵) = 𝐵)
182	180, 181	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ 𝐵) = 𝐵)
183		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ On)
184		eloni 6374	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐶 ∈ On → Ord 𝐶)
185		orddif 6460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Ord 𝐶 → 𝐶 = (suc 𝐶 ∖ {𝐶}))
186	183, 184, 185	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 = (suc 𝐶 ∖ {𝐶}))
187	186	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (suc 𝐶 ∖ {𝐶}) = 𝐶)
188	182, 187	difeq12d 4123	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶})) = (𝐵 ∖ 𝐶))
189	178, 188	eqtrid 2783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
190	189	adantll 711	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
191	190	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
192	191	raleqdv 3324	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
193	192	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
194	177, 193	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)
195	194	ex 412	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
196	175, 195	syld 47	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
197	196	expl 457	. . . . . . . . . . . 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 452	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
200	199	impd 410	. . . . . . . . 9 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
201	200	rexlimdva 3154	. . . . . . . 8 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
202	201	adantld 490	. . . . . . 7 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
203	84, 202	biimtrid 241	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
204	203	adantlrr 718	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
205	67, 204	sylbid 239	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
206	205	ex 412	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
207		ral0 4512	. . . . 5 ⊢ ∀𝑥 ∈ ∅ (𝐹‘𝑥) = ∅
208		ssdif0 4363	. . . . . . 7 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐵 ∖ 𝐶) = ∅)
209	208	biimpi 215	. . . . . 6 ⊢ (𝐵 ⊆ 𝐶 → (𝐵 ∖ 𝐶) = ∅)
210	209	raleqdv 3324	. . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ ∅ (𝐹‘𝑥) = ∅))
211	207, 210	mpbiri 258	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)
212	211	a1i13 27	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐵 ⊆ 𝐶 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
213	184	adantr 480	. . . 4 ⊢ ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → Ord 𝐶)
214	153	adantl 481	. . . 4 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → Ord 𝐵)
215		ordtri2or 6462	. . . 4 ⊢ ((Ord 𝐶 ∧ Ord 𝐵) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶))
216	213, 214, 215	syl2anr 596	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶))
217	206, 212, 216	mpjaod 857	. 2 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
218	3	ad2antrr 723	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐴 ∈ On)
219		simpllr 773	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐵 ∈ On)
220		simplrr 775	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
221	15	ad2antrr 723	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ∅ ∈ 𝐴)
222		simplrl 774	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐶 ∈ On)
223	1, 3, 4	cantnfs 9665	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
224	223	biimpd 228	. . . . . . . . 9 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
225	224	adantld 490	. . . . . . . 8 ⊢ ((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
226	225	imp 406	. . . . . . 7 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
227	226	simpld 494	. . . . . 6 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → 𝐹:𝐵⟶𝐴)
228	227	adantr 480	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹:𝐵⟶𝐴)
229		fveqeq2 6900	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑦) = ∅))
230	229	rspccv 3609	. . . . . . 7 ⊢ (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅))
231	230	adantl 481	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅))
232	231	imp 406	. . . . 5 ⊢ (((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) ∧ 𝑦 ∈ (𝐵 ∖ 𝐶)) → (𝐹‘𝑦) = ∅)
233	228, 232	suppss 8183	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝐹 supp ∅) ⊆ 𝐶)
234	1, 218, 219, 220, 221, 222, 233	cantnflt2 9672	. . 3 ⊢ ((((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))
235	234	ex 412	. 2 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)))
236	217, 235	impbid 211	1 ⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1540   ∈ wcel 2105   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  Vcvv 3473   ∖ cdif 3945   ∪ cun 3946   ⊆ wss 3948  ∅c0 4322  ifcif 4528  {csn 4628   class class class wbr 5148  {copab 5210   ↦ cmpt 5231   E cep 5579   × cxp 5674  dom cdm 5676  Ord word 6363  Oncon0 6364  suc csuc 6366  ⟶wf 6539  ‘cfv 6543   Isom wiso 6544  (class class class)co 7412   supp csupp 8150  1_oc1o 8463  2_oc2o 8464   +_o coa 8467   ·_o comu 8468   ↑_o coe 8469   finSupp cfsupp 9365   CNF ccnf 9660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-supp 8151  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-seqom 8452  df-1o 8470  df-2o 8471  df-oadd 8474  df-omul 8475  df-oexp 8476  df-er 8707  df-map 8826  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fsupp 9366  df-oi 9509  df-cnf 9661

This theorem is referenced by:  cantnf2  42378