Step |
Hyp |
Ref |
Expression |
1 |
|
kelac2.s |
|- ( ( ph /\ x e. I ) -> S e. V ) |
2 |
|
kelac2.z |
|- ( ( ph /\ x e. I ) -> S =/= (/) ) |
3 |
|
kelac2.k |
|- ( ph -> ( Xt_ ` ( x e. I |-> ( topGen ` { S , { ~P U. S } } ) ) ) e. Comp ) |
4 |
|
kelac2lem |
|- ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Comp ) |
5 |
|
cmptop |
|- ( ( topGen ` { S , { ~P U. S } } ) e. Comp -> ( topGen ` { S , { ~P U. S } } ) e. Top ) |
6 |
1 4 5
|
3syl |
|- ( ( ph /\ x e. I ) -> ( topGen ` { S , { ~P U. S } } ) e. Top ) |
7 |
|
uncom |
|- ( S u. { ~P U. S } ) = ( { ~P U. S } u. S ) |
8 |
7
|
difeq1i |
|- ( ( S u. { ~P U. S } ) \ S ) = ( ( { ~P U. S } u. S ) \ S ) |
9 |
|
difun2 |
|- ( ( { ~P U. S } u. S ) \ S ) = ( { ~P U. S } \ S ) |
10 |
8 9
|
eqtri |
|- ( ( S u. { ~P U. S } ) \ S ) = ( { ~P U. S } \ S ) |
11 |
|
snex |
|- { ~P U. S } e. _V |
12 |
|
uniprg |
|- ( ( S e. V /\ { ~P U. S } e. _V ) -> U. { S , { ~P U. S } } = ( S u. { ~P U. S } ) ) |
13 |
1 11 12
|
sylancl |
|- ( ( ph /\ x e. I ) -> U. { S , { ~P U. S } } = ( S u. { ~P U. S } ) ) |
14 |
13
|
difeq1d |
|- ( ( ph /\ x e. I ) -> ( U. { S , { ~P U. S } } \ S ) = ( ( S u. { ~P U. S } ) \ S ) ) |
15 |
|
incom |
|- ( { ~P U. S } i^i S ) = ( S i^i { ~P U. S } ) |
16 |
|
pwuninel |
|- -. ~P U. S e. S |
17 |
16
|
a1i |
|- ( ( ph /\ x e. I ) -> -. ~P U. S e. S ) |
18 |
|
disjsn |
|- ( ( S i^i { ~P U. S } ) = (/) <-> -. ~P U. S e. S ) |
19 |
17 18
|
sylibr |
|- ( ( ph /\ x e. I ) -> ( S i^i { ~P U. S } ) = (/) ) |
20 |
15 19
|
syl5eq |
|- ( ( ph /\ x e. I ) -> ( { ~P U. S } i^i S ) = (/) ) |
21 |
|
disj3 |
|- ( ( { ~P U. S } i^i S ) = (/) <-> { ~P U. S } = ( { ~P U. S } \ S ) ) |
22 |
20 21
|
sylib |
|- ( ( ph /\ x e. I ) -> { ~P U. S } = ( { ~P U. S } \ S ) ) |
23 |
10 14 22
|
3eqtr4a |
|- ( ( ph /\ x e. I ) -> ( U. { S , { ~P U. S } } \ S ) = { ~P U. S } ) |
24 |
|
prex |
|- { S , { ~P U. S } } e. _V |
25 |
|
bastg |
|- ( { S , { ~P U. S } } e. _V -> { S , { ~P U. S } } C_ ( topGen ` { S , { ~P U. S } } ) ) |
26 |
24 25
|
mp1i |
|- ( ( ph /\ x e. I ) -> { S , { ~P U. S } } C_ ( topGen ` { S , { ~P U. S } } ) ) |
27 |
11
|
prid2 |
|- { ~P U. S } e. { S , { ~P U. S } } |
28 |
27
|
a1i |
|- ( ( ph /\ x e. I ) -> { ~P U. S } e. { S , { ~P U. S } } ) |
29 |
26 28
|
sseldd |
|- ( ( ph /\ x e. I ) -> { ~P U. S } e. ( topGen ` { S , { ~P U. S } } ) ) |
30 |
23 29
|
eqeltrd |
|- ( ( ph /\ x e. I ) -> ( U. { S , { ~P U. S } } \ S ) e. ( topGen ` { S , { ~P U. S } } ) ) |
31 |
|
prid1g |
|- ( S e. V -> S e. { S , { ~P U. S } } ) |
32 |
|
elssuni |
|- ( S e. { S , { ~P U. S } } -> S C_ U. { S , { ~P U. S } } ) |
33 |
1 31 32
|
3syl |
|- ( ( ph /\ x e. I ) -> S C_ U. { S , { ~P U. S } } ) |
34 |
|
unitg |
|- ( { S , { ~P U. S } } e. _V -> U. ( topGen ` { S , { ~P U. S } } ) = U. { S , { ~P U. S } } ) |
35 |
24 34
|
ax-mp |
|- U. ( topGen ` { S , { ~P U. S } } ) = U. { S , { ~P U. S } } |
36 |
35
|
eqcomi |
|- U. { S , { ~P U. S } } = U. ( topGen ` { S , { ~P U. S } } ) |
37 |
36
|
iscld2 |
|- ( ( ( topGen ` { S , { ~P U. S } } ) e. Top /\ S C_ U. { S , { ~P U. S } } ) -> ( S e. ( Clsd ` ( topGen ` { S , { ~P U. S } } ) ) <-> ( U. { S , { ~P U. S } } \ S ) e. ( topGen ` { S , { ~P U. S } } ) ) ) |
38 |
6 33 37
|
syl2anc |
|- ( ( ph /\ x e. I ) -> ( S e. ( Clsd ` ( topGen ` { S , { ~P U. S } } ) ) <-> ( U. { S , { ~P U. S } } \ S ) e. ( topGen ` { S , { ~P U. S } } ) ) ) |
39 |
30 38
|
mpbird |
|- ( ( ph /\ x e. I ) -> S e. ( Clsd ` ( topGen ` { S , { ~P U. S } } ) ) ) |
40 |
|
f1oi |
|- ( _I |` S ) : S -1-1-onto-> S |
41 |
40
|
a1i |
|- ( ( ph /\ x e. I ) -> ( _I |` S ) : S -1-1-onto-> S ) |
42 |
|
elssuni |
|- ( { ~P U. S } e. { S , { ~P U. S } } -> { ~P U. S } C_ U. { S , { ~P U. S } } ) |
43 |
27 42
|
mp1i |
|- ( ( ph /\ x e. I ) -> { ~P U. S } C_ U. { S , { ~P U. S } } ) |
44 |
|
uniexg |
|- ( S e. V -> U. S e. _V ) |
45 |
|
pwexg |
|- ( U. S e. _V -> ~P U. S e. _V ) |
46 |
|
snidg |
|- ( ~P U. S e. _V -> ~P U. S e. { ~P U. S } ) |
47 |
1 44 45 46
|
4syl |
|- ( ( ph /\ x e. I ) -> ~P U. S e. { ~P U. S } ) |
48 |
43 47
|
sseldd |
|- ( ( ph /\ x e. I ) -> ~P U. S e. U. { S , { ~P U. S } } ) |
49 |
48 35
|
eleqtrrdi |
|- ( ( ph /\ x e. I ) -> ~P U. S e. U. ( topGen ` { S , { ~P U. S } } ) ) |
50 |
2 6 39 41 49 3
|
kelac1 |
|- ( ph -> X_ x e. I S =/= (/) ) |