Metamath Proof Explorer

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 𝐶 ) ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = ∅ ) )