Step |
Hyp |
Ref |
Expression |
1 |
|
opnfbas.1 |
|- X = U. J |
2 |
|
ssrab2 |
|- { x e. J | S C_ x } C_ J |
3 |
1
|
eqimss2i |
|- U. J C_ X |
4 |
|
sspwuni |
|- ( J C_ ~P X <-> U. J C_ X ) |
5 |
3 4
|
mpbir |
|- J C_ ~P X |
6 |
2 5
|
sstri |
|- { x e. J | S C_ x } C_ ~P X |
7 |
6
|
a1i |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> { x e. J | S C_ x } C_ ~P X ) |
8 |
1
|
topopn |
|- ( J e. Top -> X e. J ) |
9 |
8
|
anim1i |
|- ( ( J e. Top /\ S C_ X ) -> ( X e. J /\ S C_ X ) ) |
10 |
9
|
3adant3 |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( X e. J /\ S C_ X ) ) |
11 |
|
sseq2 |
|- ( x = X -> ( S C_ x <-> S C_ X ) ) |
12 |
11
|
elrab |
|- ( X e. { x e. J | S C_ x } <-> ( X e. J /\ S C_ X ) ) |
13 |
10 12
|
sylibr |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> X e. { x e. J | S C_ x } ) |
14 |
13
|
ne0d |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> { x e. J | S C_ x } =/= (/) ) |
15 |
|
ss0 |
|- ( S C_ (/) -> S = (/) ) |
16 |
15
|
necon3ai |
|- ( S =/= (/) -> -. S C_ (/) ) |
17 |
16
|
3ad2ant3 |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> -. S C_ (/) ) |
18 |
17
|
intnand |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> -. ( (/) e. J /\ S C_ (/) ) ) |
19 |
|
df-nel |
|- ( (/) e/ { x e. J | S C_ x } <-> -. (/) e. { x e. J | S C_ x } ) |
20 |
|
sseq2 |
|- ( x = (/) -> ( S C_ x <-> S C_ (/) ) ) |
21 |
20
|
elrab |
|- ( (/) e. { x e. J | S C_ x } <-> ( (/) e. J /\ S C_ (/) ) ) |
22 |
21
|
notbii |
|- ( -. (/) e. { x e. J | S C_ x } <-> -. ( (/) e. J /\ S C_ (/) ) ) |
23 |
19 22
|
bitr2i |
|- ( -. ( (/) e. J /\ S C_ (/) ) <-> (/) e/ { x e. J | S C_ x } ) |
24 |
18 23
|
sylib |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> (/) e/ { x e. J | S C_ x } ) |
25 |
|
sseq2 |
|- ( x = r -> ( S C_ x <-> S C_ r ) ) |
26 |
25
|
elrab |
|- ( r e. { x e. J | S C_ x } <-> ( r e. J /\ S C_ r ) ) |
27 |
|
sseq2 |
|- ( x = s -> ( S C_ x <-> S C_ s ) ) |
28 |
27
|
elrab |
|- ( s e. { x e. J | S C_ x } <-> ( s e. J /\ S C_ s ) ) |
29 |
26 28
|
anbi12i |
|- ( ( r e. { x e. J | S C_ x } /\ s e. { x e. J | S C_ x } ) <-> ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) |
30 |
|
simpl |
|- ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> J e. Top ) |
31 |
|
simprll |
|- ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> r e. J ) |
32 |
|
simprrl |
|- ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> s e. J ) |
33 |
|
inopn |
|- ( ( J e. Top /\ r e. J /\ s e. J ) -> ( r i^i s ) e. J ) |
34 |
30 31 32 33
|
syl3anc |
|- ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> ( r i^i s ) e. J ) |
35 |
|
ssin |
|- ( ( S C_ r /\ S C_ s ) <-> S C_ ( r i^i s ) ) |
36 |
35
|
biimpi |
|- ( ( S C_ r /\ S C_ s ) -> S C_ ( r i^i s ) ) |
37 |
36
|
ad2ant2l |
|- ( ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) -> S C_ ( r i^i s ) ) |
38 |
37
|
adantl |
|- ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> S C_ ( r i^i s ) ) |
39 |
34 38
|
jca |
|- ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> ( ( r i^i s ) e. J /\ S C_ ( r i^i s ) ) ) |
40 |
39
|
3ad2antl1 |
|- ( ( ( J e. Top /\ S C_ X /\ S =/= (/) ) /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> ( ( r i^i s ) e. J /\ S C_ ( r i^i s ) ) ) |
41 |
|
sseq2 |
|- ( x = ( r i^i s ) -> ( S C_ x <-> S C_ ( r i^i s ) ) ) |
42 |
41
|
elrab |
|- ( ( r i^i s ) e. { x e. J | S C_ x } <-> ( ( r i^i s ) e. J /\ S C_ ( r i^i s ) ) ) |
43 |
40 42
|
sylibr |
|- ( ( ( J e. Top /\ S C_ X /\ S =/= (/) ) /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> ( r i^i s ) e. { x e. J | S C_ x } ) |
44 |
|
ssid |
|- ( r i^i s ) C_ ( r i^i s ) |
45 |
|
sseq1 |
|- ( t = ( r i^i s ) -> ( t C_ ( r i^i s ) <-> ( r i^i s ) C_ ( r i^i s ) ) ) |
46 |
45
|
rspcev |
|- ( ( ( r i^i s ) e. { x e. J | S C_ x } /\ ( r i^i s ) C_ ( r i^i s ) ) -> E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) |
47 |
43 44 46
|
sylancl |
|- ( ( ( J e. Top /\ S C_ X /\ S =/= (/) ) /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) |
48 |
47
|
ex |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) -> E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) ) |
49 |
29 48
|
syl5bi |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( ( r e. { x e. J | S C_ x } /\ s e. { x e. J | S C_ x } ) -> E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) ) |
50 |
49
|
ralrimivv |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) |
51 |
14 24 50
|
3jca |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( { x e. J | S C_ x } =/= (/) /\ (/) e/ { x e. J | S C_ x } /\ A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) ) |
52 |
|
isfbas2 |
|- ( X e. J -> ( { x e. J | S C_ x } e. ( fBas ` X ) <-> ( { x e. J | S C_ x } C_ ~P X /\ ( { x e. J | S C_ x } =/= (/) /\ (/) e/ { x e. J | S C_ x } /\ A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) ) ) ) |
53 |
8 52
|
syl |
|- ( J e. Top -> ( { x e. J | S C_ x } e. ( fBas ` X ) <-> ( { x e. J | S C_ x } C_ ~P X /\ ( { x e. J | S C_ x } =/= (/) /\ (/) e/ { x e. J | S C_ x } /\ A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) ) ) ) |
54 |
53
|
3ad2ant1 |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( { x e. J | S C_ x } e. ( fBas ` X ) <-> ( { x e. J | S C_ x } C_ ~P X /\ ( { x e. J | S C_ x } =/= (/) /\ (/) e/ { x e. J | S C_ x } /\ A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) ) ) ) |
55 |
7 51 54
|
mpbir2and |
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> { x e. J | S C_ x } e. ( fBas ` X ) ) |