Metamath Proof Explorer

Theorem ellimc2

Description: Write the definition of a limit directly in terms of open sets of the topology on the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limccl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limccl.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
limccl.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
ellimc2.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion ellimc2 ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 limccl.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 limccl.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3 limccl.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4 ellimc2.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
5 limccl ⊢ ( 𝐹 limℂ 𝐵 ) ⊆ ℂ
6 5 sseli ⊢ ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) → 𝐶 ∈ ℂ )
7 6 pm4.71ri ⊢ ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝐶 ∈ ℂ ∧ 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ) )
8 eqid ⊢ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) )
9 eqid ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) )
10 8 4 9 1 2 3 ellimc ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ) )
12 4 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
13 3 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ ℂ )
14 2 13 unssd ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ )
15 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
16 12 14 15 sylancr ⊢ ( 𝜑 → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) )
18 12 a1i ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → 𝐾 ∈ ( TopOn ‘ ℂ ) )
19 ssun2 ⊢ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } )
20 snssg ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } ) ) )
21 3 20 syl ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( 𝐴 ∪ { 𝐵 } ) ) )
22 19 21 mpbiri ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) )
24 elun ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∨ 𝑧 ∈ { 𝐵 } ) )
25 velsn ⊢ ( 𝑧 ∈ { 𝐵 } ↔ 𝑧 = 𝐵 )
26 25 orbi2i ⊢ ( ( 𝑧 ∈ 𝐴 ∨ 𝑧 ∈ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) )
27 24 26 bitri ⊢ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↔ ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) )
28 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) ) ∧ 𝑧 = 𝐵 ) → 𝐶 ∈ ℂ )
29 pm5.61 ⊢ ( ( ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) ∧ ¬ 𝑧 = 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 = 𝐵 ) )
30 1 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
31 30 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 = 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
32 29 31 sylan2b ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) ∧ ¬ 𝑧 = 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
33 32 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) ) ∧ ¬ 𝑧 = 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
34 28 33 ifclda ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵 ) ) → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
35 27 34 sylan2b ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
36 35 fmpttd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ )
37 iscnp ⊢ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ↔ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ) ) )
38 37 baibd ⊢ ( ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ∈ ( TopOn ‘ ( 𝐴 ∪ { 𝐵 } ) ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) : ( 𝐴 ∪ { 𝐵 } ) ⟶ ℂ ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ↔ ∀ 𝑢 ∈ 𝐾 ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ) )
39 17 18 23 36 38 syl31anc ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) CnP 𝐾 ) ‘ 𝐵 ) ↔ ∀ 𝑢 ∈ 𝐾 ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ) )
40 iftrue ⊢ ( 𝑧 = 𝐵 → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) = 𝐶 )
41 40 9 fvmptg ⊢ ( ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) = 𝐶 )
42 22 41 sylan ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) = 𝐶 )
43 42 eleq1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) ∈ 𝑢 ↔ 𝐶 ∈ 𝑢 ) )
44 43 imbi1d ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ↔ ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ) )
45 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ 𝐾 ) → ( ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ↔ ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ) )
46 4 cnfldtop ⊢ 𝐾 ∈ Top
47 cnex ⊢ ℂ ∈ V
48 47 ssex ⊢ ( ( 𝐴 ∪ { 𝐵 } ) ⊆ ℂ → ( 𝐴 ∪ { 𝐵 } ) ∈ V )
49 14 48 syl ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) ∈ V )
50 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) → ( 𝐴 ∪ { 𝐵 } ) ∈ V )
51 restval ⊢ ( ( 𝐾 ∈ Top ∧ ( 𝐴 ∪ { 𝐵 } ) ∈ V ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ran ( 𝑤 ∈ 𝐾 ↦ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) )
52 46 50 51 sylancr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) → ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) = ran ( 𝑤 ∈ 𝐾 ↦ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) )
53 52 rexeqdv ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) → ( ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ↔ ∃ 𝑣 ∈ ran ( 𝑤 ∈ 𝐾 ↦ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) )
54 vex ⊢ 𝑤 ∈ V
55 54 inex1 ⊢ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∈ V
56 55 rgenw ⊢ ∀ 𝑤 ∈ 𝐾 ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∈ V
57 eqid ⊢ ( 𝑤 ∈ 𝐾 ↦ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) = ( 𝑤 ∈ 𝐾 ↦ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) )
58 eleq2 ⊢ ( 𝑣 = ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) → ( 𝐵 ∈ 𝑣 ↔ 𝐵 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) )
59 imaeq2 ⊢ ( 𝑣 = ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) = ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) )
60 59 sseq1d ⊢ ( 𝑣 = ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) → ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ↔ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
61 58 60 anbi12d ⊢ ( 𝑣 = ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) → ( ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ↔ ( 𝐵 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
62 57 61 rexrnmptw ⊢ ( ∀ 𝑤 ∈ 𝐾 ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∈ V → ( ∃ 𝑣 ∈ ran ( 𝑤 ∈ 𝐾 ↦ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ↔ ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
63 56 62 mp1i ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) → ( ∃ 𝑣 ∈ ran ( 𝑤 ∈ 𝐾 ↦ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ↔ ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
64 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) )
65 elin ⊢ ( 𝐵 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↔ ( 𝐵 ∈ 𝑤 ∧ 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) ) )
66 65 rbaib ⊢ ( 𝐵 ∈ ( 𝐴 ∪ { 𝐵 } ) → ( 𝐵 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↔ 𝐵 ∈ 𝑤 ) )
67 64 66 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( 𝐵 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↔ 𝐵 ∈ 𝑤 ) )
68 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝐶 ∈ ℂ )
69 fvex ⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
70 ifexg ⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) ∈ V ) → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ V )
71 68 69 70 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ V )
72 71 ralrimivw ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ V )
73 eqid ⊢ ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) )
74 73 fnmpt ⊢ ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ V → ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) Fn ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) )
75 73 fmpt ⊢ ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) : ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ⟶ 𝑢 )
76 df-f ⊢ ( ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) : ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ⟶ 𝑢 ↔ ( ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) Fn ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ran ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ⊆ 𝑢 ) )
77 75 76 bitri ⊢ ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ( ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) Fn ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ran ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ⊆ 𝑢 ) )
78 77 baib ⊢ ( ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) Fn ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) → ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ran ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ⊆ 𝑢 ) )
79 72 74 78 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ran ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ⊆ 𝑢 ) )
80 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝐶 ∈ 𝑢 )
81 elinel2 ⊢ ( 𝑧 ∈ ( 𝑤 ∩ { 𝐵 } ) → 𝑧 ∈ { 𝐵 } )
82 25 40 sylbi ⊢ ( 𝑧 ∈ { 𝐵 } → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) = 𝐶 )
83 82 eleq1d ⊢ ( 𝑧 ∈ { 𝐵 } → ( if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ 𝐶 ∈ 𝑢 ) )
84 81 83 syl ⊢ ( 𝑧 ∈ ( 𝑤 ∩ { 𝐵 } ) → ( if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ 𝐶 ∈ 𝑢 ) )
85 80 84 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( 𝑧 ∈ ( 𝑤 ∩ { 𝐵 } ) → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ) )
86 85 ralrimiv ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ∀ 𝑧 ∈ ( 𝑤 ∩ { 𝐵 } ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 )
87 undif1 ⊢ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( 𝐴 ∪ { 𝐵 } )
88 87 ineq2i ⊢ ( 𝑤 ∩ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) = ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) )
89 indi ⊢ ( 𝑤 ∩ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) ) = ( ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ∪ ( 𝑤 ∩ { 𝐵 } ) )
90 88 89 eqtr3i ⊢ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ∪ ( 𝑤 ∩ { 𝐵 } ) )
91 90 raleqi ⊢ ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ∀ 𝑧 ∈ ( ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ∪ ( 𝑤 ∩ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 )
92 ralunb ⊢ ( ∀ 𝑧 ∈ ( ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ∪ ( 𝑤 ∩ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ∧ ∀ 𝑧 ∈ ( 𝑤 ∩ { 𝐵 } ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ) )
93 91 92 bitri ⊢ ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ∧ ∀ 𝑧 ∈ ( 𝑤 ∩ { 𝐵 } ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ) )
94 93 rbaib ⊢ ( ∀ 𝑧 ∈ ( 𝑤 ∩ { 𝐵 } ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 → ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ) )
95 86 94 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ) )
96 79 95 bitr3d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ran ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ⊆ 𝑢 ↔ ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ) )
97 elinel2 ⊢ ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) )
98 eldifsni ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → 𝑧 ≠ 𝐵 )
99 ifnefalse ⊢ ( 𝑧 ≠ 𝐵 → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) )
100 98 99 syl ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) )
101 100 eleq1d ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → ( if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑧 ) ∈ 𝑢 ) )
102 97 101 syl ⊢ ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) → ( if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑧 ) ∈ 𝑢 ) )
103 102 ralbiia ⊢ ( ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ∈ 𝑢 ↔ ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ( 𝐹 ‘ 𝑧 ) ∈ 𝑢 )
104 96 103 bitrdi ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ran ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ⊆ 𝑢 ↔ ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ( 𝐹 ‘ 𝑧 ) ∈ 𝑢 ) )
105 df-ima ⊢ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) = ran ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) )
106 inss2 ⊢ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ⊆ ( 𝐴 ∪ { 𝐵 } )
107 resmpt ⊢ ( ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ⊆ ( 𝐴 ∪ { 𝐵 } ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) = ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) )
108 106 107 mp1i ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) = ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) )
109 108 rneqd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ran ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ↾ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) = ran ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) )
110 105 109 syl5eq ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) = ran ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) )
111 110 sseq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ⊆ 𝑢 ↔ ran ( 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ⊆ 𝑢 ) )
112 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝐹 : 𝐴 ⟶ ℂ )
113 112 ffund ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → Fun 𝐹 )
114 inss2 ⊢ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ ( 𝐴 ∖ { 𝐵 } )
115 difss ⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
116 114 115 sstri ⊢ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ 𝐴
117 112 fdmd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → dom 𝐹 = 𝐴 )
118 116 117 sseqtrrid ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ dom 𝐹 )
119 funimass4 ⊢ ( ( Fun 𝐹 ∧ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ↔ ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ( 𝐹 ‘ 𝑧 ) ∈ 𝑢 ) )
120 113 118 119 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ↔ ∀ 𝑧 ∈ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ( 𝐹 ‘ 𝑧 ) ∈ 𝑢 ) )
121 104 111 120 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ⊆ 𝑢 ↔ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
122 67 121 anbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( 𝐵 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ⊆ 𝑢 ) ↔ ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
123 122 rexbidva ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) → ( ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ ( 𝑤 ∩ ( 𝐴 ∪ { 𝐵 } ) ) ) ⊆ 𝑢 ) ↔ ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
124 53 63 123 3bitrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢 ) ) → ( ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ↔ ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
125 124 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ 𝐾 ) ∧ 𝐶 ∈ 𝑢 ) → ( ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ↔ ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
126 125 pm5.74da ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝐶 ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ↔ ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
127 45 126 bitrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) ∧ 𝑢 ∈ 𝐾 ) → ( ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ↔ ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
128 127 ralbidva ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( ∀ 𝑢 ∈ 𝐾 ( ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) ‘ 𝐵 ) ∈ 𝑢 → ∃ 𝑣 ∈ ( 𝐾 ↾t ( 𝐴 ∪ { 𝐵 } ) ) ( 𝐵 ∈ 𝑣 ∧ ( ( 𝑧 ∈ ( 𝐴 ∪ { 𝐵 } ) ↦ if ( 𝑧 = 𝐵 , 𝐶 , ( 𝐹 ‘ 𝑧 ) ) ) “ 𝑣 ) ⊆ 𝑢 ) ) ↔ ∀ 𝑢 ∈ 𝐾 ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
129 11 39 128 3bitrd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ℂ ) → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ∀ 𝑢 ∈ 𝐾 ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) )
130 129 pm5.32da ⊢ ( 𝜑 → ( ( 𝐶 ∈ ℂ ∧ 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ) )
131 7 130 syl5bb ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ) )