Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- U. J = U. J |
2 |
|
eqid |
|- U. K = U. K |
3 |
1 2
|
cnf |
|- ( f e. ( J Cn K ) -> f : U. J --> U. K ) |
4 |
3
|
adantl |
|- ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> f : U. J --> U. K ) |
5 |
|
cnvimass |
|- ( `' f " x ) C_ dom f |
6 |
4
|
fdmd |
|- ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> dom f = U. J ) |
7 |
6
|
adantr |
|- ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> dom f = U. J ) |
8 |
5 7
|
sseqtrid |
|- ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( `' f " x ) C_ U. J ) |
9 |
|
cnvresima |
|- ( `' ( f |` y ) " ( x i^i ( f " y ) ) ) = ( ( `' f " ( x i^i ( f " y ) ) ) i^i y ) |
10 |
4
|
ad2antrr |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> f : U. J --> U. K ) |
11 |
|
ffun |
|- ( f : U. J --> U. K -> Fun f ) |
12 |
|
inpreima |
|- ( Fun f -> ( `' f " ( x i^i ( f " y ) ) ) = ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) ) |
13 |
10 11 12
|
3syl |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( `' f " ( x i^i ( f " y ) ) ) = ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) ) |
14 |
13
|
ineq1d |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( `' f " ( x i^i ( f " y ) ) ) i^i y ) = ( ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) i^i y ) ) |
15 |
|
in32 |
|- ( ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) i^i y ) = ( ( ( `' f " x ) i^i y ) i^i ( `' f " ( f " y ) ) ) |
16 |
|
ssrin |
|- ( ( `' f " x ) C_ dom f -> ( ( `' f " x ) i^i y ) C_ ( dom f i^i y ) ) |
17 |
5 16
|
ax-mp |
|- ( ( `' f " x ) i^i y ) C_ ( dom f i^i y ) |
18 |
|
dminss |
|- ( dom f i^i y ) C_ ( `' f " ( f " y ) ) |
19 |
17 18
|
sstri |
|- ( ( `' f " x ) i^i y ) C_ ( `' f " ( f " y ) ) |
20 |
19
|
a1i |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( `' f " x ) i^i y ) C_ ( `' f " ( f " y ) ) ) |
21 |
|
df-ss |
|- ( ( ( `' f " x ) i^i y ) C_ ( `' f " ( f " y ) ) <-> ( ( ( `' f " x ) i^i y ) i^i ( `' f " ( f " y ) ) ) = ( ( `' f " x ) i^i y ) ) |
22 |
20 21
|
sylib |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( ( `' f " x ) i^i y ) i^i ( `' f " ( f " y ) ) ) = ( ( `' f " x ) i^i y ) ) |
23 |
15 22
|
eqtrid |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( ( `' f " x ) i^i ( `' f " ( f " y ) ) ) i^i y ) = ( ( `' f " x ) i^i y ) ) |
24 |
14 23
|
eqtrd |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( `' f " ( x i^i ( f " y ) ) ) i^i y ) = ( ( `' f " x ) i^i y ) ) |
25 |
9 24
|
eqtrid |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( `' ( f |` y ) " ( x i^i ( f " y ) ) ) = ( ( `' f " x ) i^i y ) ) |
26 |
|
simpr |
|- ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> f e. ( J Cn K ) ) |
27 |
26
|
ad2antrr |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> f e. ( J Cn K ) ) |
28 |
|
elpwi |
|- ( y e. ~P U. J -> y C_ U. J ) |
29 |
28
|
ad2antrl |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> y C_ U. J ) |
30 |
1
|
cnrest |
|- ( ( f e. ( J Cn K ) /\ y C_ U. J ) -> ( f |` y ) e. ( ( J |`t y ) Cn K ) ) |
31 |
27 29 30
|
syl2anc |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( f |` y ) e. ( ( J |`t y ) Cn K ) ) |
32 |
|
simpr |
|- ( ( J e. ran kGen /\ K e. Top ) -> K e. Top ) |
33 |
32
|
ad3antrrr |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> K e. Top ) |
34 |
|
toptopon2 |
|- ( K e. Top <-> K e. ( TopOn ` U. K ) ) |
35 |
33 34
|
sylib |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> K e. ( TopOn ` U. K ) ) |
36 |
|
df-ima |
|- ( f " y ) = ran ( f |` y ) |
37 |
36
|
eqimss2i |
|- ran ( f |` y ) C_ ( f " y ) |
38 |
37
|
a1i |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ran ( f |` y ) C_ ( f " y ) ) |
39 |
|
imassrn |
|- ( f " y ) C_ ran f |
40 |
10
|
frnd |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ran f C_ U. K ) |
41 |
39 40
|
sstrid |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( f " y ) C_ U. K ) |
42 |
|
cnrest2 |
|- ( ( K e. ( TopOn ` U. K ) /\ ran ( f |` y ) C_ ( f " y ) /\ ( f " y ) C_ U. K ) -> ( ( f |` y ) e. ( ( J |`t y ) Cn K ) <-> ( f |` y ) e. ( ( J |`t y ) Cn ( K |`t ( f " y ) ) ) ) ) |
43 |
35 38 41 42
|
syl3anc |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( f |` y ) e. ( ( J |`t y ) Cn K ) <-> ( f |` y ) e. ( ( J |`t y ) Cn ( K |`t ( f " y ) ) ) ) ) |
44 |
31 43
|
mpbid |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( f |` y ) e. ( ( J |`t y ) Cn ( K |`t ( f " y ) ) ) ) |
45 |
|
simplr |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> x e. ( kGen ` K ) ) |
46 |
|
simprr |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( J |`t y ) e. Comp ) |
47 |
|
imacmp |
|- ( ( f e. ( J Cn K ) /\ ( J |`t y ) e. Comp ) -> ( K |`t ( f " y ) ) e. Comp ) |
48 |
27 46 47
|
syl2anc |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( K |`t ( f " y ) ) e. Comp ) |
49 |
|
kgeni |
|- ( ( x e. ( kGen ` K ) /\ ( K |`t ( f " y ) ) e. Comp ) -> ( x i^i ( f " y ) ) e. ( K |`t ( f " y ) ) ) |
50 |
45 48 49
|
syl2anc |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( x i^i ( f " y ) ) e. ( K |`t ( f " y ) ) ) |
51 |
|
cnima |
|- ( ( ( f |` y ) e. ( ( J |`t y ) Cn ( K |`t ( f " y ) ) ) /\ ( x i^i ( f " y ) ) e. ( K |`t ( f " y ) ) ) -> ( `' ( f |` y ) " ( x i^i ( f " y ) ) ) e. ( J |`t y ) ) |
52 |
44 50 51
|
syl2anc |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( `' ( f |` y ) " ( x i^i ( f " y ) ) ) e. ( J |`t y ) ) |
53 |
25 52
|
eqeltrrd |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ ( y e. ~P U. J /\ ( J |`t y ) e. Comp ) ) -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) ) |
54 |
53
|
expr |
|- ( ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) /\ y e. ~P U. J ) -> ( ( J |`t y ) e. Comp -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) ) ) |
55 |
54
|
ralrimiva |
|- ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) ) ) |
56 |
|
kgentop |
|- ( J e. ran kGen -> J e. Top ) |
57 |
56
|
ad3antrrr |
|- ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> J e. Top ) |
58 |
|
toptopon2 |
|- ( J e. Top <-> J e. ( TopOn ` U. J ) ) |
59 |
57 58
|
sylib |
|- ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> J e. ( TopOn ` U. J ) ) |
60 |
|
elkgen |
|- ( J e. ( TopOn ` U. J ) -> ( ( `' f " x ) e. ( kGen ` J ) <-> ( ( `' f " x ) C_ U. J /\ A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) ) ) ) ) |
61 |
59 60
|
syl |
|- ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( ( `' f " x ) e. ( kGen ` J ) <-> ( ( `' f " x ) C_ U. J /\ A. y e. ~P U. J ( ( J |`t y ) e. Comp -> ( ( `' f " x ) i^i y ) e. ( J |`t y ) ) ) ) ) |
62 |
8 55 61
|
mpbir2and |
|- ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( `' f " x ) e. ( kGen ` J ) ) |
63 |
|
kgenidm |
|- ( J e. ran kGen -> ( kGen ` J ) = J ) |
64 |
63
|
ad3antrrr |
|- ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( kGen ` J ) = J ) |
65 |
62 64
|
eleqtrd |
|- ( ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) /\ x e. ( kGen ` K ) ) -> ( `' f " x ) e. J ) |
66 |
65
|
ralrimiva |
|- ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> A. x e. ( kGen ` K ) ( `' f " x ) e. J ) |
67 |
56 58
|
sylib |
|- ( J e. ran kGen -> J e. ( TopOn ` U. J ) ) |
68 |
|
kgentopon |
|- ( K e. ( TopOn ` U. K ) -> ( kGen ` K ) e. ( TopOn ` U. K ) ) |
69 |
34 68
|
sylbi |
|- ( K e. Top -> ( kGen ` K ) e. ( TopOn ` U. K ) ) |
70 |
|
iscn |
|- ( ( J e. ( TopOn ` U. J ) /\ ( kGen ` K ) e. ( TopOn ` U. K ) ) -> ( f e. ( J Cn ( kGen ` K ) ) <-> ( f : U. J --> U. K /\ A. x e. ( kGen ` K ) ( `' f " x ) e. J ) ) ) |
71 |
67 69 70
|
syl2an |
|- ( ( J e. ran kGen /\ K e. Top ) -> ( f e. ( J Cn ( kGen ` K ) ) <-> ( f : U. J --> U. K /\ A. x e. ( kGen ` K ) ( `' f " x ) e. J ) ) ) |
72 |
71
|
adantr |
|- ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> ( f e. ( J Cn ( kGen ` K ) ) <-> ( f : U. J --> U. K /\ A. x e. ( kGen ` K ) ( `' f " x ) e. J ) ) ) |
73 |
4 66 72
|
mpbir2and |
|- ( ( ( J e. ran kGen /\ K e. Top ) /\ f e. ( J Cn K ) ) -> f e. ( J Cn ( kGen ` K ) ) ) |
74 |
73
|
ex |
|- ( ( J e. ran kGen /\ K e. Top ) -> ( f e. ( J Cn K ) -> f e. ( J Cn ( kGen ` K ) ) ) ) |
75 |
74
|
ssrdv |
|- ( ( J e. ran kGen /\ K e. Top ) -> ( J Cn K ) C_ ( J Cn ( kGen ` K ) ) ) |
76 |
69
|
adantl |
|- ( ( J e. ran kGen /\ K e. Top ) -> ( kGen ` K ) e. ( TopOn ` U. K ) ) |
77 |
|
toponcom |
|- ( ( K e. Top /\ ( kGen ` K ) e. ( TopOn ` U. K ) ) -> K e. ( TopOn ` U. ( kGen ` K ) ) ) |
78 |
32 76 77
|
syl2anc |
|- ( ( J e. ran kGen /\ K e. Top ) -> K e. ( TopOn ` U. ( kGen ` K ) ) ) |
79 |
|
kgenss |
|- ( K e. Top -> K C_ ( kGen ` K ) ) |
80 |
79
|
adantl |
|- ( ( J e. ran kGen /\ K e. Top ) -> K C_ ( kGen ` K ) ) |
81 |
|
eqid |
|- U. ( kGen ` K ) = U. ( kGen ` K ) |
82 |
81
|
cnss2 |
|- ( ( K e. ( TopOn ` U. ( kGen ` K ) ) /\ K C_ ( kGen ` K ) ) -> ( J Cn ( kGen ` K ) ) C_ ( J Cn K ) ) |
83 |
78 80 82
|
syl2anc |
|- ( ( J e. ran kGen /\ K e. Top ) -> ( J Cn ( kGen ` K ) ) C_ ( J Cn K ) ) |
84 |
75 83
|
eqssd |
|- ( ( J e. ran kGen /\ K e. Top ) -> ( J Cn K ) = ( J Cn ( kGen ` K ) ) ) |