| Step |
Hyp |
Ref |
Expression |
| 1 |
|
qtopcmp.1 |
⊢ 𝑋 = ∪ 𝐽 |
| 2 |
|
f1ofo |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –onto→ 𝑌 ) |
| 3 |
1
|
elqtop2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) ) |
| 4 |
1
|
elqtop2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ↔ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ) |
| 5 |
3 4
|
anbi12d |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ) ) |
| 6 |
2 5
|
sylan2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ) ↔ ( ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ) ) |
| 7 |
|
simpl1l |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝐽 ∈ TopBases ) |
| 8 |
|
simpl2r |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) |
| 9 |
|
simpl3r |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) |
| 10 |
|
simpl1r |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) |
| 11 |
|
f1ocnv |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 ) |
| 12 |
|
f1ofn |
⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 Fn 𝑌 ) |
| 13 |
10 11 12
|
3syl |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ◡ 𝐹 Fn 𝑌 ) |
| 14 |
|
simpl2l |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑥 ⊆ 𝑌 ) |
| 15 |
|
simpr |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) |
| 16 |
15
|
elin1d |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ 𝑥 ) |
| 17 |
|
fnfvima |
⊢ ( ( ◡ 𝐹 Fn 𝑌 ∧ 𝑥 ⊆ 𝑌 ∧ 𝑧 ∈ 𝑥 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ◡ 𝐹 “ 𝑥 ) ) |
| 18 |
13 14 16 17
|
syl3anc |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ◡ 𝐹 “ 𝑥 ) ) |
| 19 |
|
simpl3l |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑦 ⊆ 𝑌 ) |
| 20 |
15
|
elin2d |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ 𝑦 ) |
| 21 |
|
fnfvima |
⊢ ( ( ◡ 𝐹 Fn 𝑌 ∧ 𝑦 ⊆ 𝑌 ∧ 𝑧 ∈ 𝑦 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ◡ 𝐹 “ 𝑦 ) ) |
| 22 |
13 19 20 21
|
syl3anc |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ◡ 𝐹 “ 𝑦 ) ) |
| 23 |
18 22
|
elind |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) |
| 24 |
|
basis2 |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ∧ ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) → ∃ 𝑤 ∈ 𝐽 ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) |
| 25 |
7 8 9 23 24
|
syl22anc |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝐽 ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) |
| 26 |
10
|
adantr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) |
| 27 |
|
inss1 |
⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥 |
| 28 |
|
simp2l |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑥 ⊆ 𝑌 ) |
| 29 |
27 28
|
sstrid |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ 𝑌 ) |
| 30 |
29
|
sselda |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ 𝑌 ) |
| 31 |
30
|
adantr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑧 ∈ 𝑌 ) |
| 32 |
|
f1ocnvfv2 |
⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑧 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 ) |
| 33 |
26 31 32
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 ) |
| 34 |
|
f1ofn |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 Fn 𝑋 ) |
| 35 |
26 34
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐹 Fn 𝑋 ) |
| 36 |
|
simprrr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) |
| 37 |
|
inss1 |
⊢ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ⊆ ( ◡ 𝐹 “ 𝑥 ) |
| 38 |
36 37
|
sstrdi |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ ( ◡ 𝐹 “ 𝑥 ) ) |
| 39 |
|
cnvimass |
⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹 |
| 40 |
|
f1odm |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → dom 𝐹 = 𝑋 ) |
| 41 |
26 40
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → dom 𝐹 = 𝑋 ) |
| 42 |
39 41
|
sseqtrid |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 “ 𝑥 ) ⊆ 𝑋 ) |
| 43 |
38 42
|
sstrd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ 𝑋 ) |
| 44 |
|
simprrl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ) |
| 45 |
|
fnfvima |
⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑤 ⊆ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑤 ) ) |
| 46 |
35 43 44 45
|
syl3anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 “ 𝑤 ) ) |
| 47 |
33 46
|
eqeltrrd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑧 ∈ ( 𝐹 “ 𝑤 ) ) |
| 48 |
|
imassrn |
⊢ ( 𝐹 “ 𝑤 ) ⊆ ran 𝐹 |
| 49 |
26 2
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐹 : 𝑋 –onto→ 𝑌 ) |
| 50 |
|
forn |
⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ran 𝐹 = 𝑌 ) |
| 51 |
49 50
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ran 𝐹 = 𝑌 ) |
| 52 |
48 51
|
sseqtrid |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ 𝑌 ) |
| 53 |
|
f1of1 |
⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –1-1→ 𝑌 ) |
| 54 |
26 53
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 ) |
| 55 |
|
f1imacnv |
⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝑤 ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) = 𝑤 ) |
| 56 |
54 43 55
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) = 𝑤 ) |
| 57 |
|
simprl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ∈ 𝐽 ) |
| 58 |
56 57
|
eqeltrd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 ) |
| 59 |
7
|
adantr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝐽 ∈ TopBases ) |
| 60 |
1
|
elqtop2 |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 ) ) ) |
| 61 |
59 49 60
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑤 ) ⊆ 𝑌 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑤 ) ) ∈ 𝐽 ) ) ) |
| 62 |
52 58 61
|
mpbir2and |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ∈ ( 𝐽 qTop 𝐹 ) ) |
| 63 |
|
fnfun |
⊢ ( 𝐹 Fn 𝑋 → Fun 𝐹 ) |
| 64 |
|
inpreima |
⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) = ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) |
| 65 |
35 63 64
|
3syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) = ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) |
| 66 |
36 65
|
sseqtrrd |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) ) |
| 67 |
35 63
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → Fun 𝐹 ) |
| 68 |
38 39
|
sstrdi |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑤 ⊆ dom 𝐹 ) |
| 69 |
|
funimass3 |
⊢ ( ( Fun 𝐹 ∧ 𝑤 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑤 ) ⊆ ( 𝑥 ∩ 𝑦 ) ↔ 𝑤 ⊆ ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 70 |
67 68 69
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( ( 𝐹 “ 𝑤 ) ⊆ ( 𝑥 ∩ 𝑦 ) ↔ 𝑤 ⊆ ( ◡ 𝐹 “ ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 71 |
66 70
|
mpbird |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 72 |
|
vex |
⊢ 𝑥 ∈ V |
| 73 |
72
|
inex1 |
⊢ ( 𝑥 ∩ 𝑦 ) ∈ V |
| 74 |
73
|
elpw2 |
⊢ ( ( 𝐹 “ 𝑤 ) ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ↔ ( 𝐹 “ 𝑤 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
| 75 |
71 74
|
sylibr |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) |
| 76 |
62 75
|
elind |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → ( 𝐹 “ 𝑤 ) ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
| 77 |
|
elunii |
⊢ ( ( 𝑧 ∈ ( 𝐹 “ 𝑤 ) ∧ ( 𝐹 “ 𝑤 ) ∈ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) → 𝑧 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
| 78 |
47 76 77
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) ∧ ( 𝑤 ∈ 𝐽 ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑤 ∧ 𝑤 ⊆ ( ( ◡ 𝐹 “ 𝑥 ) ∩ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) → 𝑧 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
| 79 |
25 78
|
rexlimddv |
⊢ ( ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
| 80 |
79
|
ex |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) → 𝑧 ∈ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 81 |
80
|
ssrdv |
⊢ ( ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ∧ ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
| 82 |
81
|
3expib |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( ( 𝑥 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ∧ ( 𝑦 ⊆ 𝑌 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 83 |
6 82
|
sylbid |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 84 |
83
|
ralrimivv |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∀ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
| 85 |
|
ovex |
⊢ ( 𝐽 qTop 𝐹 ) ∈ V |
| 86 |
|
isbasisg |
⊢ ( ( 𝐽 qTop 𝐹 ) ∈ V → ( ( 𝐽 qTop 𝐹 ) ∈ TopBases ↔ ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∀ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ) |
| 87 |
85 86
|
ax-mp |
⊢ ( ( 𝐽 qTop 𝐹 ) ∈ TopBases ↔ ∀ 𝑥 ∈ ( 𝐽 qTop 𝐹 ) ∀ 𝑦 ∈ ( 𝐽 qTop 𝐹 ) ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( ( 𝐽 qTop 𝐹 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) |
| 88 |
84 87
|
sylibr |
⊢ ( ( 𝐽 ∈ TopBases ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ TopBases ) |