cantnfresb - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cantnfresb		Structured version Visualization version GIF version

Theorem cantnfresb 42007

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 ∖ 2_o) ∧ 𝐵 ∈ 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 2733	. . . . . . . . . . 11 ⊢ dom (𝐴 CNF 𝐵) = dom (𝐴 CNF 𝐵)
2		eldifi 4125	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (On ∖ 2_o) → 𝐴 ∈ On)
3	2	adantr 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → 𝐴 ∈ On)
4		simpr 486	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → 𝐵 ∈ On)
5		eqid 2733	. . . . . . . . . . 11 ⊢ {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}
6	1, 3, 4, 5	cantnf 9684	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑_o 𝐵)))
7	6	adantr 482	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑_o 𝐵)))
8		simpr 486	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
9		ondif2 8497	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ (On ∖ 2_o) ↔ (𝐴 ∈ On ∧ 1_o ∈ 𝐴))
10	9	simprbi 498	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (On ∖ 2_o) → 1_o ∈ 𝐴)
11		dif20el 8500	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (On ∖ 2_o) → ∅ ∈ 𝐴)
12	10, 11	ifcld 4573	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (On ∖ 2_o) → if(𝑦 = 𝐶, 1_o, ∅) ∈ 𝐴)
13	12	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ 𝐵) → if(𝑦 = 𝐶, 1_o, ∅) ∈ 𝐴)
14	13	fmpttd 7110	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)):𝐵⟶𝐴)
15	11	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → ∅ ∈ 𝐴)
16		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))
17	4, 15, 16	sniffsupp 9391	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) finSupp ∅)
18	1, 3, 4	cantnfs 9657	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)):𝐵⟶𝐴 ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) finSupp ∅)))
19	14, 17, 18	mpbir2and 712	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ∈ dom (𝐴 CNF 𝐵))
20	19	adantr 482	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ∈ dom (𝐴 CNF 𝐵))
21		isorel 7318	. . . . . . . . 9 ⊢ (((𝐴 CNF 𝐵) Isom {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑_o 𝐵)) ∧ (𝐹 ∈ dom (𝐴 CNF 𝐵) ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ∈ dom (𝐴 CNF 𝐵))) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)))))
22	7, 8, 20, 21	syl12anc 836	. . . . . . . 8 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)))))
23	22	adantrl 715	. . . . . . 7 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)))))
24	23	adantr 482	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)))))
25		fvexd 6903	. . . . . . 7 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) ∈ V)
26		epelg 5580	. . . . . . 7 ⊢ (((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) ∈ V → (((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)))))
27	25, 26	syl 17	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)))))
28	2	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐴 ∈ On)
29		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐵 ∈ On)
30		fconst6g 6777	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ 𝐴 → (𝐵 × {∅}):𝐵⟶𝐴)
31	11, 30	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ (On ∖ 2_o) → (𝐵 × {∅}):𝐵⟶𝐴)
32	31	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}):𝐵⟶𝐴)
33	4, 15	fczfsuppd 9377	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) finSupp ∅)
34	1, 3, 4	cantnfs 9657	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → ((𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp ∅)))
35	32, 33, 34	mpbir2and 712	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
36	35	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐵 × {∅}) ∈ dom (𝐴 CNF 𝐵))
37		simpr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵)
38	10	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → 1_o ∈ 𝐴)
39		fczsupp0 8173	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 × {∅}) supp ∅) = ∅
40		0ss 4395	. . . . . . . . . . . . . . . 16 ⊢ ∅ ⊆ 𝐶
41	39, 40	eqsstri 4015	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 × {∅}) supp ∅) ⊆ 𝐶
42	41	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝐵 × {∅}) supp ∅) ⊆ 𝐶)
43		0ex 5306	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ∈ V
44	43	fvconst2 7200	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ 𝐵 → ((𝐵 × {∅})‘𝑦) = ∅)
45	44	ifeq2d 4547	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = 𝐶, 1_o, ((𝐵 × {∅})‘𝑦)) = if(𝑦 = 𝐶, 1_o, ∅))
46	45	mpteq2ia 5250	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ((𝐵 × {∅})‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))
47	46	eqcomi 2742	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ((𝐵 × {∅})‘𝑦)))
48	1, 28, 29, 36, 37, 38, 42, 47	cantnfp1 9672	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ∈ dom (𝐴 CNF 𝐵) ∧ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) = (((𝐴 ↑_o 𝐶) ·_o 1_o) +_o ((𝐴 CNF 𝐵)‘(𝐵 × {∅})))))
49	48	simprd 497	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) = (((𝐴 ↑_o 𝐶) ·_o 1_o) +_o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
50	49	adantrl 715	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) = (((𝐴 ↑_o 𝐶) ·_o 1_o) +_o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))
51		oecl 8532	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑_o 𝐶) ∈ On)
52	3, 51	sylan 581	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐴 ↑_o 𝐶) ∈ On)
53		om1 8538	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ↑_o 𝐶) ∈ On → ((𝐴 ↑_o 𝐶) ·_o 1_o) = (𝐴 ↑_o 𝐶))
54	52, 53	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 ↑_o 𝐶) ·_o 1_o) = (𝐴 ↑_o 𝐶))
55	1, 3, 4, 15	cantnf0 9666	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
56	55	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) = ∅)
57	54, 56	oveq12d 7422	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑_o 𝐶) ·_o 1_o) +_o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = ((𝐴 ↑_o 𝐶) +_o ∅))
58		oa0 8511	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ↑_o 𝐶) ∈ On → ((𝐴 ↑_o 𝐶) +_o ∅) = (𝐴 ↑_o 𝐶))
59	52, 58	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐴 ↑_o 𝐶) +_o ∅) = (𝐴 ↑_o 𝐶))
60	57, 59	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (((𝐴 ↑_o 𝐶) ·_o 1_o) +_o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑_o 𝐶))
61	60	adantrr 716	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 ↑_o 𝐶) ·_o 1_o) +_o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑_o 𝐶))
62	50, 61	eqtrd 2773	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) = (𝐴 ↑_o 𝐶))
63	62	eleq2d 2820	. . . . . . . . 9 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶)))
64	63	exp32 422	. . . . . . . 8 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝐶 ∈ On → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶)))))
65	64	adantrd 493	. . . . . . 7 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶)))))
66	65	imp31 419	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶)))
67	24, 27, 66	3bitrrd 306	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶) ↔ 𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))))
68		fveq1 6887	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑐) = (𝐹‘𝑐))
69	68	eleq1d 2819	. . . . . . . . . 10 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ (𝑏‘𝑐)))
70		fveq1 6887	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐹 → (𝑎‘𝑥) = (𝐹‘𝑥))
71	70	eqeq1d 2735	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐹 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = (𝑏‘𝑥)))
72	71	imbi2d 341	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐹 → ((𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))
73	72	ralbidv 3178	. . . . . . . . . 10 ⊢ (𝑎 = 𝐹 → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))
74	69, 73	anbi12d 632	. . . . . . . . 9 ⊢ (𝑎 = 𝐹 → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))))
75	74	rexbidv 3179	. . . . . . . 8 ⊢ (𝑎 = 𝐹 → (∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))))
76		fveq1 6887	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → (𝑏‘𝑐) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐))
77	76	eleq2d 2820	. . . . . . . . . 10 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐)))
78		fveq1 6887	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → (𝑏‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))
79	78	eqeq2d 2744	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → ((𝐹‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)))
80	79	imbi2d 341	. . . . . . . . . . 11 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → ((𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))))
81	80	ralbidv 3178	. . . . . . . . . 10 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))))
82	77, 81	anbi12d 632	. . . . . . . . 9 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → (((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)))))
83	82	rexbidv 3179	. . . . . . . 8 ⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)))))
84	75, 83, 5	bropabg 42006	. . . . . . 7 ⊢ (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ↔ ((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ∈ V) ∧ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)))))
85		fveq2 6888	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝐶 → (𝐹‘𝑐) = (𝐹‘𝐶))
86	85	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → (𝐹‘𝑐) = (𝐹‘𝐶))
87		eqeq1 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑐 → (𝑦 = 𝐶 ↔ 𝑐 = 𝐶))
88	87	ifbid 4550	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑐 → if(𝑦 = 𝐶, 1_o, ∅) = if(𝑐 = 𝐶, 1_o, ∅))
89		1oex 8471	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1_o ∈ V
90	89, 43	ifex 4577	. . . . . . . . . . . . . . . . . . 19 ⊢ if(𝑐 = 𝐶, 1_o, ∅) ∈ V
91	88, 16, 90	fvmpt 6994	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1_o, ∅))
92		iftrue 4533	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝐶 → if(𝑐 = 𝐶, 1_o, ∅) = 1_o)
93	91, 92	sylan9eqr 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) = 1_o)
94	86, 93	eleq12d 2828	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) ↔ (𝐹‘𝐶) ∈ 1_o))
95		el1o 8490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝐶) ∈ 1_o ↔ (𝐹‘𝐶) = ∅)
96	95	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1_o ↔ (𝐹‘𝐶) = ∅))
97	96	biimpd 228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1_o → (𝐹‘𝐶) = ∅))
98		simpl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 = 𝐶)
99	97, 98	jctild 527	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1_o → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
100	94, 99	sylbid 239	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
101	100	expimpd 455	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
102	91	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1_o, ∅))
103		simpl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 ≠ 𝐶)
104	103	neneqd 2946	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ¬ 𝑐 = 𝐶)
105	104	iffalsed 4538	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → if(𝑐 = 𝐶, 1_o, ∅) = ∅)
106	102, 105	eqtrd 2773	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) = ∅)
107	106	eleq2d 2820	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) ↔ (𝐹‘𝑐) ∈ ∅))
108	107	biimpd 228	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) → (𝐹‘𝑐) ∈ ∅))
109	108	expimpd 455	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐)) → (𝐹‘𝑐) ∈ ∅))
110		noel 4329	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝐹‘𝑐) ∈ ∅
111	110	pm2.21i 119	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑐) ∈ ∅ → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))
112	109, 111	syl6 35	. . . . . . . . . . . . . 14 ⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
113	101, 112	pm2.61ine 3026	. . . . . . . . . . . . 13 ⊢ ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))
114	113	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
115		fveqeq2 6897	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅))
116	115	ralsng 4676	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∈ 𝐵 → (∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅))
117	116	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ↔ (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)))
118	117	biimprd 247	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅)))
119	118	adantl 483	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅)))
120	4	anim1i 616	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
121	120	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐵 ∈ On ∧ 𝐶 ∈ On))
122		pm3.31 451	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)))
123	122	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))))
124		eldif 3957	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶))
125		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑐 = 𝐶)
126	125	eleq1d 2819	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑐 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥))
127		simpl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐵 ∈ On)
128	127	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐵 ∈ On)
129		onelon 6386	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
130	128, 129	sylan 581	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
131		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ On)
132		ontri1 6395	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥))
133	130, 131, 132	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥))
134	133	con2bid 355	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝑥 ↔ ¬ 𝑥 ⊆ 𝐶))
135		onsssuc 6451	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶))
136	130, 131, 135	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 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 580	. . . . . . . . . . . . . . . . . . . . 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(𝑦 = 𝐶, 1_o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))))
143		eldifi 4125	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) → 𝑥 ∈ 𝐵)
144	143	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ 𝐵)
145		eqeq1 2737	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝐶 ↔ 𝑥 = 𝐶))
146	145	ifbid 4550	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → if(𝑦 = 𝐶, 1_o, ∅) = if(𝑥 = 𝐶, 1_o, ∅))
147	89, 43	ifex 4577	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ if(𝑥 = 𝐶, 1_o, ∅) ∈ V
148	146, 16, 147	fvmpt 6994	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1_o, ∅))
149	144, 148	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1_o, ∅))
150	128, 143, 129	syl2an 597	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ On)
151		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ On → Ord 𝑥)
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → Ord 𝑥)
153		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐵 ∈ On → Ord 𝐵)
154	153	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → Ord 𝐵)
155		simplr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐶 ∈ On)
156		ordeldifsucon 41942	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Ord 𝐵 ∧ 𝐶 ∈ On) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)))
157	154, 155, 156	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)))
158	157	biimpa 478	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥))
159		ordirr 6379	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥)
160		eleq1 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥))
161	160	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = 𝐶 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝐶 ∈ 𝑥))
162	159, 161	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Ord 𝑥 → (𝑥 = 𝐶 → ¬ 𝐶 ∈ 𝑥))
163	162	con2d 134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Ord 𝑥 → (𝐶 ∈ 𝑥 → ¬ 𝑥 = 𝐶))
164	163	adantld 492	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Ord 𝑥 → ((𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥) → ¬ 𝑥 = 𝐶))
165	152, 158, 164	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ¬ 𝑥 = 𝐶)
166	165	iffalsed 4538	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → if(𝑥 = 𝐶, 1_o, ∅) = ∅)
167	149, 166	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥) = ∅)
168	167	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥) ↔ (𝐹‘𝑥) = ∅))
169	168	biimpd 228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅))
170	169	ex 414	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅)))
171	170	a2d 29	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ∅)))
172	123, 142, 171	3syld 60	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ∅)))
173	172	ralimdv2 3164	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
174	121, 173	sylan 581	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
175	174	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅))
176		ralun 4191	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅)
177	176	adantll 713	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅)
178		undif3 4289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶}))
179		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵)
180	179	snssd 4811	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵)
181		ssequn1 4179	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∪ 𝐵) = 𝐵)
182	180, 181	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ 𝐵) = 𝐵)
183		simpl 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ On)
184		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐶 ∈ On → Ord 𝐶)
185		orddif 6457	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Ord 𝐶 → 𝐶 = (suc 𝐶 ∖ {𝐶}))
186	183, 184, 185	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 = (suc 𝐶 ∖ {𝐶}))
187	186	eqcomd 2739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (suc 𝐶 ∖ {𝐶}) = 𝐶)
188	182, 187	difeq12d 4122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶})) = (𝐵 ∖ 𝐶))
189	178, 188	eqtrid 2785	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
190	189	adantll 713	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
191	190	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶))
192	191	raleqdv 3326	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
193	192	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
194	177, 193	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)
195	194	ex 414	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
196	175, 195	syld 47	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
197	196	expl 459	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
198	114, 119, 197	3syld 60	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐)) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
199	198	expdimp 454	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
200	199	impd 412	. . . . . . . . 9 ⊢ (((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
201	200	rexlimdva 3156	. . . . . . . 8 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
202	201	adantld 492	. . . . . . 7 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) ∈ V) ∧ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅))‘𝑥)))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
203	84, 202	biimtrid 241	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
204	203	adantlrr 720	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1_o, ∅)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
205	67, 204	sylbid 239	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
206	205	ex 414	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
207		ral0 4511	. . . . 5 ⊢ ∀𝑥 ∈ ∅ (𝐹‘𝑥) = ∅
208		ssdif0 4362	. . . . . . 7 ⊢ (𝐵 ⊆ 𝐶 ↔ (𝐵 ∖ 𝐶) = ∅)
209	208	biimpi 215	. . . . . 6 ⊢ (𝐵 ⊆ 𝐶 → (𝐵 ∖ 𝐶) = ∅)
210	209	raleqdv 3326	. . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ ∅ (𝐹‘𝑥) = ∅))
211	207, 210	mpbiri 258	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)
212	211	a1i13 27	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐵 ⊆ 𝐶 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)))
213	184	adantr 482	. . . 4 ⊢ ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → Ord 𝐶)
214	153	adantl 483	. . . 4 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → Ord 𝐵)
215		ordtri2or 6459	. . . 4 ⊢ ((Ord 𝐶 ∧ Ord 𝐵) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶))
216	213, 214, 215	syl2anr 598	. . 3 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶))
217	206, 212, 216	mpjaod 859	. 2 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
218	3	ad2antrr 725	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐴 ∈ On)
219		simpllr 775	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐵 ∈ On)
220		simplrr 777	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹 ∈ dom (𝐴 CNF 𝐵))
221	15	ad2antrr 725	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ∅ ∈ 𝐴)
222		simplrl 776	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐶 ∈ On)
223	1, 3, 4	cantnfs 9657	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
224	223	biimpd 228	. . . . . . . . 9 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → (𝐹 ∈ dom (𝐴 CNF 𝐵) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
225	224	adantld 492	. . . . . . . 8 ⊢ ((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) → ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
226	225	imp 408	. . . . . . 7 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
227	226	simpld 496	. . . . . 6 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → 𝐹:𝐵⟶𝐴)
228	227	adantr 482	. . . . 5 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹:𝐵⟶𝐴)
229		fveqeq2 6897	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑦) = ∅))
230	229	rspccv 3609	. . . . . . 7 ⊢ (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅))
231	230	adantl 483	. . . . . 6 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅))
232	231	imp 408	. . . . 5 ⊢ (((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) ∧ 𝑦 ∈ (𝐵 ∖ 𝐶)) → (𝐹‘𝑦) = ∅)
233	228, 232	suppss 8174	. . . 4 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝐹 supp ∅) ⊆ 𝐶)
234	1, 218, 219, 220, 221, 222, 233	cantnflt2 9664	. . 3 ⊢ ((((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶))
235	234	ex 414	. 2 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶)))
236	217, 235	impbid 211	1 ⊢ (((𝐴 ∈ (On ∖ 2_o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑_o 𝐶) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ∖ cdif 3944 ∪ cun 3945 ⊆ wss 3947 ∅c0 4321 ifcif 4527 {csn 4627 class class class wbr 5147 {copab 5209 ↦ cmpt 5230 E cep 5578 × cxp 5673 dom cdm 5675 Ord word 6360 Oncon0 6361 suc csuc 6363 ⟶wf 6536 ‘cfv 6540 Isom wiso 6541 (class class class)co 7404 supp csupp 8141 1_oc1o 8454 2_oc2o 8455 +_o coa 8458 ·_o comu 8459 ↑_o coe 8460 finSupp cfsupp 9357 CNF ccnf 9652

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7720

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 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 7360 df-ov 7407 df-oprab 7408 df-mpo 7409 df-om 7851 df-1st 7970 df-2nd 7971 df-supp 8142 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-seqom 8443 df-1o 8461 df-2o 8462 df-oadd 8465 df-omul 8466 df-oexp 8467 df-er 8699 df-map 8818 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-fsupp 9358 df-oi 9501 df-cnf 9653

This theorem is referenced by: cantnf2 42008

W3C validator