Step |
Hyp |
Ref |
Expression |
1 |
|
uniss |
|- ( x C_ ~P A -> U. x C_ U. ~P A ) |
2 |
|
unipw |
|- U. ~P A = A |
3 |
1 2
|
sseqtrdi |
|- ( x C_ ~P A -> U. x C_ A ) |
4 |
|
vuniex |
|- U. x e. _V |
5 |
4
|
elpw |
|- ( U. x e. ~P A <-> U. x C_ A ) |
6 |
3 5
|
sylibr |
|- ( x C_ ~P A -> U. x e. ~P A ) |
7 |
6
|
ax-gen |
|- A. x ( x C_ ~P A -> U. x e. ~P A ) |
8 |
7
|
a1i |
|- ( A e. V -> A. x ( x C_ ~P A -> U. x e. ~P A ) ) |
9 |
|
velpw |
|- ( x e. ~P A <-> x C_ A ) |
10 |
|
velpw |
|- ( y e. ~P A <-> y C_ A ) |
11 |
|
ssinss1 |
|- ( x C_ A -> ( x i^i y ) C_ A ) |
12 |
11
|
a1i |
|- ( y C_ A -> ( x C_ A -> ( x i^i y ) C_ A ) ) |
13 |
|
vex |
|- y e. _V |
14 |
13
|
inex2 |
|- ( x i^i y ) e. _V |
15 |
14
|
elpw |
|- ( ( x i^i y ) e. ~P A <-> ( x i^i y ) C_ A ) |
16 |
12 15
|
syl6ibr |
|- ( y C_ A -> ( x C_ A -> ( x i^i y ) e. ~P A ) ) |
17 |
10 16
|
sylbi |
|- ( y e. ~P A -> ( x C_ A -> ( x i^i y ) e. ~P A ) ) |
18 |
17
|
com12 |
|- ( x C_ A -> ( y e. ~P A -> ( x i^i y ) e. ~P A ) ) |
19 |
9 18
|
sylbi |
|- ( x e. ~P A -> ( y e. ~P A -> ( x i^i y ) e. ~P A ) ) |
20 |
19
|
ralrimiv |
|- ( x e. ~P A -> A. y e. ~P A ( x i^i y ) e. ~P A ) |
21 |
20
|
rgen |
|- A. x e. ~P A A. y e. ~P A ( x i^i y ) e. ~P A |
22 |
21
|
a1i |
|- ( A e. V -> A. x e. ~P A A. y e. ~P A ( x i^i y ) e. ~P A ) |
23 |
|
pwexg |
|- ( A e. V -> ~P A e. _V ) |
24 |
|
istopg |
|- ( ~P A e. _V -> ( ~P A e. Top <-> ( A. x ( x C_ ~P A -> U. x e. ~P A ) /\ A. x e. ~P A A. y e. ~P A ( x i^i y ) e. ~P A ) ) ) |
25 |
23 24
|
syl |
|- ( A e. V -> ( ~P A e. Top <-> ( A. x ( x C_ ~P A -> U. x e. ~P A ) /\ A. x e. ~P A A. y e. ~P A ( x i^i y ) e. ~P A ) ) ) |
26 |
8 22 25
|
mpbir2and |
|- ( A e. V -> ~P A e. Top ) |