Step |
Hyp |
Ref |
Expression |
1 |
|
prex |
|- { S , { ~P U. S } } e. _V |
2 |
|
vex |
|- x e. _V |
3 |
2
|
elpr |
|- ( x e. { S , { ~P U. S } } <-> ( x = S \/ x = { ~P U. S } ) ) |
4 |
|
vex |
|- y e. _V |
5 |
4
|
elpr |
|- ( y e. { S , { ~P U. S } } <-> ( y = S \/ y = { ~P U. S } ) ) |
6 |
|
eqtr3 |
|- ( ( x = S /\ y = S ) -> x = y ) |
7 |
6
|
orcd |
|- ( ( x = S /\ y = S ) -> ( x = y \/ ( x i^i y ) = (/) ) ) |
8 |
|
ineq12 |
|- ( ( x = { ~P U. S } /\ y = S ) -> ( x i^i y ) = ( { ~P U. S } i^i S ) ) |
9 |
|
incom |
|- ( { ~P U. S } i^i S ) = ( S i^i { ~P U. S } ) |
10 |
|
pwuninel |
|- -. ~P U. S e. S |
11 |
|
disjsn |
|- ( ( S i^i { ~P U. S } ) = (/) <-> -. ~P U. S e. S ) |
12 |
10 11
|
mpbir |
|- ( S i^i { ~P U. S } ) = (/) |
13 |
9 12
|
eqtri |
|- ( { ~P U. S } i^i S ) = (/) |
14 |
8 13
|
eqtrdi |
|- ( ( x = { ~P U. S } /\ y = S ) -> ( x i^i y ) = (/) ) |
15 |
14
|
olcd |
|- ( ( x = { ~P U. S } /\ y = S ) -> ( x = y \/ ( x i^i y ) = (/) ) ) |
16 |
|
ineq12 |
|- ( ( x = S /\ y = { ~P U. S } ) -> ( x i^i y ) = ( S i^i { ~P U. S } ) ) |
17 |
16 12
|
eqtrdi |
|- ( ( x = S /\ y = { ~P U. S } ) -> ( x i^i y ) = (/) ) |
18 |
17
|
olcd |
|- ( ( x = S /\ y = { ~P U. S } ) -> ( x = y \/ ( x i^i y ) = (/) ) ) |
19 |
|
eqtr3 |
|- ( ( x = { ~P U. S } /\ y = { ~P U. S } ) -> x = y ) |
20 |
19
|
orcd |
|- ( ( x = { ~P U. S } /\ y = { ~P U. S } ) -> ( x = y \/ ( x i^i y ) = (/) ) ) |
21 |
7 15 18 20
|
ccase |
|- ( ( ( x = S \/ x = { ~P U. S } ) /\ ( y = S \/ y = { ~P U. S } ) ) -> ( x = y \/ ( x i^i y ) = (/) ) ) |
22 |
3 5 21
|
syl2anb |
|- ( ( x e. { S , { ~P U. S } } /\ y e. { S , { ~P U. S } } ) -> ( x = y \/ ( x i^i y ) = (/) ) ) |
23 |
22
|
rgen2 |
|- A. x e. { S , { ~P U. S } } A. y e. { S , { ~P U. S } } ( x = y \/ ( x i^i y ) = (/) ) |
24 |
|
baspartn |
|- ( ( { S , { ~P U. S } } e. _V /\ A. x e. { S , { ~P U. S } } A. y e. { S , { ~P U. S } } ( x = y \/ ( x i^i y ) = (/) ) ) -> { S , { ~P U. S } } e. TopBases ) |
25 |
1 23 24
|
mp2an |
|- { S , { ~P U. S } } e. TopBases |
26 |
|
tgcl |
|- ( { S , { ~P U. S } } e. TopBases -> ( topGen ` { S , { ~P U. S } } ) e. Top ) |
27 |
25 26
|
mp1i |
|- ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Top ) |
28 |
|
prfi |
|- { S , { ~P U. S } } e. Fin |
29 |
|
pwfi |
|- ( { S , { ~P U. S } } e. Fin <-> ~P { S , { ~P U. S } } e. Fin ) |
30 |
28 29
|
mpbi |
|- ~P { S , { ~P U. S } } e. Fin |
31 |
|
tgdom |
|- ( { S , { ~P U. S } } e. _V -> ( topGen ` { S , { ~P U. S } } ) ~<_ ~P { S , { ~P U. S } } ) |
32 |
1 31
|
ax-mp |
|- ( topGen ` { S , { ~P U. S } } ) ~<_ ~P { S , { ~P U. S } } |
33 |
|
domfi |
|- ( ( ~P { S , { ~P U. S } } e. Fin /\ ( topGen ` { S , { ~P U. S } } ) ~<_ ~P { S , { ~P U. S } } ) -> ( topGen ` { S , { ~P U. S } } ) e. Fin ) |
34 |
30 32 33
|
mp2an |
|- ( topGen ` { S , { ~P U. S } } ) e. Fin |
35 |
34
|
a1i |
|- ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Fin ) |
36 |
27 35
|
elind |
|- ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. ( Top i^i Fin ) ) |
37 |
|
fincmp |
|- ( ( topGen ` { S , { ~P U. S } } ) e. ( Top i^i Fin ) -> ( topGen ` { S , { ~P U. S } } ) e. Comp ) |
38 |
36 37
|
syl |
|- ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Comp ) |