Step | Hyp | Ref
| Expression |
1 | | limccl 24038 |
. . . 4
⊢ (𝐹 limℂ 𝐵) ⊆
ℂ |
2 | 1 | sseli 3823 |
. . 3
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → 𝐶 ∈ ℂ) |
3 | 2 | pm4.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
⊢ (𝜑 → 𝐵 ∈ ℂ) |
10 | 4, 5, 6, 7, 8, 9 | ellimc 24036 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
11 | 10 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
12 | 5 | cnfldtopon 22956 |
. . . . . . 7
⊢ 𝐾 ∈
(TopOn‘ℂ) |
13 | 9 | snssd 4558 |
. . . . . . . 8
⊢ (𝜑 → {𝐵} ⊆ ℂ) |
14 | 8, 13 | unssd 4016 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∪ {𝐵}) ⊆ ℂ) |
15 | | resttopon 21336 |
. . . . . . 7
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ (𝐴 ∪ {𝐵}) ⊆ ℂ) →
(𝐾 ↾t
(𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
16 | 12, 14, 15 | sylancr 583 |
. . . . . 6
⊢ (𝜑 → (𝐾 ↾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
17 | 16 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝐾 ↾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
18 | 12 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐾 ∈
(TopOn‘ℂ)) |
19 | | ssun2 4004 |
. . . . . . 7
⊢ {𝐵} ⊆ (𝐴 ∪ {𝐵}) |
20 | | snssg 4534 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵}))) |
21 | 9, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵}))) |
22 | 19, 21 | mpbiri 250 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
23 | 22 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
24 | | elun 3980 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ {𝐵})) |
25 | | velsn 4413 |
. . . . . . . . 9
⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵) |
26 | 25 | orbi2i 943 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 ∨ 𝑧 ∈ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵)) |
27 | 24, 26 | bitri 267 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵)) |
28 | | simpllr 795 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵)) ∧ 𝑧 = 𝐵) → 𝐶 ∈ ℂ) |
29 | | pm5.61 1030 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ ¬ 𝑧 = 𝐵)) |
30 | 7 | ffvelrnda 6608 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ ℂ) |
31 | 30 | ad2ant2r 755 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑧 ∈ 𝐴 ∧ ¬ 𝑧 = 𝐵)) → (𝐹‘𝑧) ∈ ℂ) |
32 | 29, 31 | sylan2b 589 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ ((𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵)) → (𝐹‘𝑧) ∈ ℂ) |
33 | 32 | anassrs 461 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵)) ∧ ¬ 𝑧 = 𝐵) → (𝐹‘𝑧) ∈ ℂ) |
34 | 28, 33 | ifclda 4340 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑧 ∈ 𝐴 ∨ 𝑧 = 𝐵)) → if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ ℂ) |
35 | 27, 34 | sylan2b 589 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑧 ∈ (𝐴 ∪ {𝐵})) → if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ ℂ) |
36 | 35 | fmpttd 6634 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))):(𝐴 ∪ {𝐵})⟶ℂ) |
37 | | iscnp 21412 |
. . . . . 6
⊢ (((𝐾 ↾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))):(𝐴 ∪ {𝐵})⟶ℂ ∧ ∀𝑢 ∈ 𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢))))) |
38 | 37 | baibd 537 |
. . . . 5
⊢ ((((𝐾 ↾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐵 ∈ (𝐴 ∪ {𝐵})) ∧ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))):(𝐴 ∪ {𝐵})⟶ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ∀𝑢 ∈ 𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢)))) |
39 | 17, 18, 23, 36, 38 | syl31anc 1498 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ∀𝑢 ∈ 𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢)))) |
40 | | iftrue 4312 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) = 𝐶) |
41 | 40, 6 | fvmptg 6527 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (𝐴 ∪ {𝐵}) ∧ 𝐶 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) = 𝐶) |
42 | 22, 41 | sylan 577 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) = 𝐶) |
43 | 42 | eleq1d 2891 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) ∈ 𝑢 ↔ 𝐶 ∈ 𝑢)) |
44 | 43 | imbi1d 333 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶 ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢)))) |
45 | 44 | adantr 474 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈ 𝐾) → ((((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶 ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢)))) |
46 | 5 | cnfldtop 22957 |
. . . . . . . . . . 11
⊢ 𝐾 ∈ Top |
47 | | cnex 10333 |
. . . . . . . . . . . . . 14
⊢ ℂ
∈ V |
48 | 47 | ssex 5027 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∪ {𝐵}) ⊆ ℂ → (𝐴 ∪ {𝐵}) ∈ V) |
49 | 14, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∪ {𝐵}) ∈ V) |
50 | 49 | ad2antrr 719 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) → (𝐴 ∪ {𝐵}) ∈ V) |
51 | | restval 16440 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Top ∧ (𝐴 ∪ {𝐵}) ∈ V) → (𝐾 ↾t (𝐴 ∪ {𝐵})) = ran (𝑤 ∈ 𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))) |
52 | 46, 50, 51 | sylancr 583 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) → (𝐾 ↾t (𝐴 ∪ {𝐵})) = ran (𝑤 ∈ 𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))) |
53 | 52 | rexeqdv 3357 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) → (∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑣 ∈ ran (𝑤 ∈ 𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢))) |
54 | | vex 3417 |
. . . . . . . . . . . 12
⊢ 𝑤 ∈ V |
55 | 54 | inex1 5024 |
. . . . . . . . . . 11
⊢ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∈ V |
56 | 55 | rgenw 3133 |
. . . . . . . . . 10
⊢
∀𝑤 ∈
𝐾 (𝑤 ∩ (𝐴 ∪ {𝐵})) ∈ V |
57 | | eqid 2825 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = (𝑤 ∈ 𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵}))) |
58 | | eleq2 2895 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → (𝐵 ∈ 𝑣 ↔ 𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})))) |
59 | | imaeq2 5703 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) = ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵})))) |
60 | 59 | sseq1d 3857 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢 ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢)) |
61 | 58, 60 | anbi12d 626 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑤 ∩ (𝐴 ∪ {𝐵})) → ((𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢) ↔ (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢))) |
62 | 57, 61 | rexrnmpt 6618 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
𝐾 (𝑤 ∩ (𝐴 ∪ {𝐵})) ∈ V → (∃𝑣 ∈ ran (𝑤 ∈ 𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤 ∈ 𝐾 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢))) |
63 | 56, 62 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) → (∃𝑣 ∈ ran (𝑤 ∈ 𝐾 ↦ (𝑤 ∩ (𝐴 ∪ {𝐵})))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤 ∈ 𝐾 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢))) |
64 | 22 | ad3antrrr 723 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
65 | | elin 4023 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↔ (𝐵 ∈ 𝑤 ∧ 𝐵 ∈ (𝐴 ∪ {𝐵}))) |
66 | 65 | rbaib 536 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝐴 ∪ {𝐵}) → (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↔ 𝐵 ∈ 𝑤)) |
67 | 64, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↔ 𝐵 ∈ 𝑤)) |
68 | | simpllr 795 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → 𝐶 ∈ ℂ) |
69 | | fvex 6446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑧) ∈ V |
70 | | ifexg 4353 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ℂ ∧ (𝐹‘𝑧) ∈ V) → if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ V) |
71 | 68, 69, 70 | sylancl 582 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ V) |
72 | 71 | ralrimivw 3176 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ V) |
73 | | eqid 2825 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) = (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) |
74 | 73 | fnmpt 6253 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
(𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ V → (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵}))) |
75 | 73 | fmpt 6629 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
(𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))):(𝑤 ∩ (𝐴 ∪ {𝐵}))⟶𝑢) |
76 | | df-f 6127 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))):(𝑤 ∩ (𝐴 ∪ {𝐵}))⟶𝑢 ↔ ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ⊆ 𝑢)) |
77 | 75, 76 | bitri 267 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧 ∈
(𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ⊆ 𝑢)) |
78 | 77 | baib 533 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) Fn (𝑤 ∩ (𝐴 ∪ {𝐵})) → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ⊆ 𝑢)) |
79 | 72, 74, 78 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ⊆ 𝑢)) |
80 | | simplrr 798 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → 𝐶 ∈ 𝑢) |
81 | | inss2 4058 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∩ {𝐵}) ⊆ {𝐵} |
82 | 81 | sseli 3823 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝑤 ∩ {𝐵}) → 𝑧 ∈ {𝐵}) |
83 | 25, 40 | sylbi 209 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ {𝐵} → if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) = 𝐶) |
84 | 83 | eleq1d 2891 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ {𝐵} → (if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ 𝐶 ∈ 𝑢)) |
85 | 82, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (𝑤 ∩ {𝐵}) → (if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ 𝐶 ∈ 𝑢)) |
86 | 80, 85 | syl5ibrcom 239 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → (𝑧 ∈ (𝑤 ∩ {𝐵}) → if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢)) |
87 | 86 | ralrimiv 3174 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → ∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢) |
88 | | undif1 4266 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = (𝐴 ∪ {𝐵}) |
89 | 88 | ineq2i 4038 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∩ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) = (𝑤 ∩ (𝐴 ∪ {𝐵})) |
90 | | indi 4103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∩ ((𝐴 ∖ {𝐵}) ∪ {𝐵})) = ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵})) |
91 | 89, 90 | eqtr3i 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∩ (𝐴 ∪ {𝐵})) = ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵})) |
92 | 91 | raleqi 3354 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
(𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ ((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢) |
93 | | ralunb 4021 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
((𝑤 ∩ (𝐴 ∖ {𝐵})) ∪ (𝑤 ∩ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ∧ ∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢)) |
94 | 92, 93 | bitri 267 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧 ∈
(𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ∧ ∀𝑧 ∈ (𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢)) |
95 | 94 | rbaib 536 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
(𝑤 ∩ {𝐵})if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢)) |
96 | 87, 95 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → (∀𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢)) |
97 | 79, 96 | bitr3d 273 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → (ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢)) |
98 | | inss2 4058 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵}) |
99 | 98 | sseli 3823 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵})) → 𝑧 ∈ (𝐴 ∖ {𝐵})) |
100 | | eldifsni 4540 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → 𝑧 ≠ 𝐵) |
101 | | ifnefalse 4318 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ≠ 𝐵 → if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) = (𝐹‘𝑧)) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) = (𝐹‘𝑧)) |
103 | 102 | eleq1d 2891 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝐴 ∖ {𝐵}) → (if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ (𝐹‘𝑧) ∈ 𝑢)) |
104 | 99, 103 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵})) → (if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ (𝐹‘𝑧) ∈ 𝑢)) |
105 | 104 | ralbiia 3188 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
(𝑤 ∩ (𝐴 ∖ {𝐵}))if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)) ∈ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ 𝑢) |
106 | 97, 105 | syl6bb 279 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → (ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ 𝑢)) |
107 | | df-ima 5355 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = ran ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) |
108 | | inss2 4058 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∩ (𝐴 ∪ {𝐵})) ⊆ (𝐴 ∪ {𝐵}) |
109 | | resmpt 5686 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∩ (𝐴 ∪ {𝐵})) ⊆ (𝐴 ∪ {𝐵}) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))) |
110 | 108, 109 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))) |
111 | 110 | rneqd 5585 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → ran ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ↾ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))) |
112 | 107, 111 | syl5eq 2873 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) = ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))) |
113 | 112 | sseq1d 3857 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢 ↔ ran (𝑧 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) ⊆ 𝑢)) |
114 | 7 | ad3antrrr 723 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → 𝐹:𝐴⟶ℂ) |
115 | 114 | ffund 6282 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → Fun 𝐹) |
116 | | difss 3964 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 |
117 | 98, 116 | sstri 3836 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ 𝐴 |
118 | 114 | fdmd 6287 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → dom 𝐹 = 𝐴) |
119 | 117, 118 | syl5sseqr 3879 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹) |
120 | | funimass4 6494 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ (𝑤 ∩ (𝐴 ∖ {𝐵})) ⊆ dom 𝐹) → ((𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ 𝑢)) |
121 | 115, 119,
120 | syl2anc 581 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → ((𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢 ↔ ∀𝑧 ∈ (𝑤 ∩ (𝐴 ∖ {𝐵}))(𝐹‘𝑧) ∈ 𝑢)) |
122 | 106, 113,
121 | 3bitr4d 303 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢 ↔ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)) |
123 | 67, 122 | anbi12d 626 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) ∧ 𝑤 ∈ 𝐾) → ((𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢) ↔ (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
124 | 123 | rexbidva 3259 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) → (∃𝑤 ∈ 𝐾 (𝐵 ∈ (𝑤 ∩ (𝐴 ∪ {𝐵})) ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ (𝑤 ∩ (𝐴 ∪ {𝐵}))) ⊆ 𝑢) ↔ ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
125 | 53, 63, 124 | 3bitrd 297 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ 𝐾 ∧ 𝐶 ∈ 𝑢)) → (∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
126 | 125 | anassrs 461 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈ 𝐾) ∧ 𝐶 ∈ 𝑢) → (∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢) ↔ ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))) |
127 | 126 | pm5.74da 840 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈ 𝐾) → ((𝐶 ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
128 | 45, 127 | bitrd 271 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ ℂ) ∧ 𝑢 ∈ 𝐾) → ((((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ (𝐶 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
129 | 128 | ralbidva 3194 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑢 ∈ 𝐾 (((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))‘𝐵) ∈ 𝑢 → ∃𝑣 ∈ (𝐾 ↾t (𝐴 ∪ {𝐵}))(𝐵 ∈ 𝑣 ∧ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧))) “ 𝑣) ⊆ 𝑢)) ↔ ∀𝑢 ∈ 𝐾 (𝐶 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
130 | 11, 39, 129 | 3bitrd 297 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ ∀𝑢 ∈ 𝐾 (𝐶 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))) |
131 | 130 | pm5.32da 576 |
. 2
⊢ (𝜑 → ((𝐶 ∈ ℂ ∧ 𝐶 ∈ (𝐹 limℂ 𝐵)) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝐶 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))) |
132 | 3, 131 | syl5bb 275 |
1
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝐶 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢))))) |