| Step |
Hyp |
Ref |
Expression |
| 1 |
|
qtopcmp.1 |
⊢ 𝑋 = ∪ 𝐽 |
| 2 |
|
f1ocnv |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) |
| 3 |
|
f1ofun |
⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → Fun ◡ 𝐹 ) |
| 4 |
2 3
|
syl |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → Fun ◡ 𝐹 ) |
| 5 |
4
|
ad2antlr |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → Fun ◡ 𝐹 ) |
| 6 |
|
simpr |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → 𝑥 ⊆ 𝑌 ) |
| 7 |
|
df-rn |
⊢ ran 𝐹 = dom ◡ 𝐹 |
| 8 |
|
f1ofo |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –onto→ 𝑌 ) |
| 9 |
8
|
ad2antlr |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → 𝐹 : 𝑋 –onto→ 𝑌 ) |
| 10 |
|
forn |
⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ran 𝐹 = 𝑌 ) |
| 11 |
9 10
|
syl |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → ran 𝐹 = 𝑌 ) |
| 12 |
7 11
|
eqtr3id |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → dom ◡ 𝐹 = 𝑌 ) |
| 13 |
6 12
|
sseqtrrd |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → 𝑥 ⊆ dom ◡ 𝐹 ) |
| 14 |
|
funimass4 |
⊢ ( ( Fun ◡ 𝐹 ∧ 𝑥 ⊆ dom ◡ 𝐹 ) → ( ( ◡ 𝐹 “ 𝑥 ) ⊆ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( ◡ 𝐹 ‘ 𝑦 ) ∈ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 15 |
5 13 14
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → ( ( ◡ 𝐹 “ 𝑥 ) ⊆ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( ◡ 𝐹 ‘ 𝑦 ) ∈ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 16 |
|
dfss3 |
⊢ ( 𝑥 ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ) |
| 17 |
|
simprl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ) |
| 18 |
17
|
elin1d |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → 𝑧 ∈ ( 𝐽 qTop 𝐹 ) ) |
| 19 |
1
|
elqtop2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑧 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑧 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑧 ) ∈ 𝐽 ) ) ) |
| 20 |
8 19
|
sylan2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑧 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑧 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑧 ) ∈ 𝐽 ) ) ) |
| 21 |
20
|
ad3antrrr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑧 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑧 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑧 ) ∈ 𝐽 ) ) ) |
| 22 |
18 21
|
mpbid |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ( 𝑧 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑧 ) ∈ 𝐽 ) ) |
| 23 |
22
|
simprd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ( ◡ 𝐹 “ 𝑧 ) ∈ 𝐽 ) |
| 24 |
17
|
elin2d |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → 𝑧 ∈ 𝒫 𝑥 ) |
| 25 |
24
|
elpwid |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → 𝑧 ⊆ 𝑥 ) |
| 26 |
|
imass2 |
⊢ ( 𝑧 ⊆ 𝑥 → ( ◡ 𝐹 “ 𝑧 ) ⊆ ( ◡ 𝐹 “ 𝑥 ) ) |
| 27 |
25 26
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ( ◡ 𝐹 “ 𝑧 ) ⊆ ( ◡ 𝐹 “ 𝑥 ) ) |
| 28 |
23 27
|
elpwd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ( ◡ 𝐹 “ 𝑧 ) ∈ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) |
| 29 |
23 28
|
elind |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ( ◡ 𝐹 “ 𝑧 ) ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 30 |
|
simp-4r |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) |
| 31 |
30 2
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) |
| 32 |
|
f1ofn |
⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 Fn 𝑌 ) |
| 33 |
31 32
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ◡ 𝐹 Fn 𝑌 ) |
| 34 |
6
|
ad2antrr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → 𝑥 ⊆ 𝑌 ) |
| 35 |
25 34
|
sstrd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → 𝑧 ⊆ 𝑌 ) |
| 36 |
|
simprr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → 𝑦 ∈ 𝑧 ) |
| 37 |
|
fnfvima |
⊢ ( ( ◡ 𝐹 Fn 𝑌 ∧ 𝑧 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑧 ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ 𝑧 ) ) |
| 38 |
33 35 36 37
|
syl3anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ 𝑧 ) ) |
| 39 |
|
eleq2 |
⊢ ( 𝑤 = ( ◡ 𝐹 “ 𝑧 ) → ( ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ↔ ( ◡ 𝐹 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ 𝑧 ) ) ) |
| 40 |
39
|
rspcev |
⊢ ( ( ( ◡ 𝐹 “ 𝑧 ) ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ 𝑧 ) ) → ∃ 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) |
| 41 |
29 38 40
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ 𝑧 ) ) → ∃ 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) |
| 42 |
41
|
rexlimdvaa |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) 𝑦 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) |
| 43 |
|
simp-4r |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) |
| 44 |
|
f1ofun |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → Fun 𝐹 ) |
| 45 |
43 44
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → Fun 𝐹 ) |
| 46 |
|
simprl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ) |
| 47 |
46
|
elin2d |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝑤 ∈ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) |
| 48 |
47
|
elpwid |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝑤 ⊆ ( ◡ 𝐹 “ 𝑥 ) ) |
| 49 |
|
funimass2 |
⊢ ( ( Fun 𝐹 ∧ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑥 ) ) → ( 𝐹 “ 𝑤 ) ⊆ 𝑥 ) |
| 50 |
45 48 49
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( 𝐹 “ 𝑤 ) ⊆ 𝑥 ) |
| 51 |
6
|
ad2antrr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝑥 ⊆ 𝑌 ) |
| 52 |
50 51
|
sstrd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( 𝐹 “ 𝑤 ) ⊆ 𝑌 ) |
| 53 |
|
f1of1 |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –1-1→ 𝑌 ) |
| 54 |
43 53
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 ) |
| 55 |
46
|
elin1d |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝑤 ∈ 𝐽 ) |
| 56 |
|
elssuni |
⊢ ( 𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽 ) |
| 57 |
56 1
|
sseqtrrdi |
⊢ ( 𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋 ) |
| 58 |
55 57
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝑤 ⊆ 𝑋 ) |
| 59 |
|
f1imacnv |
⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝑤 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) = 𝑤 ) |
| 60 |
54 58 59
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) = 𝑤 ) |
| 61 |
60 55
|
eqeltrd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 ) |
| 62 |
1
|
elqtop2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 ) ) ) |
| 63 |
8 62
|
sylan2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 ) ) ) |
| 64 |
63
|
ad3antrrr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 ) ) ) |
| 65 |
52 61 64
|
mpbir2and |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) ) |
| 66 |
|
vex |
⊢ 𝑥 ∈ V |
| 67 |
66
|
elpw2 |
⊢ ( ( 𝐹 “ 𝑤 ) ∈ 𝒫 𝑥 ↔ ( 𝐹 “ 𝑤 ) ⊆ 𝑥 ) |
| 68 |
50 67
|
sylibr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( 𝐹 “ 𝑤 ) ∈ 𝒫 𝑥 ) |
| 69 |
65 68
|
elind |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( 𝐹 “ 𝑤 ) ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ) |
| 70 |
6
|
sselda |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑌 ) |
| 71 |
70
|
adantr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝑦 ∈ 𝑌 ) |
| 72 |
|
f1ocnvfv2 |
⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 ) |
| 73 |
43 71 72
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) = 𝑦 ) |
| 74 |
|
f1ofn |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 Fn 𝑋 ) |
| 75 |
74
|
adantl |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → 𝐹 Fn 𝑋 ) |
| 76 |
75
|
ad3antrrr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝐹 Fn 𝑋 ) |
| 77 |
|
simprr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) |
| 78 |
|
fnfvima |
⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑤 ⊆ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ ( 𝐹 “ 𝑤 ) ) |
| 79 |
76 58 77 78
|
syl3anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ ( 𝐹 “ 𝑤 ) ) |
| 80 |
73 79
|
eqeltrrd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → 𝑦 ∈ ( 𝐹 “ 𝑤 ) ) |
| 81 |
|
eleq2 |
⊢ ( 𝑧 = ( 𝐹 “ 𝑤 ) → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ( 𝐹 “ 𝑤 ) ) ) |
| 82 |
81
|
rspcev |
⊢ ( ( ( 𝐹 “ 𝑤 ) ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ∧ 𝑦 ∈ ( 𝐹 “ 𝑤 ) ) → ∃ 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) 𝑦 ∈ 𝑧 ) |
| 83 |
69 80 82
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) → ∃ 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) 𝑦 ∈ 𝑧 ) |
| 84 |
83
|
rexlimdvaa |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 → ∃ 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) 𝑦 ∈ 𝑧 ) ) |
| 85 |
42 84
|
impbid |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) 𝑦 ∈ 𝑧 ↔ ∃ 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) |
| 86 |
|
eluni2 |
⊢ ( 𝑦 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ↔ ∃ 𝑧 ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) 𝑦 ∈ 𝑧 ) |
| 87 |
|
eluni2 |
⊢ ( ( ◡ 𝐹 ‘ 𝑦 ) ∈ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ( ◡ 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) |
| 88 |
85 86 87
|
3bitr4g |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ↔ ( ◡ 𝐹 ‘ 𝑦 ) ∈ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 89 |
88
|
ralbidva |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 ( ◡ 𝐹 ‘ 𝑦 ) ∈ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 90 |
16 89
|
bitrid |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → ( 𝑥 ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 ( ◡ 𝐹 ‘ 𝑦 ) ∈ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 91 |
15 90
|
bitr4d |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → ( ( ◡ 𝐹 “ 𝑥 ) ⊆ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ↔ 𝑥 ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ) ) |
| 92 |
|
eltg |
⊢ ( 𝐽 ∈ TopBases → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ( topGen ‘ 𝐽 ) ↔ ( ◡ 𝐹 “ 𝑥 ) ⊆ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 93 |
92
|
ad2antrr |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ( topGen ‘ 𝐽 ) ↔ ( ◡ 𝐹 “ 𝑥 ) ⊆ ∪ ( 𝐽 ∩ 𝒫 ( ◡ 𝐹 “ 𝑥 ) ) ) ) |
| 94 |
|
ovex |
⊢ ( 𝐽 qTop 𝐹 ) ∈ V |
| 95 |
|
eltg |
⊢ ( ( 𝐽 qTop 𝐹 ) ∈ V → ( 𝑥 ∈ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ↔ 𝑥 ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ) ) |
| 96 |
94 95
|
mp1i |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → ( 𝑥 ∈ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ↔ 𝑥 ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 𝑥 ) ) ) |
| 97 |
91 93 96
|
3bitr4d |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ 𝑥 ⊆ 𝑌 ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ ( topGen ‘ 𝐽 ) ↔ 𝑥 ∈ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ) ) |
| 98 |
97
|
pm5.32da |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ( topGen ‘ 𝐽 ) ) ↔ ( 𝑥 ⊆ 𝑌 ∧ 𝑥 ∈ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ) ) ) |
| 99 |
|
tgtopon |
⊢ ( 𝐽 ∈ TopBases → ( topGen ‘ 𝐽 ) ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
| 100 |
99
|
adantr |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( topGen ‘ 𝐽 ) ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
| 101 |
1
|
fveq2i |
⊢ ( TopOn ‘ 𝑋 ) = ( TopOn ‘ ∪ 𝐽 ) |
| 102 |
100 101
|
eleqtrrdi |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( topGen ‘ 𝐽 ) ∈ ( TopOn ‘ 𝑋 ) ) |
| 103 |
8
|
adantl |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → 𝐹 : 𝑋 –onto→ 𝑌 ) |
| 104 |
|
elqtop3 |
⊢ ( ( ( topGen ‘ 𝐽 ) ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑥 ∈ ( ( topGen ‘ 𝐽 ) qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ( topGen ‘ 𝐽 ) ) ) ) |
| 105 |
102 103 104
|
syl2anc |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑥 ∈ ( ( topGen ‘ 𝐽 ) qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ( topGen ‘ 𝐽 ) ) ) ) |
| 106 |
|
unitg |
⊢ ( ( 𝐽 qTop 𝐹 ) ∈ V → ∪ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) = ∪ ( 𝐽 qTop 𝐹 ) ) |
| 107 |
94 106
|
ax-mp |
⊢ ∪ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) = ∪ ( 𝐽 qTop 𝐹 ) |
| 108 |
1
|
elqtop2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) ) |
| 109 |
8 108
|
sylan2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) ) |
| 110 |
|
velpw |
⊢ ( 𝑥 ∈ 𝒫 𝑌 ↔ 𝑥 ⊆ 𝑌 ) |
| 111 |
110
|
biranri |
⊢ ( ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) → 𝑥 ∈ 𝒫 𝑌 ) |
| 112 |
109 111
|
biimtrdi |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) → 𝑥 ∈ 𝒫 𝑌 ) ) |
| 113 |
112
|
ssrdv |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ⊆ 𝒫 𝑌 ) |
| 114 |
|
sspwuni |
⊢ ( ( 𝐽 qTop 𝐹 ) ⊆ 𝒫 𝑌 ↔ ∪ ( 𝐽 qTop 𝐹 ) ⊆ 𝑌 ) |
| 115 |
113 114
|
sylib |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ∪ ( 𝐽 qTop 𝐹 ) ⊆ 𝑌 ) |
| 116 |
107 115
|
eqsstrid |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ∪ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ⊆ 𝑌 ) |
| 117 |
|
sspwuni |
⊢ ( ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ⊆ 𝒫 𝑌 ↔ ∪ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ⊆ 𝑌 ) |
| 118 |
116 117
|
sylibr |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ⊆ 𝒫 𝑌 ) |
| 119 |
118
|
sseld |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑥 ∈ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) → 𝑥 ∈ 𝒫 𝑌 ) ) |
| 120 |
119 110
|
imbitrdi |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑥 ∈ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) → 𝑥 ⊆ 𝑌 ) ) |
| 121 |
120
|
pm4.71rd |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑥 ∈ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ↔ ( 𝑥 ⊆ 𝑌 ∧ 𝑥 ∈ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ) ) ) |
| 122 |
98 105 121
|
3bitr4d |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝑥 ∈ ( ( topGen ‘ 𝐽 ) qTop 𝐹 ) ↔ 𝑥 ∈ ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ) ) |
| 123 |
122
|
eqrdv |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( topGen ‘ 𝐽 ) qTop 𝐹 ) = ( topGen ‘ ( 𝐽 qTop 𝐹 ) ) ) |