Step |
Hyp |
Ref |
Expression |
1 |
|
f2ndres |
|- ( 2nd |` ( X X. Y ) ) : ( X X. Y ) --> Y |
2 |
1
|
a1i |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( 2nd |` ( X X. Y ) ) : ( X X. Y ) --> Y ) |
3 |
|
ffn |
|- ( ( 2nd |` ( X X. Y ) ) : ( X X. Y ) --> Y -> ( 2nd |` ( X X. Y ) ) Fn ( X X. Y ) ) |
4 |
|
elpreima |
|- ( ( 2nd |` ( X X. Y ) ) Fn ( X X. Y ) -> ( z e. ( `' ( 2nd |` ( X X. Y ) ) " w ) <-> ( z e. ( X X. Y ) /\ ( ( 2nd |` ( X X. Y ) ) ` z ) e. w ) ) ) |
5 |
1 3 4
|
mp2b |
|- ( z e. ( `' ( 2nd |` ( X X. Y ) ) " w ) <-> ( z e. ( X X. Y ) /\ ( ( 2nd |` ( X X. Y ) ) ` z ) e. w ) ) |
6 |
|
fvres |
|- ( z e. ( X X. Y ) -> ( ( 2nd |` ( X X. Y ) ) ` z ) = ( 2nd ` z ) ) |
7 |
6
|
eleq1d |
|- ( z e. ( X X. Y ) -> ( ( ( 2nd |` ( X X. Y ) ) ` z ) e. w <-> ( 2nd ` z ) e. w ) ) |
8 |
|
1st2nd2 |
|- ( z e. ( X X. Y ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. ) |
9 |
|
xp1st |
|- ( z e. ( X X. Y ) -> ( 1st ` z ) e. X ) |
10 |
|
elxp6 |
|- ( z e. ( X X. w ) <-> ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( ( 1st ` z ) e. X /\ ( 2nd ` z ) e. w ) ) ) |
11 |
|
anass |
|- ( ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. X ) /\ ( 2nd ` z ) e. w ) <-> ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( ( 1st ` z ) e. X /\ ( 2nd ` z ) e. w ) ) ) |
12 |
10 11
|
bitr4i |
|- ( z e. ( X X. w ) <-> ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. X ) /\ ( 2nd ` z ) e. w ) ) |
13 |
12
|
baib |
|- ( ( z = <. ( 1st ` z ) , ( 2nd ` z ) >. /\ ( 1st ` z ) e. X ) -> ( z e. ( X X. w ) <-> ( 2nd ` z ) e. w ) ) |
14 |
8 9 13
|
syl2anc |
|- ( z e. ( X X. Y ) -> ( z e. ( X X. w ) <-> ( 2nd ` z ) e. w ) ) |
15 |
7 14
|
bitr4d |
|- ( z e. ( X X. Y ) -> ( ( ( 2nd |` ( X X. Y ) ) ` z ) e. w <-> z e. ( X X. w ) ) ) |
16 |
15
|
pm5.32i |
|- ( ( z e. ( X X. Y ) /\ ( ( 2nd |` ( X X. Y ) ) ` z ) e. w ) <-> ( z e. ( X X. Y ) /\ z e. ( X X. w ) ) ) |
17 |
5 16
|
bitri |
|- ( z e. ( `' ( 2nd |` ( X X. Y ) ) " w ) <-> ( z e. ( X X. Y ) /\ z e. ( X X. w ) ) ) |
18 |
|
toponss |
|- ( ( S e. ( TopOn ` Y ) /\ w e. S ) -> w C_ Y ) |
19 |
18
|
adantll |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. S ) -> w C_ Y ) |
20 |
|
xpss2 |
|- ( w C_ Y -> ( X X. w ) C_ ( X X. Y ) ) |
21 |
19 20
|
syl |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. S ) -> ( X X. w ) C_ ( X X. Y ) ) |
22 |
21
|
sseld |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. S ) -> ( z e. ( X X. w ) -> z e. ( X X. Y ) ) ) |
23 |
22
|
pm4.71rd |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. S ) -> ( z e. ( X X. w ) <-> ( z e. ( X X. Y ) /\ z e. ( X X. w ) ) ) ) |
24 |
17 23
|
bitr4id |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. S ) -> ( z e. ( `' ( 2nd |` ( X X. Y ) ) " w ) <-> z e. ( X X. w ) ) ) |
25 |
24
|
eqrdv |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. S ) -> ( `' ( 2nd |` ( X X. Y ) ) " w ) = ( X X. w ) ) |
26 |
|
toponmax |
|- ( R e. ( TopOn ` X ) -> X e. R ) |
27 |
|
txopn |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ ( X e. R /\ w e. S ) ) -> ( X X. w ) e. ( R tX S ) ) |
28 |
27
|
expr |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ X e. R ) -> ( w e. S -> ( X X. w ) e. ( R tX S ) ) ) |
29 |
26 28
|
mpidan |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( w e. S -> ( X X. w ) e. ( R tX S ) ) ) |
30 |
29
|
imp |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. S ) -> ( X X. w ) e. ( R tX S ) ) |
31 |
25 30
|
eqeltrd |
|- ( ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) /\ w e. S ) -> ( `' ( 2nd |` ( X X. Y ) ) " w ) e. ( R tX S ) ) |
32 |
31
|
ralrimiva |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> A. w e. S ( `' ( 2nd |` ( X X. Y ) ) " w ) e. ( R tX S ) ) |
33 |
|
txtopon |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) e. ( TopOn ` ( X X. Y ) ) ) |
34 |
|
iscn |
|- ( ( ( R tX S ) e. ( TopOn ` ( X X. Y ) ) /\ S e. ( TopOn ` Y ) ) -> ( ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) <-> ( ( 2nd |` ( X X. Y ) ) : ( X X. Y ) --> Y /\ A. w e. S ( `' ( 2nd |` ( X X. Y ) ) " w ) e. ( R tX S ) ) ) ) |
35 |
33 34
|
sylancom |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) <-> ( ( 2nd |` ( X X. Y ) ) : ( X X. Y ) --> Y /\ A. w e. S ( `' ( 2nd |` ( X X. Y ) ) " w ) e. ( R tX S ) ) ) ) |
36 |
2 32 35
|
mpbir2and |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) ) |