Step | Hyp | Ref
| Expression |
1 | | cncfuni.f |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
2 | | cncfuni.auni |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐵) |
3 | 2 | sselda 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪ 𝐵) |
4 | | eluni2 4440 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝐵
↔ ∃𝑏 ∈
𝐵 𝑥 ∈ 𝑏) |
5 | 3, 4 | sylib 208 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑏 ∈ 𝐵 𝑥 ∈ 𝑏) |
6 | | simp1l 1085 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝜑) |
7 | | simp2 1062 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝑏 ∈ 𝐵) |
8 | | elin 3796 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∩ 𝑏) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝑏)) |
9 | 8 | biimpri 218 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (𝐴 ∩ 𝑏)) |
10 | 9 | adantll 750 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (𝐴 ∩ 𝑏)) |
11 | 10 | 3adant2 1080 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ (𝐴 ∩ 𝑏)) |
12 | | cncfuni.fcn |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ)) |
13 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
14 | 1, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → dom 𝐹 = 𝐴) |
15 | 14 | ineq2d 3814 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑏 ∩ dom 𝐹) = (𝑏 ∩ 𝐴)) |
16 | | incom 3805 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∩ 𝐴) = (𝐴 ∩ 𝑏) |
17 | 15, 16 | syl6req 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 ∩ 𝑏) = (𝑏 ∩ dom 𝐹)) |
18 | 17 | reseq2d 5396 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑏)) = (𝐹 ↾ (𝑏 ∩ dom 𝐹))) |
19 | | frel 6050 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝐴⟶ℂ → Rel 𝐹) |
20 | 1, 19 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Rel 𝐹) |
21 | | resindm 5444 |
. . . . . . . . . . . . . . . . . 18
⊢ (Rel
𝐹 → (𝐹 ↾ (𝑏 ∩ dom 𝐹)) = (𝐹 ↾ 𝑏)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 ↾ (𝑏 ∩ dom 𝐹)) = (𝐹 ↾ 𝑏)) |
23 | 18, 22 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑏)) = (𝐹 ↾ 𝑏)) |
24 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ∩ 𝑏) ⊆ 𝐴 |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 ∩ 𝑏) ⊆ 𝐴) |
26 | | cncfuni.acn |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
27 | 25, 26 | sstrd 3613 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 ∩ 𝑏) ⊆ ℂ) |
28 | | ssid 3624 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℂ
⊆ ℂ |
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ℂ ⊆
ℂ) |
30 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) = ((TopOpen‘ℂfld)
↾t (𝐴
∩ 𝑏)) |
32 | 30 | cnfldtop 22587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(TopOpen‘ℂfld) ∈ Top |
33 | | unicntop 22589 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
34 | 33 | restid 16094 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
35 | 32, 34 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
36 | 35 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . 19
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
37 | 30, 31, 36 | cncfcn 22712 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∩ 𝑏) ⊆ ℂ ∧ ℂ ⊆
ℂ) → ((𝐴 ∩
𝑏)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn
(TopOpen‘ℂfld))) |
38 | 27, 29, 37 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐴 ∩ 𝑏)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn
(TopOpen‘ℂfld))) |
39 | 38 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
= ((𝐴 ∩ 𝑏)–cn→ℂ)) |
40 | 23, 39 | eleq12d 2695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
↔ (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ))) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
↔ (𝐹 ↾ 𝑏) ∈ ((𝐴 ∩ 𝑏)–cn→ℂ))) |
42 | 12, 41 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn
(TopOpen‘ℂfld))) |
43 | 42 | 3adant3 1081 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn
(TopOpen‘ℂfld))) |
44 | 30 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . 16
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
46 | | resttopon 20965 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝐴 ∩ 𝑏) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏))) |
47 | 45, 27, 46 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏))) |
48 | 47 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏))) |
49 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
50 | | cncnp 21084 |
. . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) ∈ (TopOn‘(𝐴 ∩ 𝑏)) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
↔ ((𝐹 ↾ (𝐴 ∩ 𝑏)):(𝐴 ∩ 𝑏)⟶ℂ ∧ ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)))) |
51 | 48, 49, 50 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) Cn (TopOpen‘ℂfld))
↔ ((𝐹 ↾ (𝐴 ∩ 𝑏)):(𝐴 ∩ 𝑏)⟶ℂ ∧ ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)))) |
52 | 43, 51 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((𝐹 ↾ (𝐴 ∩ 𝑏)):(𝐴 ∩ 𝑏)⟶ℂ ∧ ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥))) |
53 | 52 | simprd 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ∀𝑥 ∈ (𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) |
54 | | simp3 1063 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝑥 ∈ (𝐴 ∩ 𝑏)) |
55 | | rspa 2930 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
(𝐴 ∩ 𝑏)(𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥) ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) |
56 | 53, 54, 55 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) |
57 | 32 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈ Top) |
58 | | cnex 10017 |
. . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V |
59 | 58 | ssex 4802 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ⊆ ℂ → 𝐴 ∈ V) |
60 | 26, 59 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ V) |
61 | | restabs 20969 |
. . . . . . . . . . . . . 14
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝐴 ∩ 𝑏) ⊆ 𝐴 ∧ 𝐴 ∈ V) →
(((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) = ((TopOpen‘ℂfld)
↾t (𝐴
∩ 𝑏))) |
62 | 57, 25, 60, 61 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) = ((TopOpen‘ℂfld)
↾t (𝐴
∩ 𝑏))) |
63 | 62 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) = (((TopOpen‘ℂfld)
↾t 𝐴)
↾t (𝐴
∩ 𝑏))) |
64 | 63 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP (TopOpen‘ℂfld))
= ((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))) |
65 | 64 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝜑 →
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥) = (((((TopOpen‘ℂfld)
↾t 𝐴)
↾t (𝐴
∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) |
66 | 65 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
((((TopOpen‘ℂfld) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥) = (((((TopOpen‘ℂfld)
↾t 𝐴)
↾t (𝐴
∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) |
67 | 56, 66 | eleqtrd 2703 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥)) |
68 | | resttop 20964 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝐴 ∈ V) →
((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top) |
69 | 57, 60, 68 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top) |
70 | 69 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top) |
71 | 33 | restuni 20966 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝐴 ⊆ ℂ) → 𝐴 = ∪
((TopOpen‘ℂfld) ↾t 𝐴)) |
72 | 57, 26, 71 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 = ∪
((TopOpen‘ℂfld) ↾t 𝐴)) |
73 | 25, 72 | sseqtrd 3641 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∩ 𝑏) ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝐴)) |
74 | 73 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐴 ∩ 𝑏) ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝐴)) |
75 | | cncfuni.opn |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐴 ∩ 𝑏) ∈
((TopOpen‘ℂfld) ↾t 𝐴)) |
76 | 75 | 3adant3 1081 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐴 ∩ 𝑏) ∈
((TopOpen‘ℂfld) ↾t 𝐴)) |
77 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ ∪ ((TopOpen‘ℂfld)
↾t 𝐴) =
∪ ((TopOpen‘ℂfld)
↾t 𝐴) |
78 | 77 | isopn3 20870 |
. . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top ∧ (𝐴 ∩ 𝑏) ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝐴)) → ((𝐴 ∩ 𝑏) ∈
((TopOpen‘ℂfld) ↾t 𝐴) ↔
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) = (𝐴 ∩ 𝑏))) |
79 | 70, 74, 78 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → ((𝐴 ∩ 𝑏) ∈
((TopOpen‘ℂfld) ↾t 𝐴) ↔
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) = (𝐴 ∩ 𝑏))) |
80 | 76, 79 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) →
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) = (𝐴 ∩ 𝑏)) |
81 | 80 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐴 ∩ 𝑏) =
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏))) |
82 | 54, 81 | eleqtrd 2703 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝑥 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏))) |
83 | 72 | feq2d 6031 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹:𝐴⟶ℂ ↔ 𝐹:∪
((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ)) |
84 | 1, 83 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:∪
((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ) |
85 | 84 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝐹:∪
((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ) |
86 | 77, 33 | cnprest 21093 |
. . . . . . . . 9
⊢
(((((TopOpen‘ℂfld) ↾t 𝐴) ∈ Top ∧ (𝐴 ∩ 𝑏) ⊆ ∪
((TopOpen‘ℂfld) ↾t 𝐴)) ∧ (𝑥 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝐴))‘(𝐴 ∩ 𝑏)) ∧ 𝐹:∪
((TopOpen‘ℂfld) ↾t 𝐴)⟶ℂ)) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥) ↔ (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥))) |
87 | 70, 74, 82, 85, 86 | syl22anc 1327 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥) ↔ (𝐹 ↾ (𝐴 ∩ 𝑏)) ∈
(((((TopOpen‘ℂfld) ↾t 𝐴) ↾t (𝐴 ∩ 𝑏)) CnP
(TopOpen‘ℂfld))‘𝑥))) |
88 | 67, 87 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ (𝐴 ∩ 𝑏)) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)) |
89 | 6, 7, 11, 88 | syl3anc 1326 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵 ∧ 𝑥 ∈ 𝑏) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)) |
90 | 89 | rexlimdv3a 3033 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑥 ∈ 𝑏 → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥))) |
91 | 5, 90 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)) |
92 | 91 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)) |
93 | | resttopon 20965 |
. . . . 5
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝐴 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝐴) ∈ (TopOn‘𝐴)) |
94 | 45, 26, 93 | syl2anc 693 |
. . . 4
⊢ (𝜑 →
((TopOpen‘ℂfld) ↾t 𝐴) ∈ (TopOn‘𝐴)) |
95 | | cncnp 21084 |
. . . 4
⊢
((((TopOpen‘ℂfld) ↾t 𝐴) ∈ (TopOn‘𝐴) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)))) |
96 | 94, 45, 95 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝐴⟶ℂ ∧ ∀𝑥 ∈ 𝐴 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝐴) CnP
(TopOpen‘ℂfld))‘𝑥)))) |
97 | 1, 92, 96 | mpbir2and 957 |
. 2
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝐴) Cn
(TopOpen‘ℂfld))) |
98 | | eqid 2622 |
. . . . 5
⊢
((TopOpen‘ℂfld) ↾t 𝐴) =
((TopOpen‘ℂfld) ↾t 𝐴) |
99 | 30, 98, 36 | cncfcn 22712 |
. . . 4
⊢ ((𝐴 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝐴–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝐴) Cn
(TopOpen‘ℂfld))) |
100 | 26, 29, 99 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐴–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝐴) Cn
(TopOpen‘ℂfld))) |
101 | 100 | eqcomd 2628 |
. 2
⊢ (𝜑 →
(((TopOpen‘ℂfld) ↾t 𝐴) Cn (TopOpen‘ℂfld))
= (𝐴–cn→ℂ)) |
102 | 97, 101 | eleqtrd 2703 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→ℂ)) |