MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ellimc2 Structured version   Visualization version   GIF version

Theorem ellimc2 23361
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.)
Hypotheses
Ref Expression
limccl.f (𝜑𝐹:𝐴⟶ℂ)
limccl.a (𝜑𝐴 ⊆ ℂ)
limccl.b (𝜑𝐵 ∈ ℂ)
ellimc2.k 𝐾 = (TopOpen‘ℂfld)
Assertion
Ref Expression
ellimc2 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢𝐾 (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))))
Distinct variable groups:   𝑤,𝑢,𝐴   𝑢,𝐵,𝑤   𝜑,𝑢,𝑤   𝑢,𝐶,𝑤   𝑢,𝐹,𝑤   𝑢,𝐾,𝑤

Proof of Theorem ellimc2
Dummy variables 𝑧 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 23359 . . . 4 (𝐹 lim 𝐵) ⊆ ℂ
21sseli 3560 . . 3 (𝐶 ∈ (𝐹 lim 𝐵) → 𝐶 ∈ ℂ)
32pm4.71ri 662 . 2 (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ 𝐶 ∈ (𝐹 lim 𝐵)))
4 eqid 2606 . . . . . 6 (𝐾t (𝐴 ∪ {𝐵})) = (𝐾t (𝐴 ∪ {𝐵}))
5 ellimc2.k . . . . . 6 𝐾 = (TopOpen‘ℂfld)
6 eqid 2606 . . . . . 6 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))
7 limccl.f . . . . . 6 (𝜑𝐹:𝐴⟶ℂ)
8 limccl.a . . . . . 6 (𝜑𝐴 ⊆ ℂ)
9 limccl.b . . . . . 6 (𝜑𝐵 ∈ ℂ)
104, 5, 6, 7, 8, 9ellimc 23357 . . . . 5 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
1110adantr 479 . . . 4 ((𝜑𝐶 ∈ ℂ) → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
125cnfldtopon 22325 . . . . . . 7 𝐾 ∈ (TopOn‘ℂ)
139snssd 4277 . . . . . . . 8 (𝜑 → {𝐵} ⊆ ℂ)
148, 13unssd 3747 . . . . . . 7 (𝜑 → (𝐴 ∪ {𝐵}) ⊆ ℂ)
15 resttopon 20714 . . . . . . 7 ((𝐾 ∈ (TopOn‘ℂ) ∧ (𝐴 ∪ {𝐵}) ⊆ ℂ) → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
1612, 14, 15sylancr 693 . . . . . 6 (𝜑 → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
1716adantr 479 . . . . 5 ((𝜑𝐶 ∈ ℂ) → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
1812a1i 11 . . . . 5 ((𝜑𝐶 ∈ ℂ) → 𝐾 ∈ (TopOn‘ℂ))
19 ssun2 3735 . . . . . . 7 {𝐵} ⊆ (𝐴 ∪ {𝐵})
20 snssg 4264 . . . . . . . 8 (𝐵 ∈ ℂ → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵})))
219, 20syl 17 . . . . . . 7 (𝜑 → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵})))
2219, 21mpbiri 246 . . . . . 6 (𝜑𝐵 ∈ (𝐴 ∪ {𝐵}))
2322adantr 479 . . . . 5 ((𝜑𝐶 ∈ ℂ) → 𝐵 ∈ (𝐴 ∪ {𝐵}))
24 elun 3711 . . . . . . . 8 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑧𝐴𝑧 ∈ {𝐵}))
25 velsn 4137 . . . . . . . . 9 (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
2625orbi2i 539 . . . . . . . 8 ((𝑧𝐴𝑧 ∈ {𝐵}) ↔ (𝑧𝐴𝑧 = 𝐵))
2724, 26bitri 262 . . . . . . 7 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑧𝐴𝑧 = 𝐵))
28 simpllr 794 . . . . . . . 8 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑧𝐴𝑧 = 𝐵)) ∧ 𝑧 = 𝐵) → 𝐶 ∈ ℂ)
29 pm5.61 744 . . . . . . . . . 10 (((𝑧𝐴𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵) ↔ (𝑧𝐴 ∧ ¬ 𝑧 = 𝐵))
307ffvelrnda 6249 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (𝐹𝑧) ∈ ℂ)
3130ad2ant2r 778 . . . . . . . . . 10 (((𝜑𝐶 ∈ ℂ) ∧ (𝑧𝐴 ∧ ¬ 𝑧 = 𝐵)) → (𝐹𝑧) ∈ ℂ)
3229, 31sylan2b 490 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ ((𝑧𝐴𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵)) → (𝐹𝑧) ∈ ℂ)
3332anassrs 677 . . . . . . . 8 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑧𝐴𝑧 = 𝐵)) ∧ ¬ 𝑧 = 𝐵) → (𝐹𝑧) ∈ ℂ)
3428, 33ifclda 4066 . . . . . . 7 (((𝜑𝐶 ∈ ℂ) ∧ (𝑧𝐴𝑧 = 𝐵)) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ ℂ)
3527, 34sylan2b 490 . . . . . 6 (((𝜑𝐶 ∈ ℂ) ∧ 𝑧 ∈ (𝐴 ∪ {𝐵})) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ ℂ)
3635, 6fmptd 6274 . . . . 5 ((𝜑𝐶 ∈ ℂ) → (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ)
37 iscnp 20790 . . . . . 6 (((𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ ∧ ∀𝑢𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)))))
3837baibd 945 . . . . 5 ((((𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) ∧ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ∀𝑢𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢))))
3917, 18, 23, 36, 38syl31anc 1320 . . . 4 ((𝜑𝐶 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ∀𝑢𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢))))
40 iftrue 4038 . . . . . . . . . . 11 (𝑧 = 𝐵 → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) = 𝐶)
4140, 6fvmptg 6171 . . . . . . . . . 10 ((𝐵 ∈ (𝐴 ∪ {𝐵}) ∧ 𝐶 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) = 𝐶)
4222, 41sylan 486 . . . . . . . . 9 ((𝜑𝐶 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) = 𝐶)
4342eleq1d 2668 . . . . . . . 8 ((𝜑𝐶 ∈ ℂ) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢𝐶𝑢))
4443imbi1d 329 . . . . . . 7 ((𝜑𝐶 ∈ ℂ) → ((((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢))))
4544adantr 479 . . . . . 6 (((𝜑𝐶 ∈ ℂ) ∧ 𝑢𝐾) → ((((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢))))
465cnfldtop 22326 . . . . . . . . . . 11 𝐾 ∈ Top
47 cnex 9870 . . . . . . . . . . . . . 14 ℂ ∈ V
4847ssex 4722 . . . . . . . . . . . . 13 ((𝐴 ∪ {𝐵}) ⊆ ℂ → (𝐴 ∪ {𝐵}) ∈ V)
4914, 48syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∪ {𝐵}) ∈ V)
5049ad2antrr 757 . . . . . . . . . . 11 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (𝐴 ∪ {𝐵}) ∈ V)
51 restval 15853 . . . . . . . . . . 11 ((𝐾 ∈ Top ∧ (𝐴 ∪ {𝐵}) ∈ V) → (𝐾t (𝐴 ∪ {𝐵})) = ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵}))))
5246, 50, 51sylancr 693 . . . . . . . . . 10 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (𝐾t (𝐴 ∪ {𝐵})) = ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵}))))
5352rexeqdv 3118 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑣 ∈ ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)))
54 vex 3172 . . . . . . . . . . . 12 𝑤 ∈ V
5554inex1 4719 . . . . . . . . . . 11 (𝑤 ∩ (𝐴 ∪ {𝐵})) ∈ V
5655rgenw 2904 . . . . . . . . . 10 𝑤𝐾 (𝑤 ∩ (𝐴 ∪ {𝐵})) ∈ V
57 eqid 2606 . . . . . . . . . . 11 (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))
58 eleq2 2673 . . . . . . . . . . . 12 (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → (𝐵𝑣𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))))
59 imaeq2 5365 . . . . . . . . . . . . 13 (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) = ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))))
6059sseq1d 3591 . . . . . . . . . . . 12 (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢))
6158, 60anbi12d 742 . . . . . . . . . . 11 (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → ((𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢)))
6257, 61rexrnmpt 6259 . . . . . . . . . 10 (∀𝑤𝐾 (𝑤 ∩ (𝐴 ∪ {𝐵})) ∈ V → (∃𝑣 ∈ ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢)))
6356, 62mp1i 13 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (∃𝑣 ∈ ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢)))
6422ad3antrrr 761 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → 𝐵 ∈ (𝐴 ∪ {𝐵}))
65 elin 3754 . . . . . . . . . . . . 13 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↔ (𝐵𝑤𝐵 ∈ (𝐴 ∪ {𝐵})))
6665rbaib 944 . . . . . . . . . . . 12 (𝐵 ∈ (𝐴 ∪ {𝐵}) → (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↔ 𝐵𝑤))
6764, 66syl 17 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↔ 𝐵𝑤))
68 simpllr 794 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → 𝐶 ∈ ℂ)
69 fvex 6095 . . . . . . . . . . . . . . . . 17 (𝐹𝑧) ∈ V
70 ifexg 4103 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ ℂ ∧ (𝐹𝑧) ∈ V) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ V)
7168, 69, 70sylancl 692 . . . . . . . . . . . . . . . 16 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ V)
7271ralrimivw 2946 . . . . . . . . . . . . . . 15 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ V)
73 eqid 2606 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) = (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))
7473fnmpt 5916 . . . . . . . . . . . . . . 15 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ V → (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})))
7573fmpt 6271 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝑤 ∩ (𝐴 ∪ {𝐵}))⟶𝑢)
76 df-f 5791 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝑤 ∩ (𝐴 ∪ {𝐵}))⟶𝑢 ↔ ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
7775, 76bitri 262 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
7877baib 941 . . . . . . . . . . . . . . 15 ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})) → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
7972, 74, 783syl 18 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
80 simplrr 796 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → 𝐶𝑢)
81 inss2 3792 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∩ {𝐵}) ⊆ {𝐵}
8281sseli 3560 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝑤 ∩ {𝐵}) → 𝑧 ∈ {𝐵})
8325, 40sylbi 205 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ {𝐵} → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) = 𝐶)
8483eleq1d 2668 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝐵} → (if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢𝐶𝑢))
8582, 84syl 17 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝑤 ∩ {𝐵}) → (if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢𝐶𝑢))
8680, 85syl5ibrcom 235 . . . . . . . . . . . . . . . 16 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (𝑧 ∈ (𝑤 ∩ {𝐵}) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
8786ralrimiv 2944 . . . . . . . . . . . . . . 15 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢)
88 undif1 3991 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = (𝐴 ∪ {𝐵})
8988ineq2i 3769 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∩ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) = (𝑤 ∩ (𝐴 ∪ {𝐵}))
90 indi 3828 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∩ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) = ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))
9189, 90eqtr3i 2630 . . . . . . . . . . . . . . . . . 18 (𝑤 ∩ (𝐴 ∪ {𝐵})) = ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))
9291raleqi 3115 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢)
93 ralunb 3752 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ∧ ∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
9492, 93bitri 262 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ∧ ∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
9594rbaib 944 . . . . . . . . . . . . . . 15 (∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
9687, 95syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
9779, 96bitr3d 268 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
98 inss2 3792 . . . . . . . . . . . . . . . 16 (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵})
9998sseli 3560 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵})) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
100 eldifsni 4257 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧𝐵)
101 ifnefalse 4044 . . . . . . . . . . . . . . . . 17 (𝑧𝐵 → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) = (𝐹𝑧))
102100, 101syl 17 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐴 ∖ {𝐵}) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) = (𝐹𝑧))
103102eleq1d 2668 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐴 ∖ {𝐵}) → (if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (𝐹𝑧) ∈ 𝑢))
10499, 103syl 17 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵})) → (if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (𝐹𝑧) ∈ 𝑢))
105104ralbiia 2958 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ 𝑢)
10697, 105syl6bb 274 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ 𝑢))
107 df-ima 5038 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = ran ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵})))
108 inss2 3792 . . . . . . . . . . . . . . . 16 (𝑤 ∩ (𝐴 ∪ {𝐵})) ⊆ (𝐴 ∪ {𝐵})
109 resmpt 5353 . . . . . . . . . . . . . . . 16 ((𝑤 ∩ (𝐴 ∪ {𝐵})) ⊆ (𝐴 ∪ {𝐵}) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))))
110108, 109mp1i 13 . . . . . . . . . . . . . . 15 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))))
111110rneqd 5258 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ran ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))))
112107, 111syl5eq 2652 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))))
113112sseq1d 3591 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢 ↔ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
1147ad3antrrr 761 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → 𝐹:𝐴⟶ℂ)
115 ffun 5944 . . . . . . . . . . . . . 14 (𝐹:𝐴⟶ℂ → Fun 𝐹)
116114, 115syl 17 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → Fun 𝐹)
117 difss 3695 . . . . . . . . . . . . . . 15 (𝐴 ∖ {𝐵}) ⊆ 𝐴
11898, 117sstri 3573 . . . . . . . . . . . . . 14 (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ 𝐴
119 fdm 5947 . . . . . . . . . . . . . . 15 (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴)
120114, 119syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → dom 𝐹 = 𝐴)
121118, 120syl5sseqr 3613 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹)
122 funimass4 6139 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹) → ((𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ 𝑢))
123116, 121, 122syl2anc 690 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ((𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ 𝑢))
124106, 113, 1233bitr4d 298 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))
12567, 124anbi12d 742 . . . . . . . . . 10 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ((𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢) ↔ (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
126125rexbidva 3027 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (∃𝑤𝐾 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
12753, 63, 1263bitrd 292 . . . . . . . 8 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
128127anassrs 677 . . . . . . 7 ((((𝜑𝐶 ∈ ℂ) ∧ 𝑢𝐾) ∧ 𝐶𝑢) → (∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
129128pm5.74da 718 . . . . . 6 (((𝜑𝐶 ∈ ℂ) ∧ 𝑢𝐾) → ((𝐶𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
13045, 129bitrd 266 . . . . 5 (((𝜑𝐶 ∈ ℂ) ∧ 𝑢𝐾) → ((((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
131130ralbidva 2964 . . . 4 ((𝜑𝐶 ∈ ℂ) → (∀𝑢𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ ∀𝑢𝐾 (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
13211, 39, 1313bitrd 292 . . 3 ((𝜑𝐶 ∈ ℂ) → (𝐶 ∈ (𝐹 lim 𝐵) ↔ ∀𝑢𝐾 (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
133132pm5.32da 670 . 2 (𝜑 → ((𝐶 ∈ ℂ ∧ 𝐶 ∈ (𝐹 lim 𝐵)) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢𝐾 (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))))
1343, 133syl5bb 270 1 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢𝐾 (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2776  wral 2892  wrex 2893  Vcvv 3169  cdif 3533  cun 3534  cin 3535  wss 3536  ifcif 4032  {csn 4121  cmpt 4634  dom cdm 5025  ran crn 5026  cres 5027  cima 5028  Fun wfun 5781   Fn wfn 5782  wf 5783  cfv 5787  (class class class)co 6524  cc 9787  t crest 15847  TopOpenctopn 15848  fldccnfld 19510  Topctop 20456  TopOnctopon 20457   CnP ccnp 20778   lim climc 23346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-fi 8174  df-sup 8205  df-inf 8206  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-4 10925  df-5 10926  df-6 10927  df-7 10928  df-8 10929  df-9 10930  df-n0 11137  df-z 11208  df-dec 11323  df-uz 11517  df-q 11618  df-rp 11662  df-xneg 11775  df-xadd 11776  df-xmul 11777  df-fz 12150  df-seq 12616  df-exp 12675  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-struct 15640  df-ndx 15641  df-slot 15642  df-base 15643  df-plusg 15724  df-mulr 15725  df-starv 15726  df-tset 15730  df-ple 15731  df-ds 15734  df-unif 15735  df-rest 15849  df-topn 15850  df-topgen 15870  df-psmet 19502  df-xmet 19503  df-met 19504  df-bl 19505  df-mopn 19506  df-cnfld 19511  df-top 20460  df-bases 20461  df-topon 20462  df-topsp 20463  df-cnp 20781  df-xms 21873  df-ms 21874  df-limc 23350
This theorem is referenced by:  limcnlp  23362  ellimc3  23363  limcflf  23365  limcresi  23369  limciun  23378  lhop1lem  23494  limccog  38488
  Copyright terms: Public domain W3C validator