Step |
Hyp |
Ref |
Expression |
1 |
|
qtopomap.4 |
⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) |
2 |
|
qtopomap.5 |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) |
3 |
|
qtopomap.6 |
⊢ ( 𝜑 → ran 𝐹 = 𝑌 ) |
4 |
|
qtopomap.7 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) |
5 |
|
qtopss |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ ran 𝐹 = 𝑌 ) → 𝐾 ⊆ ( 𝐽 qTop 𝐹 ) ) |
6 |
2 1 3 5
|
syl3anc |
⊢ ( 𝜑 → 𝐾 ⊆ ( 𝐽 qTop 𝐹 ) ) |
7 |
|
cntop1 |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top ) |
8 |
2 7
|
syl |
⊢ ( 𝜑 → 𝐽 ∈ Top ) |
9 |
|
toptopon2 |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
10 |
8 9
|
sylib |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
11 |
|
cnf2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐹 : ∪ 𝐽 ⟶ 𝑌 ) |
12 |
10 1 2 11
|
syl3anc |
⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 ⟶ 𝑌 ) |
13 |
12
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn ∪ 𝐽 ) |
14 |
|
df-fo |
⊢ ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 ↔ ( 𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 = 𝑌 ) ) |
15 |
13 3 14
|
sylanbrc |
⊢ ( 𝜑 → 𝐹 : ∪ 𝐽 –onto→ 𝑌 ) |
16 |
|
elqtop3 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 : ∪ 𝐽 –onto→ 𝑌 ) → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ) |
17 |
10 15 16
|
syl2anc |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ) |
18 |
|
foimacnv |
⊢ ( ( 𝐹 : ∪ 𝐽 –onto→ 𝑌 ∧ 𝑦 ⊆ 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 ) |
19 |
15 18
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝑌 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 ) |
20 |
19
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 ) |
21 |
|
imaeq2 |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) |
22 |
21
|
eleq1d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( 𝐹 “ 𝑥 ) ∈ 𝐾 ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ∈ 𝐾 ) ) |
23 |
4
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐽 ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) |
24 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ∀ 𝑥 ∈ 𝐽 ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) |
25 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) |
26 |
22 24 25
|
rspcdva |
⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ∈ 𝐾 ) |
27 |
20 26
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑦 ∈ 𝐾 ) |
28 |
27
|
ex |
⊢ ( 𝜑 → ( ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) → 𝑦 ∈ 𝐾 ) ) |
29 |
17 28
|
sylbid |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) → 𝑦 ∈ 𝐾 ) ) |
30 |
29
|
ssrdv |
⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ⊆ 𝐾 ) |
31 |
6 30
|
eqssd |
⊢ ( 𝜑 → 𝐾 = ( 𝐽 qTop 𝐹 ) ) |