Step |
Hyp |
Ref |
Expression |
1 |
|
opnfbas.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
ssrab2 |
⊢ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝐽 |
3 |
1
|
eqimss2i |
⊢ ∪ 𝐽 ⊆ 𝑋 |
4 |
|
sspwuni |
⊢ ( 𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽 ⊆ 𝑋 ) |
5 |
3 4
|
mpbir |
⊢ 𝐽 ⊆ 𝒫 𝑋 |
6 |
2 5
|
sstri |
⊢ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋 |
7 |
6
|
a1i |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋 ) |
8 |
1
|
topopn |
⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 ) |
9 |
8
|
anim1i |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) ) |
10 |
9
|
3adant3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) ) |
11 |
|
sseq2 |
⊢ ( 𝑥 = 𝑋 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑋 ) ) |
12 |
11
|
elrab |
⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( 𝑋 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋 ) ) |
13 |
10 12
|
sylibr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝑋 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) |
14 |
13
|
ne0d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ) |
15 |
|
ss0 |
⊢ ( 𝑆 ⊆ ∅ → 𝑆 = ∅ ) |
16 |
15
|
necon3ai |
⊢ ( 𝑆 ≠ ∅ → ¬ 𝑆 ⊆ ∅ ) |
17 |
16
|
3ad2ant3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ¬ 𝑆 ⊆ ∅ ) |
18 |
17
|
intnand |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ¬ ( ∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅ ) ) |
19 |
|
df-nel |
⊢ ( ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ¬ ∅ ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) |
20 |
|
sseq2 |
⊢ ( 𝑥 = ∅ → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ ∅ ) ) |
21 |
20
|
elrab |
⊢ ( ∅ ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( ∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅ ) ) |
22 |
21
|
notbii |
⊢ ( ¬ ∅ ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ¬ ( ∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅ ) ) |
23 |
19 22
|
bitr2i |
⊢ ( ¬ ( ∅ ∈ 𝐽 ∧ 𝑆 ⊆ ∅ ) ↔ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) |
24 |
18 23
|
sylib |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) |
25 |
|
sseq2 |
⊢ ( 𝑥 = 𝑟 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑟 ) ) |
26 |
25
|
elrab |
⊢ ( 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ) |
27 |
|
sseq2 |
⊢ ( 𝑥 = 𝑠 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑠 ) ) |
28 |
27
|
elrab |
⊢ ( 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) |
29 |
26 28
|
anbi12i |
⊢ ( ( 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) ↔ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) |
30 |
|
simpl |
⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → 𝐽 ∈ Top ) |
31 |
|
simprll |
⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → 𝑟 ∈ 𝐽 ) |
32 |
|
simprrl |
⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → 𝑠 ∈ 𝐽 ) |
33 |
|
inopn |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑟 ∈ 𝐽 ∧ 𝑠 ∈ 𝐽 ) → ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ) |
34 |
30 31 32 33
|
syl3anc |
⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ) |
35 |
|
ssin |
⊢ ( ( 𝑆 ⊆ 𝑟 ∧ 𝑆 ⊆ 𝑠 ) ↔ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) |
36 |
35
|
biimpi |
⊢ ( ( 𝑆 ⊆ 𝑟 ∧ 𝑆 ⊆ 𝑠 ) → 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) |
37 |
36
|
ad2ant2l |
⊢ ( ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) → 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) |
38 |
37
|
adantl |
⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) |
39 |
34 38
|
jca |
⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ( ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ∧ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) |
40 |
39
|
3ad2antl1 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ( ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ∧ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) |
41 |
|
sseq2 |
⊢ ( 𝑥 = ( 𝑟 ∩ 𝑠 ) → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) |
42 |
41
|
elrab |
⊢ ( ( 𝑟 ∩ 𝑠 ) ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( ( 𝑟 ∩ 𝑠 ) ∈ 𝐽 ∧ 𝑆 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) |
43 |
40 42
|
sylibr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ( 𝑟 ∩ 𝑠 ) ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) |
44 |
|
ssid |
⊢ ( 𝑟 ∩ 𝑠 ) ⊆ ( 𝑟 ∩ 𝑠 ) |
45 |
|
sseq1 |
⊢ ( 𝑡 = ( 𝑟 ∩ 𝑠 ) → ( 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ↔ ( 𝑟 ∩ 𝑠 ) ⊆ ( 𝑟 ∩ 𝑠 ) ) ) |
46 |
45
|
rspcev |
⊢ ( ( ( 𝑟 ∩ 𝑠 ) ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ( 𝑟 ∩ 𝑠 ) ⊆ ( 𝑟 ∩ 𝑠 ) ) → ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) |
47 |
43 44 46
|
sylancl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) ∧ ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) ) → ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) |
48 |
47
|
ex |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( ( 𝑟 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑟 ) ∧ ( 𝑠 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑠 ) ) → ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) |
49 |
29 48
|
syl5bi |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) → ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) |
50 |
49
|
ralrimivv |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) |
51 |
14 24 50
|
3jca |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ∧ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) |
52 |
|
isfbas2 |
⊢ ( 𝑋 ∈ 𝐽 → ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) ↔ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋 ∧ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ∧ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) ) |
53 |
8 52
|
syl |
⊢ ( 𝐽 ∈ Top → ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) ↔ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋 ∧ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ∧ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) ) |
54 |
53
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) ↔ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ⊆ 𝒫 𝑋 ∧ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ∧ ∅ ∉ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ ∀ 𝑟 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∀ 𝑠 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∃ 𝑡 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } 𝑡 ⊆ ( 𝑟 ∩ 𝑠 ) ) ) ) ) |
55 |
7 51 54
|
mpbir2and |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) ) |