| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqidd |
|- ( T. -> ( SetCat ` 2o ) = ( SetCat ` 2o ) ) |
| 2 |
|
2oex |
|- 2o e. _V |
| 3 |
2
|
a1i |
|- ( T. -> 2o e. _V ) |
| 4 |
|
elpri |
|- ( x e. { (/) , { (/) } } -> ( x = (/) \/ x = { (/) } ) ) |
| 5 |
|
0ex |
|- (/) e. _V |
| 6 |
|
sneq |
|- ( y = (/) -> { y } = { (/) } ) |
| 7 |
6
|
eqeq2d |
|- ( y = (/) -> ( x = { y } <-> x = { (/) } ) ) |
| 8 |
5 7
|
spcev |
|- ( x = { (/) } -> E. y x = { y } ) |
| 9 |
8
|
orim2i |
|- ( ( x = (/) \/ x = { (/) } ) -> ( x = (/) \/ E. y x = { y } ) ) |
| 10 |
|
mo0sn |
|- ( E* z z e. x <-> ( x = (/) \/ E. y x = { y } ) ) |
| 11 |
10
|
biimpri |
|- ( ( x = (/) \/ E. y x = { y } ) -> E* z z e. x ) |
| 12 |
4 9 11
|
3syl |
|- ( x e. { (/) , { (/) } } -> E* z z e. x ) |
| 13 |
|
df2o2 |
|- 2o = { (/) , { (/) } } |
| 14 |
12 13
|
eleq2s |
|- ( x e. 2o -> E* z z e. x ) |
| 15 |
14
|
rgen |
|- A. x e. 2o E* z z e. x |
| 16 |
15
|
a1i |
|- ( T. -> A. x e. 2o E* z z e. x ) |
| 17 |
1 3 16
|
setcthin |
|- ( T. -> ( SetCat ` 2o ) e. ThinCat ) |
| 18 |
17
|
mptru |
|- ( SetCat ` 2o ) e. ThinCat |