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

Theorem ellimc2 24040
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 24038 . . . 4 (𝐹 lim 𝐵) ⊆ ℂ
21sseli 3823 . . 3 (𝐶 ∈ (𝐹 lim 𝐵) → 𝐶 ∈ ℂ)
32pm4.71ri 558 . 2 (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ 𝐶 ∈ (𝐹 lim 𝐵)))
4 eqid 2825 . . . . . 6 (𝐾t (𝐴 ∪ {𝐵})) = (𝐾t (𝐴 ∪ {𝐵}))
5 ellimc2.k . . . . . 6 𝐾 = (TopOpen‘ℂfld)
6 eqid 2825 . . . . . 6 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))
7 limccl.f . . . . . 6 (𝜑𝐹:𝐴⟶ℂ)
8 limccl.a . . . . . 6 (𝜑𝐴 ⊆ ℂ)
9 limccl.b . . . . . 6 (𝜑𝐵 ∈ ℂ)
104, 5, 6, 7, 8, 9ellimc 24036 . . . . 5 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
1110adantr 474 . . . 4 ((𝜑𝐶 ∈ ℂ) → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
125cnfldtopon 22956 . . . . . . 7 𝐾 ∈ (TopOn‘ℂ)
139snssd 4558 . . . . . . . 8 (𝜑 → {𝐵} ⊆ ℂ)
148, 13unssd 4016 . . . . . . 7 (𝜑 → (𝐴 ∪ {𝐵}) ⊆ ℂ)
15 resttopon 21336 . . . . . . 7 ((𝐾 ∈ (TopOn‘ℂ) ∧ (𝐴 ∪ {𝐵}) ⊆ ℂ) → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
1612, 14, 15sylancr 583 . . . . . 6 (𝜑 → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
1716adantr 474 . . . . 5 ((𝜑𝐶 ∈ ℂ) → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
1812a1i 11 . . . . 5 ((𝜑𝐶 ∈ ℂ) → 𝐾 ∈ (TopOn‘ℂ))
19 ssun2 4004 . . . . . . 7 {𝐵} ⊆ (𝐴 ∪ {𝐵})
20 snssg 4534 . . . . . . . 8 (𝐵 ∈ ℂ → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵})))
219, 20syl 17 . . . . . . 7 (𝜑 → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵})))
2219, 21mpbiri 250 . . . . . 6 (𝜑𝐵 ∈ (𝐴 ∪ {𝐵}))
2322adantr 474 . . . . 5 ((𝜑𝐶 ∈ ℂ) → 𝐵 ∈ (𝐴 ∪ {𝐵}))
24 elun 3980 . . . . . . . 8 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑧𝐴𝑧 ∈ {𝐵}))
25 velsn 4413 . . . . . . . . 9 (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
2625orbi2i 943 . . . . . . . 8 ((𝑧𝐴𝑧 ∈ {𝐵}) ↔ (𝑧𝐴𝑧 = 𝐵))
2724, 26bitri 267 . . . . . . 7 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑧𝐴𝑧 = 𝐵))
28 simpllr 795 . . . . . . . 8 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑧𝐴𝑧 = 𝐵)) ∧ 𝑧 = 𝐵) → 𝐶 ∈ ℂ)
29 pm5.61 1030 . . . . . . . . . 10 (((𝑧𝐴𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵) ↔ (𝑧𝐴 ∧ ¬ 𝑧 = 𝐵))
307ffvelrnda 6608 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (𝐹𝑧) ∈ ℂ)
3130ad2ant2r 755 . . . . . . . . . 10 (((𝜑𝐶 ∈ ℂ) ∧ (𝑧𝐴 ∧ ¬ 𝑧 = 𝐵)) → (𝐹𝑧) ∈ ℂ)
3229, 31sylan2b 589 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ ((𝑧𝐴𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵)) → (𝐹𝑧) ∈ ℂ)
3332anassrs 461 . . . . . . . 8 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑧𝐴𝑧 = 𝐵)) ∧ ¬ 𝑧 = 𝐵) → (𝐹𝑧) ∈ ℂ)
3428, 33ifclda 4340 . . . . . . 7 (((𝜑𝐶 ∈ ℂ) ∧ (𝑧𝐴𝑧 = 𝐵)) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ ℂ)
3527, 34sylan2b 589 . . . . . 6 (((𝜑𝐶 ∈ ℂ) ∧ 𝑧 ∈ (𝐴 ∪ {𝐵})) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ ℂ)
3635fmpttd 6634 . . . . 5 ((𝜑𝐶 ∈ ℂ) → (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ)
37 iscnp 21412 . . . . . 6 (((𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ ∧ ∀𝑢𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)))))
3837baibd 537 . . . . 5 ((((𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) ∧ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ∀𝑢𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢))))
3917, 18, 23, 36, 38syl31anc 1498 . . . 4 ((𝜑𝐶 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ∈ (((𝐾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ∀𝑢𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢))))
40 iftrue 4312 . . . . . . . . . . 11 (𝑧 = 𝐵 → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) = 𝐶)
4140, 6fvmptg 6527 . . . . . . . . . 10 ((𝐵 ∈ (𝐴 ∪ {𝐵}) ∧ 𝐶 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) = 𝐶)
4222, 41sylan 577 . . . . . . . . 9 ((𝜑𝐶 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) = 𝐶)
4342eleq1d 2891 . . . . . . . 8 ((𝜑𝐶 ∈ ℂ) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢𝐶𝑢))
4443imbi1d 333 . . . . . . 7 ((𝜑𝐶 ∈ ℂ) → ((((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢))))
4544adantr 474 . . . . . 6 (((𝜑𝐶 ∈ ℂ) ∧ 𝑢𝐾) → ((((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢))))
465cnfldtop 22957 . . . . . . . . . . 11 𝐾 ∈ Top
47 cnex 10333 . . . . . . . . . . . . . 14 ℂ ∈ V
4847ssex 5027 . . . . . . . . . . . . 13 ((𝐴 ∪ {𝐵}) ⊆ ℂ → (𝐴 ∪ {𝐵}) ∈ V)
4914, 48syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∪ {𝐵}) ∈ V)
5049ad2antrr 719 . . . . . . . . . . 11 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (𝐴 ∪ {𝐵}) ∈ V)
51 restval 16440 . . . . . . . . . . 11 ((𝐾 ∈ Top ∧ (𝐴 ∪ {𝐵}) ∈ V) → (𝐾t (𝐴 ∪ {𝐵})) = ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵}))))
5246, 50, 51sylancr 583 . . . . . . . . . 10 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (𝐾t (𝐴 ∪ {𝐵})) = ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵}))))
5352rexeqdv 3357 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑣 ∈ ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)))
54 vex 3417 . . . . . . . . . . . 12 𝑤 ∈ V
5554inex1 5024 . . . . . . . . . . 11 (𝑤 ∩ (𝐴 ∪ {𝐵})) ∈ V
5655rgenw 3133 . . . . . . . . . 10 𝑤𝐾 (𝑤 ∩ (𝐴 ∪ {𝐵})) ∈ V
57 eqid 2825 . . . . . . . . . . 11 (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))
58 eleq2 2895 . . . . . . . . . . . 12 (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → (𝐵𝑣𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))))
59 imaeq2 5703 . . . . . . . . . . . . 13 (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) = ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))))
6059sseq1d 3857 . . . . . . . . . . . 12 (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢))
6158, 60anbi12d 626 . . . . . . . . . . 11 (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → ((𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢)))
6257, 61rexrnmpt 6618 . . . . . . . . . 10 (∀𝑤𝐾 (𝑤 ∩ (𝐴 ∪ {𝐵})) ∈ V → (∃𝑣 ∈ ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢)))
6356, 62mp1i 13 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (∃𝑣 ∈ ran (𝑤𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢)))
6422ad3antrrr 723 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → 𝐵 ∈ (𝐴 ∪ {𝐵}))
65 elin 4023 . . . . . . . . . . . . 13 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↔ (𝐵𝑤𝐵 ∈ (𝐴 ∪ {𝐵})))
6665rbaib 536 . . . . . . . . . . . 12 (𝐵 ∈ (𝐴 ∪ {𝐵}) → (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↔ 𝐵𝑤))
6764, 66syl 17 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↔ 𝐵𝑤))
68 simpllr 795 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → 𝐶 ∈ ℂ)
69 fvex 6446 . . . . . . . . . . . . . . . . 17 (𝐹𝑧) ∈ V
70 ifexg 4353 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ ℂ ∧ (𝐹𝑧) ∈ V) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ V)
7168, 69, 70sylancl 582 . . . . . . . . . . . . . . . 16 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ V)
7271ralrimivw 3176 . . . . . . . . . . . . . . 15 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ V)
73 eqid 2825 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) = (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))
7473fnmpt 6253 . . . . . . . . . . . . . . 15 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ V → (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})))
7573fmpt 6629 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝑤 ∩ (𝐴 ∪ {𝐵}))⟶𝑢)
76 df-f 6127 . . . . . . . . . . . . . . . . 17 ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))):(𝑤 ∩ (𝐴 ∪ {𝐵}))⟶𝑢 ↔ ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
7775, 76bitri 267 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
7877baib 533 . . . . . . . . . . . . . . 15 ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})) → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
7972, 74, 783syl 18 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
80 simplrr 798 . . . . . . . . . . . . . . . . 17 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → 𝐶𝑢)
81 inss2 4058 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∩ {𝐵}) ⊆ {𝐵}
8281sseli 3823 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ (𝑤 ∩ {𝐵}) → 𝑧 ∈ {𝐵})
8325, 40sylbi 209 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ {𝐵} → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) = 𝐶)
8483eleq1d 2891 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝐵} → (if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢𝐶𝑢))
8582, 84syl 17 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝑤 ∩ {𝐵}) → (if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢𝐶𝑢))
8680, 85syl5ibrcom 239 . . . . . . . . . . . . . . . 16 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (𝑧 ∈ (𝑤 ∩ {𝐵}) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
8786ralrimiv 3174 . . . . . . . . . . . . . . 15 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢)
88 undif1 4266 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = (𝐴 ∪ {𝐵})
8988ineq2i 4038 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∩ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) = (𝑤 ∩ (𝐴 ∪ {𝐵}))
90 indi 4103 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∩ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) = ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))
9189, 90eqtr3i 2851 . . . . . . . . . . . . . . . . . 18 (𝑤 ∩ (𝐴 ∪ {𝐵})) = ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))
9291raleqi 3354 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢)
93 ralunb 4021 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ∧ ∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
9492, 93bitri 267 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ∧ ∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
9594rbaib 536 . . . . . . . . . . . . . . 15 (∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
9687, 95syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
9779, 96bitr3d 273 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢))
98 inss2 4058 . . . . . . . . . . . . . . . 16 (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵})
9998sseli 3823 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵})) → 𝑧 ∈ (𝐴 ∖ {𝐵}))
100 eldifsni 4540 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧𝐵)
101 ifnefalse 4318 . . . . . . . . . . . . . . . . 17 (𝑧𝐵 → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) = (𝐹𝑧))
102100, 101syl 17 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐴 ∖ {𝐵}) → if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) = (𝐹𝑧))
103102eleq1d 2891 . . . . . . . . . . . . . . 15 (𝑧 ∈ (𝐴 ∖ {𝐵}) → (if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (𝐹𝑧) ∈ 𝑢))
10499, 103syl 17 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵})) → (if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ (𝐹𝑧) ∈ 𝑢))
105104ralbiia 3188 . . . . . . . . . . . . 13 (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ 𝑢)
10697, 105syl6bb 279 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ 𝑢))
107 df-ima 5355 . . . . . . . . . . . . . 14 ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = ran ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵})))
108 inss2 4058 . . . . . . . . . . . . . . . 16 (𝑤 ∩ (𝐴 ∪ {𝐵})) ⊆ (𝐴 ∪ {𝐵})
109 resmpt 5686 . . . . . . . . . . . . . . . 16 ((𝑤 ∩ (𝐴 ∪ {𝐵})) ⊆ (𝐴 ∪ {𝐵}) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))))
110108, 109mp1i 13 . . . . . . . . . . . . . . 15 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))))
111110rneqd 5585 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ran ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))))
112107, 111syl5eq 2873 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))))
113112sseq1d 3857 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢 ↔ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) ⊆ 𝑢))
1147ad3antrrr 723 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → 𝐹:𝐴⟶ℂ)
115114ffund 6282 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → Fun 𝐹)
116 difss 3964 . . . . . . . . . . . . . . 15 (𝐴 ∖ {𝐵}) ⊆ 𝐴
11798, 116sstri 3836 . . . . . . . . . . . . . 14 (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ 𝐴
118114fdmd 6287 . . . . . . . . . . . . . 14 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → dom 𝐹 = 𝐴)
119117, 118syl5sseqr 3879 . . . . . . . . . . . . 13 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹)
120 funimass4 6494 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹) → ((𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ 𝑢))
121115, 119, 120syl2anc 581 . . . . . . . . . . . 12 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ((𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹𝑧) ∈ 𝑢))
122106, 113, 1213bitr4d 303 . . . . . . . . . . 11 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))
12367, 122anbi12d 626 . . . . . . . . . 10 ((((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) ∧ 𝑤𝐾) → ((𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢) ↔ (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
124123rexbidva 3259 . . . . . . . . 9 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (∃𝑤𝐾 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
12553, 63, 1243bitrd 297 . . . . . . . 8 (((𝜑𝐶 ∈ ℂ) ∧ (𝑢𝐾𝐶𝑢)) → (∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
126125anassrs 461 . . . . . . 7 ((((𝜑𝐶 ∈ ℂ) ∧ 𝑢𝐾) ∧ 𝐶𝑢) → (∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))
127126pm5.74da 840 . . . . . 6 (((𝜑𝐶 ∈ ℂ) ∧ 𝑢𝐾) → ((𝐶𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
12845, 127bitrd 271 . . . . 5 (((𝜑𝐶 ∈ ℂ) ∧ 𝑢𝐾) → ((((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
129128ralbidva 3194 . . . 4 ((𝜑𝐶 ∈ ℂ) → (∀𝑢𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾t (𝐴 ∪ {𝐵}))(𝐵𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ ∀𝑢𝐾 (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
13011, 39, 1293bitrd 297 . . 3 ((𝜑𝐶 ∈ ℂ) → (𝐶 ∈ (𝐹 lim 𝐵) ↔ ∀𝑢𝐾 (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))
131130pm5.32da 576 . 2 (𝜑 → ((𝐶 ∈ ℂ ∧ 𝐶 ∈ (𝐹 lim 𝐵)) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢𝐾 (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))))
1323, 131syl5bb 275 1 (𝜑 → (𝐶 ∈ (𝐹 lim 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢𝐾 (𝐶𝑢 → ∃𝑤𝐾 (𝐵𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 880  w3a 1113   = wceq 1658  wcel 2166  wne 2999  wral 3117  wrex 3118  Vcvv 3414  cdif 3795  cun 3796  cin 3797  wss 3798  ifcif 4306  {csn 4397  cmpt 4952  dom cdm 5342  ran crn 5343  cres 5344  cima 5345  Fun wfun 6117   Fn wfn 6118  wf 6119  cfv 6123  (class class class)co 6905  cc 10250  t crest 16434  TopOpenctopn 16435  fldccnfld 20106  Topctop 21068  TopOnctopon 21085   CnP ccnp 21400   lim climc 24025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-oadd 7830  df-er 8009  df-map 8124  df-pm 8125  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-fi 8586  df-sup 8617  df-inf 8618  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-7 11419  df-8 11420  df-9 11421  df-n0 11619  df-z 11705  df-dec 11822  df-uz 11969  df-q 12072  df-rp 12113  df-xneg 12232  df-xadd 12233  df-xmul 12234  df-fz 12620  df-seq 13096  df-exp 13155  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-struct 16224  df-ndx 16225  df-slot 16226  df-base 16228  df-plusg 16318  df-mulr 16319  df-starv 16320  df-tset 16324  df-ple 16325  df-ds 16327  df-unif 16328  df-rest 16436  df-topn 16437  df-topgen 16457  df-psmet 20098  df-xmet 20099  df-met 20100  df-bl 20101  df-mopn 20102  df-cnfld 20107  df-top 21069  df-topon 21086  df-topsp 21108  df-bases 21121  df-cnp 21403  df-xms 22495  df-ms 22496  df-limc 24029
This theorem is referenced by:  limcnlp  24041  ellimc3  24042  limcflf  24044  limcresi  24048  limciun  24057  lhop1lem  24175  limccog  40647
  Copyright terms: Public domain W3C validator