Step | Hyp | Ref
| Expression |
1 | | cnextf.1 |
. . . . 5
⊢ 𝐶 = ∪
𝐽 |
2 | | cnextf.2 |
. . . . 5
⊢ 𝐵 = ∪
𝐾 |
3 | | cnextf.3 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) |
4 | | cnextf.4 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Haus) |
5 | | cnextf.5 |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
6 | | cnextf.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
7 | | cnextf.6 |
. . . . 5
⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶) |
8 | | cnextf.7 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | cnextf 21680 |
. . . 4
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵) |
10 | | ffn 5958 |
. . . 4
⊢ (((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵 → ((𝐽CnExt𝐾)‘𝐹) Fn 𝐶) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) Fn 𝐶) |
12 | | fnssres 5918 |
. . 3
⊢ ((((𝐽CnExt𝐾)‘𝐹) Fn 𝐶 ∧ 𝐴 ⊆ 𝐶) → (((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴) Fn 𝐴) |
13 | 11, 6, 12 | syl2anc 691 |
. 2
⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴) Fn 𝐴) |
14 | | ffn 5958 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
15 | 5, 14 | syl 17 |
. 2
⊢ (𝜑 → 𝐹 Fn 𝐴) |
16 | | fvres 6117 |
. . . 4
⊢ (𝑦 ∈ 𝐴 → ((((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴)‘𝑦) = (((𝐽CnExt𝐾)‘𝐹)‘𝑦)) |
17 | 16 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴)‘𝑦) = (((𝐽CnExt𝐾)‘𝐹)‘𝑦)) |
18 | 6 | sselda 3568 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐶) |
19 | 1, 2, 3, 4, 5, 6, 7, 8 | cnextfvval 21679 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑦) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹)) |
20 | 18, 19 | syldan 486 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((𝐽CnExt𝐾)‘𝐹)‘𝑦) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹)) |
21 | 5 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐵) |
22 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
23 | 1 | restuni 20776 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
24 | 3, 6, 23 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
25 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
26 | 22, 25 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ∪ (𝐽 ↾t 𝐴)) |
27 | | cnextfres1.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) |
28 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
((cls‘𝐽)‘𝐴) ∈ V |
29 | 7, 28 | syl6eqelr 2697 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ V) |
30 | 29, 6 | ssexd 4733 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ V) |
31 | | resttop 20774 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top) |
32 | 3, 30, 31 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Top) |
33 | | haustop 20945 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) |
34 | 4, 33 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ Top) |
35 | 24 | feq2d 5944 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐹:∪ (𝐽 ↾t 𝐴)⟶𝐵)) |
36 | 5, 35 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:∪ (𝐽 ↾t 𝐴)⟶𝐵) |
37 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ ∪ (𝐽
↾t 𝐴) =
∪ (𝐽 ↾t 𝐴) |
38 | 37, 2 | cnnei 20896 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:∪
(𝐽 ↾t
𝐴)⟶𝐵) → (𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ ∀𝑦 ∈ ∪ (𝐽 ↾t 𝐴)∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤)) |
39 | 32, 34, 36, 38 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ↔ ∀𝑦 ∈ ∪ (𝐽 ↾t 𝐴)∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤)) |
40 | 27, 39 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ ∪ (𝐽 ↾t 𝐴)∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤) |
41 | 40 | r19.21bi 2916 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ (𝐽 ↾t 𝐴)) → ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤) |
42 | 26, 41 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤) |
43 | 42 | r19.21bi 2916 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})) → ∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤) |
44 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐽 ∈ Top) |
45 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐴 ⊆ 𝐶) |
46 | | snssi 4280 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝐴 → {𝑦} ⊆ 𝐴) |
47 | 46 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → {𝑦} ⊆ 𝐴) |
48 | 1 | neitr 20794 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ∧ {𝑦} ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)) |
49 | 44, 45, 47, 48 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘{𝑦}) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)) |
50 | 49 | rexeqdv 3122 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤 ↔ ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤)) |
51 | 50 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})) → (∃𝑣 ∈ ((nei‘(𝐽 ↾t 𝐴))‘{𝑦})(𝐹 “ 𝑣) ⊆ 𝑤 ↔ ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤)) |
52 | 43, 51 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})) → ∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤) |
53 | 52 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤) |
54 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Haus) |
55 | 2 | toptopon 20548 |
. . . . . . . . . 10
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝐵)) |
56 | 55 | biimpi 205 |
. . . . . . . . 9
⊢ (𝐾 ∈ Top → 𝐾 ∈ (TopOn‘𝐵)) |
57 | 54, 33, 56 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ (TopOn‘𝐵)) |
58 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((cls‘𝐽)‘𝐴) = 𝐶) |
59 | 18, 58 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ((cls‘𝐽)‘𝐴)) |
60 | 1 | toptopon 20548 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝐶)) |
61 | 3, 60 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐶)) |
62 | 61 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐶)) |
63 | | trnei 21506 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝐶) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑦 ∈ 𝐶) → (𝑦 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
64 | 62, 45, 18, 63 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴))) |
65 | 59, 64 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴)) |
66 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐹:𝐴⟶𝐵) |
67 | | flfnei 21605 |
. . . . . . . 8
⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) → ((𝐹‘𝑦) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ↔ ((𝐹‘𝑦) ∈ 𝐵 ∧ ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤))) |
68 | 57, 65, 66, 67 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ↔ ((𝐹‘𝑦) ∈ 𝐵 ∧ ∀𝑤 ∈ ((nei‘𝐾)‘{(𝐹‘𝑦)})∃𝑣 ∈ (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)(𝐹 “ 𝑣) ⊆ 𝑤))) |
69 | 21, 53, 68 | mpbir2and 959 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹)) |
70 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐶 ↔ 𝑦 ∈ 𝐶)) |
71 | 70 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ 𝑦 ∈ 𝐶))) |
72 | | sneq 4135 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
73 | 72 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((nei‘𝐽)‘{𝑥}) = ((nei‘𝐽)‘{𝑦})) |
74 | 73 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (((nei‘𝐽)‘{𝑥}) ↾t 𝐴) = (((nei‘𝐽)‘{𝑦}) ↾t 𝐴)) |
75 | 74 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))) |
76 | 75 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹)) |
77 | 76 | neeq1d 2841 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅ ↔ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅)) |
78 | 71, 77 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅))) |
79 | 78, 8 | chvarv 2251 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅) |
80 | 18, 79 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅) |
81 | 2 | hausflf2 21612 |
. . . . . . 7
⊢ (((𝐾 ∈ Haus ∧
(((nei‘𝐽)‘{𝑦}) ↾t 𝐴) ∈ (Fil‘𝐴) ∧ 𝐹:𝐴⟶𝐵) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≠ ∅) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≈
1𝑜) |
82 | 54, 65, 66, 80, 81 | syl31anc 1321 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≈
1𝑜) |
83 | | en1eqsn 8075 |
. . . . . 6
⊢ (((𝐹‘𝑦) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ∧ ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) ≈ 1𝑜) →
((𝐾 fLimf
(((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) = {(𝐹‘𝑦)}) |
84 | 69, 82, 83 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) = {(𝐹‘𝑦)}) |
85 | 84 | unieqd 4382 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) = ∪ {(𝐹‘𝑦)}) |
86 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘𝑦) ∈ V |
87 | 86 | unisn 4387 |
. . . 4
⊢ ∪ {(𝐹‘𝑦)} = (𝐹‘𝑦) |
88 | 85, 87 | syl6eq 2660 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∪
((𝐾 fLimf
(((nei‘𝐽)‘{𝑦}) ↾t 𝐴))‘𝐹) = (𝐹‘𝑦)) |
89 | 17, 20, 88 | 3eqtrd 2648 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
90 | 13, 15, 89 | eqfnfvd 6222 |
1
⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴) = 𝐹) |