Step |
Hyp |
Ref |
Expression |
1 |
|
cnrest.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
eqid |
⊢ ∪ 𝐾 = ∪ 𝐾 |
3 |
1 2
|
cnf |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 ) |
4 |
3
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ∪ 𝐾 ) |
5 |
|
simpr |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 ) |
6 |
4 5
|
fssresd |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ∪ 𝐾 ) |
7 |
|
cnvresima |
⊢ ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑜 ) = ( ( ◡ 𝐹 “ 𝑜 ) ∩ 𝐴 ) |
8 |
|
cntop1 |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top ) |
9 |
8
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐽 ∈ Top ) |
10 |
9
|
adantr |
⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑜 ∈ 𝐾 ) → 𝐽 ∈ Top ) |
11 |
1
|
topopn |
⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 ) |
12 |
|
ssexg |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽 ) → 𝐴 ∈ V ) |
13 |
12
|
ancoms |
⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V ) |
14 |
11 13
|
sylan |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V ) |
15 |
8 14
|
sylan |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑜 ∈ 𝐾 ) → 𝐴 ∈ V ) |
17 |
|
cnima |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑜 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑜 ) ∈ 𝐽 ) |
18 |
17
|
adantlr |
⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑜 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑜 ) ∈ 𝐽 ) |
19 |
|
elrestr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ ( ◡ 𝐹 “ 𝑜 ) ∈ 𝐽 ) → ( ( ◡ 𝐹 “ 𝑜 ) ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) ) |
20 |
10 16 18 19
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑜 ∈ 𝐾 ) → ( ( ◡ 𝐹 “ 𝑜 ) ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) ) |
21 |
7 20
|
eqeltrid |
⊢ ( ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑜 ∈ 𝐾 ) → ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑜 ) ∈ ( 𝐽 ↾t 𝐴 ) ) |
22 |
21
|
ralrimiva |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ∀ 𝑜 ∈ 𝐾 ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑜 ) ∈ ( 𝐽 ↾t 𝐴 ) ) |
23 |
1
|
toptopon |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
24 |
8 23
|
sylib |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
25 |
|
resttopon |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ) |
26 |
24 25
|
sylan |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ) |
27 |
|
cntop2 |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top ) |
28 |
27
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐾 ∈ Top ) |
29 |
2
|
toptopon |
⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) |
30 |
28 29
|
sylib |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) |
31 |
|
iscn |
⊢ ( ( ( 𝐽 ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ∪ 𝐾 ∧ ∀ 𝑜 ∈ 𝐾 ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑜 ) ∈ ( 𝐽 ↾t 𝐴 ) ) ) ) |
32 |
26 30 31
|
syl2anc |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ ∪ 𝐾 ∧ ∀ 𝑜 ∈ 𝐾 ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝑜 ) ∈ ( 𝐽 ↾t 𝐴 ) ) ) ) |
33 |
6 22 32
|
mpbir2and |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐾 ) ) |