Step |
Hyp |
Ref |
Expression |
0 |
|
c1stc |
|- 1stc |
1 |
|
vj |
|- j |
2 |
|
ctop |
|- Top |
3 |
|
vx |
|- x |
4 |
1
|
cv |
|- j |
5 |
4
|
cuni |
|- U. j |
6 |
|
vy |
|- y |
7 |
4
|
cpw |
|- ~P j |
8 |
6
|
cv |
|- y |
9 |
|
cdom |
|- ~<_ |
10 |
|
com |
|- _om |
11 |
8 10 9
|
wbr |
|- y ~<_ _om |
12 |
|
vz |
|- z |
13 |
3
|
cv |
|- x |
14 |
12
|
cv |
|- z |
15 |
13 14
|
wcel |
|- x e. z |
16 |
14
|
cpw |
|- ~P z |
17 |
8 16
|
cin |
|- ( y i^i ~P z ) |
18 |
17
|
cuni |
|- U. ( y i^i ~P z ) |
19 |
13 18
|
wcel |
|- x e. U. ( y i^i ~P z ) |
20 |
15 19
|
wi |
|- ( x e. z -> x e. U. ( y i^i ~P z ) ) |
21 |
20 12 4
|
wral |
|- A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) |
22 |
11 21
|
wa |
|- ( y ~<_ _om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) |
23 |
22 6 7
|
wrex |
|- E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) |
24 |
23 3 5
|
wral |
|- A. x e. U. j E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) |
25 |
24 1 2
|
crab |
|- { j e. Top | A. x e. U. j E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) } |
26 |
0 25
|
wceq |
|- 1stc = { j e. Top | A. x e. U. j E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) } |