Theorem cantnfresb

Description: A Cantor normal form which sums to less than a certain power has only zeros for larger components. (Contributed by RP, 3-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ dom ( 𝐴 CNF 𝐵 ) = dom ( 𝐴 CNF 𝐵 )
2		eldifi	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → 𝐴 ∈ On )
3	2	adantr	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → 𝐴 ∈ On )
4		simpr	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → 𝐵 ∈ On )
5		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) }
6	1 3 4 5	cantnf	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝐴 CNF 𝐵 ) Isom { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } , E ( dom ( 𝐴 CNF 𝐵 ) , ( 𝐴 ↑o 𝐵 ) ) )
7	6	adantr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) → ( 𝐴 CNF 𝐵 ) Isom { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } , E ( dom ( 𝐴 CNF 𝐵 ) , ( 𝐴 ↑o 𝐵 ) ) )
8		simpr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) → 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) )
9		ondif2	⊢ ( 𝐴 ∈ ( On ∖ 2o ) ↔ ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) )
10	9	simprbi	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → 1o ∈ 𝐴 )
11		dif20el	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → ∅ ∈ 𝐴 )
12	10 11	ifcld	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → if ( 𝑦 = 𝐶 , 1o , ∅ ) ∈ 𝐴 )
13	12	ad2antrr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝑦 ∈ 𝐵 ) → if ( 𝑦 = 𝐶 , 1o , ∅ ) ∈ 𝐴 )
14	13	fmpttd	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) : 𝐵 ⟶ 𝐴 )
15	11	adantr	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ∅ ∈ 𝐴 )
16		eqid	⊢ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) )
17	4 15 16	sniffsupp	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) finSupp ∅ )
18	1 3 4	cantnfs	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ∈ dom ( 𝐴 CNF 𝐵 ) ↔ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) : 𝐵 ⟶ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) finSupp ∅ ) ) )
19	14 17 18	mpbir2and	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ∈ dom ( 𝐴 CNF 𝐵 ) )
20	19	adantr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) → ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ∈ dom ( 𝐴 CNF 𝐵 ) )
21		isorel	⊢ ( ( ( 𝐴 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	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) → ( 𝐹 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) E ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ) )
23	22	adantrl	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐹 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) E ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ) )
24	23	adantr	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) E ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ) )
25		fvexd	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ∈ V )
26		epelg	⊢ ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ∈ V → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) E ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ) )
27	25 26	syl	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝐶 ∈ 𝐵 ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) E ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ) )
28	2	ad2antrr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → 𝐴 ∈ On )
29		simplr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → 𝐵 ∈ On )
30		fconst6g	⊢ ( ∅ ∈ 𝐴 → ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 )
31	11 30	syl	⊢ ( 𝐴 ∈ ( On ∖ 2o ) → ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 )
32	31	adantr	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 )
33	4 15	fczfsuppd	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝐵 × { ∅ } ) finSupp ∅ )
34	1 3 4	cantnfs	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( ( 𝐵 × { ∅ } ) ∈ dom ( 𝐴 CNF 𝐵 ) ↔ ( ( 𝐵 × { ∅ } ) : 𝐵 ⟶ 𝐴 ∧ ( 𝐵 × { ∅ } ) finSupp ∅ ) ) )
35	32 33 34	mpbir2and	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝐵 × { ∅ } ) ∈ dom ( 𝐴 CNF 𝐵 ) )
36	35	adantr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐵 × { ∅ } ) ∈ dom ( 𝐴 CNF 𝐵 ) )
37		simpr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
38	10	ad2antrr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → 1o ∈ 𝐴 )
39		fczsupp0	⊢ ( ( 𝐵 × { ∅ } ) supp ∅ ) = ∅
40		0ss	⊢ ∅ ⊆ 𝐶
41	39 40	eqsstri	⊢ ( ( 𝐵 × { ∅ } ) supp ∅ ) ⊆ 𝐶
42	41	a1i	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐵 × { ∅ } ) supp ∅ ) ⊆ 𝐶 )
43		0ex	⊢ ∅ ∈ V
44	43	fvconst2	⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝐵 × { ∅ } ) ‘ 𝑦 ) = ∅ )
45	44	ifeq2d	⊢ ( 𝑦 ∈ 𝐵 → if ( 𝑦 = 𝐶 , 1o , ( ( 𝐵 × { ∅ } ) ‘ 𝑦 ) ) = if ( 𝑦 = 𝐶 , 1o , ∅ ) )
46	45	mpteq2ia	⊢ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ( ( 𝐵 × { ∅ } ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) )
47	46	eqcomi	⊢ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ( ( 𝐵 × { ∅ } ) ‘ 𝑦 ) ) )
48	1 28 29 36 37 38 42 47	cantnfp1	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ∈ dom ( 𝐴 CNF 𝐵 ) ∧ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) = ( ( ( 𝐴 ↑o 𝐶 ) ·o 1o ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ) ) )
49	48	simprd	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) = ( ( ( 𝐴 ↑o 𝐶 ) ·o 1o ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ) )
50	49	adantrl	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) = ( ( ( 𝐴 ↑o 𝐶 ) ·o 1o ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ) )
51		oecl	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐶 ) ∈ On )
52	3 51	sylan	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( 𝐴 ↑o 𝐶 ) ∈ On )
53		om1	⊢ ( ( 𝐴 ↑o 𝐶 ) ∈ On → ( ( 𝐴 ↑o 𝐶 ) ·o 1o ) = ( 𝐴 ↑o 𝐶 ) )
54	52 53	syl	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐶 ) ·o 1o ) = ( 𝐴 ↑o 𝐶 ) )
55	1 3 4 15	cantnf0	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ∅ )
56	55	adantr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) = ∅ )
57	54 56	oveq12d	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( ( 𝐴 ↑o 𝐶 ) ·o 1o ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ) = ( ( 𝐴 ↑o 𝐶 ) +o ∅ ) )
58		oa0	⊢ ( ( 𝐴 ↑o 𝐶 ) ∈ On → ( ( 𝐴 ↑o 𝐶 ) +o ∅ ) = ( 𝐴 ↑o 𝐶 ) )
59	52 58	syl	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( 𝐴 ↑o 𝐶 ) +o ∅ ) = ( 𝐴 ↑o 𝐶 ) )
60	57 59	eqtrd	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( ( 𝐴 ↑o 𝐶 ) ·o 1o ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ) = ( 𝐴 ↑o 𝐶 ) )
61	60	adantrr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) ) → ( ( ( 𝐴 ↑o 𝐶 ) ·o 1o ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝐵 × { ∅ } ) ) ) = ( 𝐴 ↑o 𝐶 ) )
62	50 61	eqtrd	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) = ( 𝐴 ↑o 𝐶 ) )
63	62	eleq2d	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )
64	63	exp32	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝐶 ∈ On → ( 𝐶 ∈ 𝐵 → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) ) ) ) )
65	64	adantrd	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) → ( 𝐶 ∈ 𝐵 → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) ) ) ) )
66	65	imp31	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝐶 ∈ 𝐵 ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )
67	24 27 66	3bitrrd	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝐶 ∈ 𝐵 ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) ↔ 𝐹 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ) )
68		fveq1	⊢ ( 𝑎 = 𝐹 → ( 𝑎 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑐 ) )
69	68	eleq1d	⊢ ( 𝑎 = 𝐹 → ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ↔ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ) )
70		fveq1	⊢ ( 𝑎 = 𝐹 → ( 𝑎 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
71	70	eqeq1d	⊢ ( 𝑎 = 𝐹 → ( ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) )
72	71	imbi2d	⊢ ( 𝑎 = 𝐹 → ( ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ↔ ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) )
73	72	ralbidv	⊢ ( 𝑎 = 𝐹 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) )
74	69 73	anbi12d	⊢ ( 𝑎 = 𝐹 → ( ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) ) )
75	74	rexbidv	⊢ ( 𝑎 = 𝐹 → ( ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) ↔ ∃ 𝑐 ∈ 𝐵 ( ( 𝐹 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) ) )
76		fveq1	⊢ ( 𝑏 = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ( 𝑏 ‘ 𝑐 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) )
77	76	eleq2d	⊢ ( 𝑏 = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ( ( 𝐹 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ↔ ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ) )
78		fveq1	⊢ ( 𝑏 = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ( 𝑏 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) )
79	78	eqeq2d	⊢ ( 𝑏 = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) )
80	79	imbi2d	⊢ ( 𝑏 = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ( ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ↔ ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) )
81	80	ralbidv	⊢ ( 𝑏 = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) )
82	77 81	anbi12d	⊢ ( 𝑏 = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ( ( ( 𝐹 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) ) )
83	82	rexbidv	⊢ ( 𝑏 = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ( ∃ 𝑐 ∈ 𝐵 ( ( 𝐹 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) ↔ ∃ 𝑐 ∈ 𝐵 ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) ) )
84	75 83 5	bropabg	⊢ ( 𝐹 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ↔ ( ( 𝐹 ∈ V ∧ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ∈ V ) ∧ ∃ 𝑐 ∈ 𝐵 ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) ) )
85		fveq2	⊢ ( 𝑐 = 𝐶 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝐶 ) )
86	85	adantr	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝐶 ) )
87		eqeq1	⊢ ( 𝑦 = 𝑐 → ( 𝑦 = 𝐶 ↔ 𝑐 = 𝐶 ) )
88	87	ifbid	⊢ ( 𝑦 = 𝑐 → if ( 𝑦 = 𝐶 , 1o , ∅ ) = if ( 𝑐 = 𝐶 , 1o , ∅ ) )
89		1oex	⊢ 1o ∈ V
90	89 43	ifex	⊢ if ( 𝑐 = 𝐶 , 1o , ∅ ) ∈ V
91	88 16 90	fvmpt	⊢ ( 𝑐 ∈ 𝐵 → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) = if ( 𝑐 = 𝐶 , 1o , ∅ ) )
92		iftrue	⊢ ( 𝑐 = 𝐶 → if ( 𝑐 = 𝐶 , 1o , ∅ ) = 1o )
93	91 92	sylan9eqr	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) = 1o )
94	86 93	eleq12d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ↔ ( 𝐹 ‘ 𝐶 ) ∈ 1o ) )
95		el1o	⊢ ( ( 𝐹 ‘ 𝐶 ) ∈ 1o ↔ ( 𝐹 ‘ 𝐶 ) = ∅ )
96	95	a1i	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐶 ) ∈ 1o ↔ ( 𝐹 ‘ 𝐶 ) = ∅ ) )
97	96	biimpd	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐶 ) ∈ 1o → ( 𝐹 ‘ 𝐶 ) = ∅ ) )
98		simpl	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵 ) → 𝑐 = 𝐶 )
99	97 98	jctild	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝐶 ) ∈ 1o → ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) ) )
100	94 99	sylbid	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) → ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) ) )
101	100	expimpd	⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ) → ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) ) )
102	91	adantl	⊢ ( ( 𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) = if ( 𝑐 = 𝐶 , 1o , ∅ ) )
103		simpl	⊢ ( ( 𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵 ) → 𝑐 ≠ 𝐶 )
104	103	neneqd	⊢ ( ( 𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ¬ 𝑐 = 𝐶 )
105	104	iffalsed	⊢ ( ( 𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵 ) → if ( 𝑐 = 𝐶 , 1o , ∅ ) = ∅ )
106	102 105	eqtrd	⊢ ( ( 𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) = ∅ )
107	106	eleq2d	⊢ ( ( 𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ↔ ( 𝐹 ‘ 𝑐 ) ∈ ∅ ) )
108	107	biimpd	⊢ ( ( 𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) → ( 𝐹 ‘ 𝑐 ) ∈ ∅ ) )
109	108	expimpd	⊢ ( 𝑐 ≠ 𝐶 → ( ( 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ∅ ) )
110		noel	⊢ ¬ ( 𝐹 ‘ 𝑐 ) ∈ ∅
111	110	pm2.21i	⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ∅ → ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) )
112	109 111	syl6	⊢ ( 𝑐 ≠ 𝐶 → ( ( 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ) → ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) ) )
113	101 112	pm2.61ine	⊢ ( ( 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ) → ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) )
114	113	a1i	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ) → ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) ) )
115		fveqeq2	⊢ ( 𝑥 = 𝐶 → ( ( 𝐹 ‘ 𝑥 ) = ∅ ↔ ( 𝐹 ‘ 𝐶 ) = ∅ ) )
116	115	ralsng	⊢ ( 𝐶 ∈ 𝐵 → ( ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ↔ ( 𝐹 ‘ 𝐶 ) = ∅ ) )
117	116	anbi2d	⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝑐 = 𝐶 ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) ↔ ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) ) )
118	117	biimprd	⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) → ( 𝑐 = 𝐶 ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
119	118	adantl	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝑐 = 𝐶 ∧ ( 𝐹 ‘ 𝐶 ) = ∅ ) → ( 𝑐 = 𝐶 ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
120	4	anim1i	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) )
121	120	adantr	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) )
122		pm3.31	⊢ ( ( 𝑥 ∈ 𝐵 → ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) )
123	122	a1i	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( ( 𝑥 ∈ 𝐵 → ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) )
124		eldif	⊢ ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶 ) )
125		simplr	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑐 = 𝐶 )
126	125	eleq1d	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑐 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥 ) )
127		simpl	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) → 𝐵 ∈ On )
128	127	adantr	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → 𝐵 ∈ On )
129		onelon	⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
130	128 129	sylan	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
131		simpllr	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ On )
132		ontri1	⊢ ( ( 𝑥 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥 ) )
133	130 131 132	syl2anc	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥 ) )
134	133	con2bid	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐶 ∈ 𝑥 ↔ ¬ 𝑥 ⊆ 𝐶 ) )
135		onsssuc	⊢ ( ( 𝑥 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶 ) )
136	130 131 135	syl2anc	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶 ) )
137	136	notbid	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ⊆ 𝐶 ↔ ¬ 𝑥 ∈ suc 𝐶 ) )
138	126 134 137	3bitrrd	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ suc 𝐶 ↔ 𝑐 ∈ 𝑥 ) )
139	138	pm5.32da	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥 ) ) )
140	124 139	bitrid	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥 ) ) )
141	140	biimpd	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥 ) ) )
142	141	imim1d	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) → ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) )
143		eldifi	⊢ ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) → 𝑥 ∈ 𝐵 )
144	143	adantl	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → 𝑥 ∈ 𝐵 )
145		eqeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 𝐶 ↔ 𝑥 = 𝐶 ) )
146	145	ifbid	⊢ ( 𝑦 = 𝑥 → if ( 𝑦 = 𝐶 , 1o , ∅ ) = if ( 𝑥 = 𝐶 , 1o , ∅ ) )
147	89 43	ifex	⊢ if ( 𝑥 = 𝐶 , 1o , ∅ ) ∈ V
148	146 16 147	fvmpt	⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) = if ( 𝑥 = 𝐶 , 1o , ∅ ) )
149	144 148	syl	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) = if ( 𝑥 = 𝐶 , 1o , ∅ ) )
150	128 143 129	syl2an	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → 𝑥 ∈ On )
151		eloni	⊢ ( 𝑥 ∈ On → Ord 𝑥 )
152	150 151	syl	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → Ord 𝑥 )
153		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
154	153	ad2antrr	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → Ord 𝐵 )
155		simplr	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → 𝐶 ∈ On )
156		ordeldifsucon	⊢ ( ( Ord 𝐵 ∧ 𝐶 ∈ On ) → ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥 ) ) )
157	154 155 156	syl2anc	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥 ) ) )
158	157	biimpa	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥 ) )
159		ordirr	⊢ ( Ord 𝑥 → ¬ 𝑥 ∈ 𝑥 )
160		eleq1	⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥 ) )
161	160	notbid	⊢ ( 𝑥 = 𝐶 → ( ¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝐶 ∈ 𝑥 ) )
162	159 161	syl5ibcom	⊢ ( Ord 𝑥 → ( 𝑥 = 𝐶 → ¬ 𝐶 ∈ 𝑥 ) )
163	162	con2d	⊢ ( Ord 𝑥 → ( 𝐶 ∈ 𝑥 → ¬ 𝑥 = 𝐶 ) )
164	163	adantld	⊢ ( Ord 𝑥 → ( ( 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥 ) → ¬ 𝑥 = 𝐶 ) )
165	152 158 164	sylc	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → ¬ 𝑥 = 𝐶 )
166	165	iffalsed	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → if ( 𝑥 = 𝐶 , 1o , ∅ ) = ∅ )
167	149 166	eqtrd	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) = ∅ )
168	167	eqeq2d	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = ∅ ) )
169	168	biimpd	⊢ ( ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ∅ ) )
170	169	ex	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
171	170	a2d	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) → ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
172	123 142 171	3syld	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( ( 𝑥 ∈ 𝐵 → ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
173	172	ralimdv2	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ) ∧ 𝑐 = 𝐶 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
174	121 173	sylan	⊢ ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 = 𝐶 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
175	174	adantr	⊢ ( ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
176		ralun	⊢ ( ( ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∀ 𝑥 ∈ ( { 𝐶 } ∪ ( 𝐵 ∖ suc 𝐶 ) ) ( 𝐹 ‘ 𝑥 ) = ∅ )
177	176	adantll	⊢ ( ( ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∀ 𝑥 ∈ ( { 𝐶 } ∪ ( 𝐵 ∖ suc 𝐶 ) ) ( 𝐹 ‘ 𝑥 ) = ∅ )
178		undif3	⊢ ( { 𝐶 } ∪ ( 𝐵 ∖ suc 𝐶 ) ) = ( ( { 𝐶 } ∪ 𝐵 ) ∖ ( suc 𝐶 ∖ { 𝐶 } ) )
179		simpr	⊢ ( ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
180	179	snssd	⊢ ( ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) → { 𝐶 } ⊆ 𝐵 )
181		ssequn1	⊢ ( { 𝐶 } ⊆ 𝐵 ↔ ( { 𝐶 } ∪ 𝐵 ) = 𝐵 )
182	180 181	sylib	⊢ ( ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) → ( { 𝐶 } ∪ 𝐵 ) = 𝐵 )
183		simpl	⊢ ( ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ On )
184		eloni	⊢ ( 𝐶 ∈ On → Ord 𝐶 )
185		orddif	⊢ ( Ord 𝐶 → 𝐶 = ( suc 𝐶 ∖ { 𝐶 } ) )
186	183 184 185	3syl	⊢ ( ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) → 𝐶 = ( suc 𝐶 ∖ { 𝐶 } ) )
187	186	eqcomd	⊢ ( ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) → ( suc 𝐶 ∖ { 𝐶 } ) = 𝐶 )
188	182 187	difeq12d	⊢ ( ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) → ( ( { 𝐶 } ∪ 𝐵 ) ∖ ( suc 𝐶 ∖ { 𝐶 } ) ) = ( 𝐵 ∖ 𝐶 ) )
189	178 188	eqtrid	⊢ ( ( 𝐶 ∈ On ∧ 𝐶 ∈ 𝐵 ) → ( { 𝐶 } ∪ ( 𝐵 ∖ suc 𝐶 ) ) = ( 𝐵 ∖ 𝐶 ) )
190	189	adantll	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( { 𝐶 } ∪ ( 𝐵 ∖ suc 𝐶 ) ) = ( 𝐵 ∖ 𝐶 ) )
191	190	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 = 𝐶 ) → ( { 𝐶 } ∪ ( 𝐵 ∖ suc 𝐶 ) ) = ( 𝐵 ∖ 𝐶 ) )
192	191	raleqdv	⊢ ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 = 𝐶 ) → ( ∀ 𝑥 ∈ ( { 𝐶 } ∪ ( 𝐵 ∖ suc 𝐶 ) ) ( 𝐹 ‘ 𝑥 ) = ∅ ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
193	192	ad2antrr	⊢ ( ( ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( ∀ 𝑥 ∈ ( { 𝐶 } ∪ ( 𝐵 ∖ suc 𝐶 ) ) ( 𝐹 ‘ 𝑥 ) = ∅ ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
194	177 193	mpbid	⊢ ( ( ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ )
195	194	ex	⊢ ( ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ suc 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
196	175 195	syld	⊢ ( ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 = 𝐶 ) ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
197	196	expl	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝑐 = 𝐶 ∧ ∀ 𝑥 ∈ { 𝐶 } ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
198	114 119 197	3syld	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝑐 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
199	198	expdimp	⊢ ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
200	199	impd	⊢ ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
201	200	rexlimdva	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( ∃ 𝑐 ∈ 𝐵 ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
202	201	adantld	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( ( ( 𝐹 ∈ V ∧ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ∈ V ) ∧ ∃ 𝑐 ∈ 𝐵 ( ( 𝐹 ‘ 𝑐 ) ∈ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
203	84 202	biimtrid	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
204	203	adantlrr	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ∈ 𝐵 ( ( 𝑎 ‘ 𝑐 ) ∈ ( 𝑏 ‘ 𝑐 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑐 ∈ 𝑥 → ( 𝑎 ‘ 𝑥 ) = ( 𝑏 ‘ 𝑥 ) ) ) } ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = 𝐶 , 1o , ∅ ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
205	67 204	sylbid	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ 𝐶 ∈ 𝐵 ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
206	205	ex	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐶 ∈ 𝐵 → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
207		ral0	⊢ ∀ 𝑥 ∈ ∅ ( 𝐹 ‘ 𝑥 ) = ∅
208		ssdif0	⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐵 ∖ 𝐶 ) = ∅ )
209	208	biimpi	⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐵 ∖ 𝐶 ) = ∅ )
210	209	raleqdv	⊢ ( 𝐵 ⊆ 𝐶 → ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ↔ ∀ 𝑥 ∈ ∅ ( 𝐹 ‘ 𝑥 ) = ∅ ) )
211	207 210	mpbiri	⊢ ( 𝐵 ⊆ 𝐶 → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ )
212	211	a1i13	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐵 ⊆ 𝐶 → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) ) )
213	184	adantr	⊢ ( ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) → Ord 𝐶 )
214	153	adantl	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → Ord 𝐵 )
215		ordtri2or	⊢ ( ( Ord 𝐶 ∧ Ord 𝐵 ) → ( 𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶 ) )
216	213 214 215	syl2anr	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶 ) )
217	206 212 216	mpjaod	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )
218	3	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → 𝐴 ∈ On )
219		simpllr	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → 𝐵 ∈ On )
220		simplrr	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) )
221	15	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∅ ∈ 𝐴 )
222		simplrl	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → 𝐶 ∈ On )
223	1 3 4	cantnfs	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )
224	223	biimpd	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) → ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )
225	224	adantld	⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) → ( ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) → ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )
226	225	imp	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) → ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) )
227	226	simpld	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) → 𝐹 : 𝐵 ⟶ 𝐴 )
228	227	adantr	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → 𝐹 : 𝐵 ⟶ 𝐴 )
229		fveqeq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) = ∅ ↔ ( 𝐹 ‘ 𝑦 ) = ∅ ) )
230	229	rspccv	⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ → ( 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) → ( 𝐹 ‘ 𝑦 ) = ∅ ) )
231	230	adantl	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) → ( 𝐹 ‘ 𝑦 ) = ∅ ) )
232	231	imp	⊢ ( ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) → ( 𝐹 ‘ 𝑦 ) = ∅ )
233	228 232	suppss	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( 𝐹 supp ∅ ) ⊆ 𝐶 )
234	1 218 219 220 221 222 233	cantnflt2	⊢ ( ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) )
235	234	ex	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) ) )
236	217 235	impbid	⊢ ( ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐹 ∈ dom ( 𝐴 CNF 𝐵 ) ) ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )