| Step |
Hyp |
Ref |
Expression |
| 1 |
|
f0 |
|- (/) : (/) --> (/) |
| 2 |
|
cnv0 |
|- `' (/) = (/) |
| 3 |
2
|
imaeq1i |
|- ( `' (/) " x ) = ( (/) " x ) |
| 4 |
|
0ima |
|- ( (/) " x ) = (/) |
| 5 |
3 4
|
eqtri |
|- ( `' (/) " x ) = (/) |
| 6 |
|
0ex |
|- (/) e. _V |
| 7 |
6
|
snid |
|- (/) e. { (/) } |
| 8 |
5 7
|
eqeltri |
|- ( `' (/) " x ) e. { (/) } |
| 9 |
8
|
rgenw |
|- A. x e. { (/) } ( `' (/) " x ) e. { (/) } |
| 10 |
|
sn0topon |
|- { (/) } e. ( TopOn ` (/) ) |
| 11 |
|
iscn |
|- ( ( { (/) } e. ( TopOn ` (/) ) /\ { (/) } e. ( TopOn ` (/) ) ) -> ( (/) e. ( { (/) } Cn { (/) } ) <-> ( (/) : (/) --> (/) /\ A. x e. { (/) } ( `' (/) " x ) e. { (/) } ) ) ) |
| 12 |
10 10 11
|
mp2an |
|- ( (/) e. ( { (/) } Cn { (/) } ) <-> ( (/) : (/) --> (/) /\ A. x e. { (/) } ( `' (/) " x ) e. { (/) } ) ) |
| 13 |
1 9 12
|
mpbir2an |
|- (/) e. ( { (/) } Cn { (/) } ) |