Step |
Hyp |
Ref |
Expression |
1 |
|
iscn |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( ( _I |` X ) e. ( J Cn K ) <-> ( ( _I |` X ) : X --> X /\ A. x e. K ( `' ( _I |` X ) " x ) e. J ) ) ) |
2 |
|
f1oi |
|- ( _I |` X ) : X -1-1-onto-> X |
3 |
|
f1of |
|- ( ( _I |` X ) : X -1-1-onto-> X -> ( _I |` X ) : X --> X ) |
4 |
2 3
|
ax-mp |
|- ( _I |` X ) : X --> X |
5 |
4
|
biantrur |
|- ( A. x e. K ( `' ( _I |` X ) " x ) e. J <-> ( ( _I |` X ) : X --> X /\ A. x e. K ( `' ( _I |` X ) " x ) e. J ) ) |
6 |
1 5
|
bitr4di |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( ( _I |` X ) e. ( J Cn K ) <-> A. x e. K ( `' ( _I |` X ) " x ) e. J ) ) |
7 |
|
cnvresid |
|- `' ( _I |` X ) = ( _I |` X ) |
8 |
7
|
imaeq1i |
|- ( `' ( _I |` X ) " x ) = ( ( _I |` X ) " x ) |
9 |
|
elssuni |
|- ( x e. K -> x C_ U. K ) |
10 |
9
|
adantl |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> x C_ U. K ) |
11 |
|
toponuni |
|- ( K e. ( TopOn ` X ) -> X = U. K ) |
12 |
11
|
ad2antlr |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> X = U. K ) |
13 |
10 12
|
sseqtrrd |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> x C_ X ) |
14 |
|
resiima |
|- ( x C_ X -> ( ( _I |` X ) " x ) = x ) |
15 |
13 14
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> ( ( _I |` X ) " x ) = x ) |
16 |
8 15
|
eqtrid |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> ( `' ( _I |` X ) " x ) = x ) |
17 |
16
|
eleq1d |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ x e. K ) -> ( ( `' ( _I |` X ) " x ) e. J <-> x e. J ) ) |
18 |
17
|
ralbidva |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( A. x e. K ( `' ( _I |` X ) " x ) e. J <-> A. x e. K x e. J ) ) |
19 |
|
dfss3 |
|- ( K C_ J <-> A. x e. K x e. J ) |
20 |
18 19
|
bitr4di |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( A. x e. K ( `' ( _I |` X ) " x ) e. J <-> K C_ J ) ) |
21 |
6 20
|
bitrd |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( ( _I |` X ) e. ( J Cn K ) <-> K C_ J ) ) |