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 ⊢ φ → F : A ⟶ ℂ
limccl.a ⊢ φ → A ⊆ ℂ
limccl.b ⊢ φ → B ∈ ℂ
ellimc2.k ⊢ K = TopOpen ⁡ ℂ fld
Assertion ellimc2 ⊢ φ → C ∈ F lim ℂ B ↔ C ∈ ℂ ∧ ∀ u ∈ K C ∈ u → ∃ w ∈ K B ∈ w ∧ F w ∩ A ∖ B ⊆ u

Proof

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