Step |
Hyp |
Ref |
Expression |
1 |
|
txlm.z |
|- Z = ( ZZ>= ` M ) |
2 |
|
txlm.m |
|- ( ph -> M e. ZZ ) |
3 |
|
txlm.j |
|- ( ph -> J e. ( TopOn ` X ) ) |
4 |
|
txlm.k |
|- ( ph -> K e. ( TopOn ` Y ) ) |
5 |
|
txlm.f |
|- ( ph -> F : Z --> X ) |
6 |
|
txlm.g |
|- ( ph -> G : Z --> Y ) |
7 |
|
txlm.h |
|- H = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) |
8 |
|
r19.27v |
|- ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. u e. J ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
9 |
|
r19.28v |
|- ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
10 |
9
|
ralimi |
|- ( A. u e. J ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
11 |
8 10
|
syl |
|- ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
12 |
|
simprl |
|- ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> w e. ( J tX K ) ) |
13 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
14 |
3 13
|
syl |
|- ( ph -> J e. Top ) |
15 |
|
topontop |
|- ( K e. ( TopOn ` Y ) -> K e. Top ) |
16 |
4 15
|
syl |
|- ( ph -> K e. Top ) |
17 |
|
eqid |
|- ran ( u e. J , v e. K |-> ( u X. v ) ) = ran ( u e. J , v e. K |-> ( u X. v ) ) |
18 |
17
|
txval |
|- ( ( J e. Top /\ K e. Top ) -> ( J tX K ) = ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) ) |
19 |
14 16 18
|
syl2anc |
|- ( ph -> ( J tX K ) = ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) ) |
20 |
19
|
adantr |
|- ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> ( J tX K ) = ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) ) |
21 |
12 20
|
eleqtrd |
|- ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> w e. ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) ) |
22 |
|
simprr |
|- ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> <. R , S >. e. w ) |
23 |
|
tg2 |
|- ( ( w e. ( topGen ` ran ( u e. J , v e. K |-> ( u X. v ) ) ) /\ <. R , S >. e. w ) -> E. t e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. t /\ t C_ w ) ) |
24 |
21 22 23
|
syl2anc |
|- ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> E. t e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. t /\ t C_ w ) ) |
25 |
|
vex |
|- u e. _V |
26 |
|
vex |
|- v e. _V |
27 |
25 26
|
xpex |
|- ( u X. v ) e. _V |
28 |
27
|
rgen2w |
|- A. u e. J A. v e. K ( u X. v ) e. _V |
29 |
|
eqid |
|- ( u e. J , v e. K |-> ( u X. v ) ) = ( u e. J , v e. K |-> ( u X. v ) ) |
30 |
|
eleq2 |
|- ( t = ( u X. v ) -> ( <. R , S >. e. t <-> <. R , S >. e. ( u X. v ) ) ) |
31 |
|
sseq1 |
|- ( t = ( u X. v ) -> ( t C_ w <-> ( u X. v ) C_ w ) ) |
32 |
30 31
|
anbi12d |
|- ( t = ( u X. v ) -> ( ( <. R , S >. e. t /\ t C_ w ) <-> ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) ) |
33 |
29 32
|
rexrnmpo |
|- ( A. u e. J A. v e. K ( u X. v ) e. _V -> ( E. t e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. t /\ t C_ w ) <-> E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) ) |
34 |
28 33
|
ax-mp |
|- ( E. t e. ran ( u e. J , v e. K |-> ( u X. v ) ) ( <. R , S >. e. t /\ t C_ w ) <-> E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) |
35 |
24 34
|
sylib |
|- ( ( ph /\ ( w e. ( J tX K ) /\ <. R , S >. e. w ) ) -> E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) |
36 |
35
|
ex |
|- ( ph -> ( ( w e. ( J tX K ) /\ <. R , S >. e. w ) -> E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) ) |
37 |
|
r19.29 |
|- ( ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. u e. J ( A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) ) |
38 |
|
r19.29 |
|- ( ( A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. v e. K ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) ) |
39 |
|
simprl |
|- ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> <. R , S >. e. ( u X. v ) ) |
40 |
|
opelxp |
|- ( <. R , S >. e. ( u X. v ) <-> ( R e. u /\ S e. v ) ) |
41 |
39 40
|
sylib |
|- ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( R e. u /\ S e. v ) ) |
42 |
|
pm2.27 |
|- ( R e. u -> ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) |
43 |
|
pm2.27 |
|- ( S e. v -> ( ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) |
44 |
42 43
|
im2anan9 |
|- ( ( R e. u /\ S e. v ) -> ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
45 |
41 44
|
syl |
|- ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
46 |
1
|
rexanuz2 |
|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. u /\ ( G ` k ) e. v ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) |
47 |
1
|
uztrn2 |
|- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z ) |
48 |
|
opelxpi |
|- ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> <. ( F ` k ) , ( G ` k ) >. e. ( u X. v ) ) |
49 |
|
fveq2 |
|- ( n = k -> ( F ` n ) = ( F ` k ) ) |
50 |
|
fveq2 |
|- ( n = k -> ( G ` n ) = ( G ` k ) ) |
51 |
49 50
|
opeq12d |
|- ( n = k -> <. ( F ` n ) , ( G ` n ) >. = <. ( F ` k ) , ( G ` k ) >. ) |
52 |
|
opex |
|- <. ( F ` k ) , ( G ` k ) >. e. _V |
53 |
51 7 52
|
fvmpt |
|- ( k e. Z -> ( H ` k ) = <. ( F ` k ) , ( G ` k ) >. ) |
54 |
53
|
eleq1d |
|- ( k e. Z -> ( ( H ` k ) e. ( u X. v ) <-> <. ( F ` k ) , ( G ` k ) >. e. ( u X. v ) ) ) |
55 |
48 54
|
syl5ibr |
|- ( k e. Z -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. ( u X. v ) ) ) |
56 |
55
|
adantl |
|- ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ k e. Z ) -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. ( u X. v ) ) ) |
57 |
|
simplrr |
|- ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ k e. Z ) -> ( u X. v ) C_ w ) |
58 |
57
|
sseld |
|- ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ k e. Z ) -> ( ( H ` k ) e. ( u X. v ) -> ( H ` k ) e. w ) ) |
59 |
56 58
|
syld |
|- ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ k e. Z ) -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. w ) ) |
60 |
47 59
|
sylan2 |
|- ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. w ) ) |
61 |
60
|
anassrs |
|- ( ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> ( H ` k ) e. w ) ) |
62 |
61
|
ralimdva |
|- ( ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) |
63 |
62
|
reximdva |
|- ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. u /\ ( G ` k ) e. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) |
64 |
46 63
|
syl5bir |
|- ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) |
65 |
45 64
|
syld |
|- ( ( ( ( ph /\ u e. J ) /\ v e. K ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) |
66 |
65
|
ex |
|- ( ( ( ph /\ u e. J ) /\ v e. K ) -> ( ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) -> ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
67 |
66
|
impcomd |
|- ( ( ( ph /\ u e. J ) /\ v e. K ) -> ( ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) |
68 |
67
|
rexlimdva |
|- ( ( ph /\ u e. J ) -> ( E. v e. K ( ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) |
69 |
38 68
|
syl5 |
|- ( ( ph /\ u e. J ) -> ( ( A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) |
70 |
69
|
rexlimdva |
|- ( ph -> ( E. u e. J ( A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) |
71 |
37 70
|
syl5 |
|- ( ph -> ( ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) /\ E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) |
72 |
71
|
expcomd |
|- ( ph -> ( E. u e. J E. v e. K ( <. R , S >. e. ( u X. v ) /\ ( u X. v ) C_ w ) -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
73 |
36 72
|
syld |
|- ( ph -> ( ( w e. ( J tX K ) /\ <. R , S >. e. w ) -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
74 |
73
|
expdimp |
|- ( ( ph /\ w e. ( J tX K ) ) -> ( <. R , S >. e. w -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
75 |
74
|
com23 |
|- ( ( ph /\ w e. ( J tX K ) ) -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
76 |
75
|
ralrimdva |
|- ( ph -> ( A. u e. J A. v e. K ( ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
77 |
11 76
|
syl5 |
|- ( ph -> ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
78 |
77
|
adantr |
|- ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) -> A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
79 |
14
|
adantr |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> J e. Top ) |
80 |
16
|
adantr |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> K e. Top ) |
81 |
|
simprr |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> u e. J ) |
82 |
|
toponmax |
|- ( K e. ( TopOn ` Y ) -> Y e. K ) |
83 |
4 82
|
syl |
|- ( ph -> Y e. K ) |
84 |
83
|
adantr |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> Y e. K ) |
85 |
|
txopn |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( u e. J /\ Y e. K ) ) -> ( u X. Y ) e. ( J tX K ) ) |
86 |
79 80 81 84 85
|
syl22anc |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( u X. Y ) e. ( J tX K ) ) |
87 |
|
eleq2 |
|- ( w = ( u X. Y ) -> ( <. R , S >. e. w <-> <. R , S >. e. ( u X. Y ) ) ) |
88 |
|
eleq2 |
|- ( w = ( u X. Y ) -> ( ( H ` k ) e. w <-> ( H ` k ) e. ( u X. Y ) ) ) |
89 |
88
|
rexralbidv |
|- ( w = ( u X. Y ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) ) |
90 |
87 89
|
imbi12d |
|- ( w = ( u X. Y ) -> ( ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) <-> ( <. R , S >. e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) ) ) |
91 |
90
|
rspcv |
|- ( ( u X. Y ) e. ( J tX K ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( <. R , S >. e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) ) ) |
92 |
86 91
|
syl |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( <. R , S >. e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) ) ) |
93 |
|
simprl |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> S e. Y ) |
94 |
|
opelxpi |
|- ( ( R e. u /\ S e. Y ) -> <. R , S >. e. ( u X. Y ) ) |
95 |
93 94
|
sylan2 |
|- ( ( R e. u /\ ( ph /\ ( S e. Y /\ u e. J ) ) ) -> <. R , S >. e. ( u X. Y ) ) |
96 |
95
|
expcom |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( R e. u -> <. R , S >. e. ( u X. Y ) ) ) |
97 |
53
|
eleq1d |
|- ( k e. Z -> ( ( H ` k ) e. ( u X. Y ) <-> <. ( F ` k ) , ( G ` k ) >. e. ( u X. Y ) ) ) |
98 |
|
opelxp1 |
|- ( <. ( F ` k ) , ( G ` k ) >. e. ( u X. Y ) -> ( F ` k ) e. u ) |
99 |
97 98
|
syl6bi |
|- ( k e. Z -> ( ( H ` k ) e. ( u X. Y ) -> ( F ` k ) e. u ) ) |
100 |
47 99
|
syl |
|- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ( H ` k ) e. ( u X. Y ) -> ( F ` k ) e. u ) ) |
101 |
100
|
ralimdva |
|- ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) |
102 |
101
|
reximia |
|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) |
103 |
102
|
a1i |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) |
104 |
96 103
|
imim12d |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( ( <. R , S >. e. ( u X. Y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( u X. Y ) ) -> ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) ) |
105 |
92 104
|
syld |
|- ( ( ph /\ ( S e. Y /\ u e. J ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) ) |
106 |
105
|
anassrs |
|- ( ( ( ph /\ S e. Y ) /\ u e. J ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) ) |
107 |
106
|
ralrimdva |
|- ( ( ph /\ S e. Y ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) ) |
108 |
107
|
adantrl |
|- ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) ) |
109 |
14
|
adantr |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> J e. Top ) |
110 |
16
|
adantr |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> K e. Top ) |
111 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
112 |
3 111
|
syl |
|- ( ph -> X e. J ) |
113 |
112
|
adantr |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> X e. J ) |
114 |
|
simprr |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> v e. K ) |
115 |
|
txopn |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( X e. J /\ v e. K ) ) -> ( X X. v ) e. ( J tX K ) ) |
116 |
109 110 113 114 115
|
syl22anc |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( X X. v ) e. ( J tX K ) ) |
117 |
|
eleq2 |
|- ( w = ( X X. v ) -> ( <. R , S >. e. w <-> <. R , S >. e. ( X X. v ) ) ) |
118 |
|
eleq2 |
|- ( w = ( X X. v ) -> ( ( H ` k ) e. w <-> ( H ` k ) e. ( X X. v ) ) ) |
119 |
118
|
rexralbidv |
|- ( w = ( X X. v ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) ) |
120 |
117 119
|
imbi12d |
|- ( w = ( X X. v ) -> ( ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) <-> ( <. R , S >. e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) ) ) |
121 |
120
|
rspcv |
|- ( ( X X. v ) e. ( J tX K ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( <. R , S >. e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) ) ) |
122 |
116 121
|
syl |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( <. R , S >. e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) ) ) |
123 |
|
opelxpi |
|- ( ( R e. X /\ S e. v ) -> <. R , S >. e. ( X X. v ) ) |
124 |
123
|
ex |
|- ( R e. X -> ( S e. v -> <. R , S >. e. ( X X. v ) ) ) |
125 |
124
|
ad2antrl |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( S e. v -> <. R , S >. e. ( X X. v ) ) ) |
126 |
53
|
eleq1d |
|- ( k e. Z -> ( ( H ` k ) e. ( X X. v ) <-> <. ( F ` k ) , ( G ` k ) >. e. ( X X. v ) ) ) |
127 |
|
opelxp2 |
|- ( <. ( F ` k ) , ( G ` k ) >. e. ( X X. v ) -> ( G ` k ) e. v ) |
128 |
126 127
|
syl6bi |
|- ( k e. Z -> ( ( H ` k ) e. ( X X. v ) -> ( G ` k ) e. v ) ) |
129 |
47 128
|
syl |
|- ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ( H ` k ) e. ( X X. v ) -> ( G ` k ) e. v ) ) |
130 |
129
|
ralimdva |
|- ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) -> A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) |
131 |
130
|
reximia |
|- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) |
132 |
131
|
a1i |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) |
133 |
125 132
|
imim12d |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( ( <. R , S >. e. ( X X. v ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. ( X X. v ) ) -> ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
134 |
122 133
|
syld |
|- ( ( ph /\ ( R e. X /\ v e. K ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
135 |
134
|
anassrs |
|- ( ( ( ph /\ R e. X ) /\ v e. K ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
136 |
135
|
ralrimdva |
|- ( ( ph /\ R e. X ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
137 |
136
|
adantrr |
|- ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) |
138 |
108 137
|
jcad |
|- ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) -> ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) ) |
139 |
78 138
|
impbid |
|- ( ( ph /\ ( R e. X /\ S e. Y ) ) -> ( ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) <-> A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
140 |
139
|
pm5.32da |
|- ( ph -> ( ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) <-> ( ( R e. X /\ S e. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) ) |
141 |
|
opelxp |
|- ( <. R , S >. e. ( X X. Y ) <-> ( R e. X /\ S e. Y ) ) |
142 |
141
|
anbi1i |
|- ( ( <. R , S >. e. ( X X. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) <-> ( ( R e. X /\ S e. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) |
143 |
140 142
|
bitr4di |
|- ( ph -> ( ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) <-> ( <. R , S >. e. ( X X. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) ) |
144 |
|
eqidd |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) ) |
145 |
3 1 2 5 144
|
lmbrf |
|- ( ph -> ( F ( ~~>t ` J ) R <-> ( R e. X /\ A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) ) ) |
146 |
|
eqidd |
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( G ` k ) ) |
147 |
4 1 2 6 146
|
lmbrf |
|- ( ph -> ( G ( ~~>t ` K ) S <-> ( S e. Y /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) ) |
148 |
145 147
|
anbi12d |
|- ( ph -> ( ( F ( ~~>t ` J ) R /\ G ( ~~>t ` K ) S ) <-> ( ( R e. X /\ A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) /\ ( S e. Y /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) ) ) |
149 |
|
an4 |
|- ( ( ( R e. X /\ A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) ) /\ ( S e. Y /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) <-> ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) ) |
150 |
148 149
|
bitrdi |
|- ( ph -> ( ( F ( ~~>t ` J ) R /\ G ( ~~>t ` K ) S ) <-> ( ( R e. X /\ S e. Y ) /\ ( A. u e. J ( R e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. u ) /\ A. v e. K ( S e. v -> E. j e. Z A. k e. ( ZZ>= ` j ) ( G ` k ) e. v ) ) ) ) ) |
151 |
|
txtopon |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) ) |
152 |
3 4 151
|
syl2anc |
|- ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) ) |
153 |
5
|
ffvelrnda |
|- ( ( ph /\ n e. Z ) -> ( F ` n ) e. X ) |
154 |
6
|
ffvelrnda |
|- ( ( ph /\ n e. Z ) -> ( G ` n ) e. Y ) |
155 |
153 154
|
opelxpd |
|- ( ( ph /\ n e. Z ) -> <. ( F ` n ) , ( G ` n ) >. e. ( X X. Y ) ) |
156 |
155 7
|
fmptd |
|- ( ph -> H : Z --> ( X X. Y ) ) |
157 |
|
eqidd |
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( H ` k ) ) |
158 |
152 1 2 156 157
|
lmbrf |
|- ( ph -> ( H ( ~~>t ` ( J tX K ) ) <. R , S >. <-> ( <. R , S >. e. ( X X. Y ) /\ A. w e. ( J tX K ) ( <. R , S >. e. w -> E. j e. Z A. k e. ( ZZ>= ` j ) ( H ` k ) e. w ) ) ) ) |
159 |
143 150 158
|
3bitr4d |
|- ( ph -> ( ( F ( ~~>t ` J ) R /\ G ( ~~>t ` K ) S ) <-> H ( ~~>t ` ( J tX K ) ) <. R , S >. ) ) |