Step |
Hyp |
Ref |
Expression |
1 |
|
cnextfrel.1 |
⊢ 𝐶 = ∪ 𝐽 |
2 |
|
cnextfrel.2 |
⊢ 𝐵 = ∪ 𝐾 |
3 |
|
haustop |
⊢ ( 𝐾 ∈ Haus → 𝐾 ∈ Top ) |
4 |
1 2
|
cnextrel |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Rel ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) |
5 |
3 4
|
sylanl2 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Rel ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) |
6 |
|
simpllr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐾 ∈ Haus ) |
7 |
1
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐶 ) ) |
8 |
7
|
biimpi |
⊢ ( 𝐽 ∈ Top → 𝐽 ∈ ( TopOn ‘ 𝐶 ) ) |
9 |
8
|
ad3antrrr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐽 ∈ ( TopOn ‘ 𝐶 ) ) |
10 |
|
simplrr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐴 ⊆ 𝐶 ) |
11 |
9 7
|
sylibr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐽 ∈ Top ) |
12 |
1
|
clsss3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐶 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐶 ) |
13 |
11 10 12
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐶 ) |
14 |
|
simpr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) |
15 |
13 14
|
sseldd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝑥 ∈ 𝐶 ) |
16 |
|
trnei |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) ) |
17 |
16
|
biimpa |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝐶 ) ∧ 𝐴 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) |
18 |
9 10 15 14 17
|
syl31anc |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ) |
19 |
|
simplrl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
20 |
2
|
hausflf |
⊢ ( ( 𝐾 ∈ Haus ∧ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
21 |
6 18 19 20
|
syl3anc |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
22 |
21
|
ex |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
23 |
22
|
alrimiv |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ∀ 𝑥 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
24 |
|
moanimv |
⊢ ( ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
25 |
24
|
albii |
⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
26 |
23 25
|
sylibr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
27 |
|
df-br |
⊢ ( 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ 〈 𝑥 , 𝑦 〉 ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) |
28 |
27
|
a1i |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ 〈 𝑥 , 𝑦 〉 ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) ) |
29 |
1 2
|
cnextfval |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
30 |
3 29
|
sylanl2 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
31 |
30
|
eleq2d |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( 〈 𝑥 , 𝑦 〉 ∈ ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) ) |
32 |
|
opeliunxp |
⊢ ( 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
33 |
32
|
a1i |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) ) |
34 |
28 31 33
|
3bitrd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) ) |
35 |
34
|
mobidv |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ∃* 𝑦 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) ) |
36 |
35
|
albidv |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ( ∀ 𝑥 ∃* 𝑦 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) ) |
37 |
26 36
|
mpbird |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → ∀ 𝑥 ∃* 𝑦 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ) |
38 |
|
dffun6 |
⊢ ( Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ↔ ( Rel ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) 𝑦 ) ) |
39 |
5 37 38
|
sylanbrc |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Haus ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ) → Fun ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) ) |