Step |
Hyp |
Ref |
Expression |
1 |
|
flfcnp2.j |
|- ( ph -> J e. ( TopOn ` X ) ) |
2 |
|
flfcnp2.k |
|- ( ph -> K e. ( TopOn ` Y ) ) |
3 |
|
flfcnp2.l |
|- ( ph -> L e. ( Fil ` Z ) ) |
4 |
|
flfcnp2.a |
|- ( ( ph /\ x e. Z ) -> A e. X ) |
5 |
|
flfcnp2.b |
|- ( ( ph /\ x e. Z ) -> B e. Y ) |
6 |
|
flfcnp2.r |
|- ( ph -> R e. ( ( J fLimf L ) ` ( x e. Z |-> A ) ) ) |
7 |
|
flfcnp2.s |
|- ( ph -> S e. ( ( K fLimf L ) ` ( x e. Z |-> B ) ) ) |
8 |
|
flfcnp2.o |
|- ( ph -> O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) ) |
9 |
|
df-ov |
|- ( R O S ) = ( O ` <. R , S >. ) |
10 |
|
txtopon |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) ) |
11 |
1 2 10
|
syl2anc |
|- ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) ) |
12 |
4 5
|
opelxpd |
|- ( ( ph /\ x e. Z ) -> <. A , B >. e. ( X X. Y ) ) |
13 |
12
|
fmpttd |
|- ( ph -> ( x e. Z |-> <. A , B >. ) : Z --> ( X X. Y ) ) |
14 |
4
|
fmpttd |
|- ( ph -> ( x e. Z |-> A ) : Z --> X ) |
15 |
5
|
fmpttd |
|- ( ph -> ( x e. Z |-> B ) : Z --> Y ) |
16 |
|
nfcv |
|- F/_ y <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. |
17 |
|
nffvmpt1 |
|- F/_ x ( ( x e. Z |-> A ) ` y ) |
18 |
|
nffvmpt1 |
|- F/_ x ( ( x e. Z |-> B ) ` y ) |
19 |
17 18
|
nfop |
|- F/_ x <. ( ( x e. Z |-> A ) ` y ) , ( ( x e. Z |-> B ) ` y ) >. |
20 |
|
fveq2 |
|- ( x = y -> ( ( x e. Z |-> A ) ` x ) = ( ( x e. Z |-> A ) ` y ) ) |
21 |
|
fveq2 |
|- ( x = y -> ( ( x e. Z |-> B ) ` x ) = ( ( x e. Z |-> B ) ` y ) ) |
22 |
20 21
|
opeq12d |
|- ( x = y -> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. = <. ( ( x e. Z |-> A ) ` y ) , ( ( x e. Z |-> B ) ` y ) >. ) |
23 |
16 19 22
|
cbvmpt |
|- ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) = ( y e. Z |-> <. ( ( x e. Z |-> A ) ` y ) , ( ( x e. Z |-> B ) ` y ) >. ) |
24 |
1 2 3 14 15 23
|
txflf |
|- ( ph -> ( <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) ) <-> ( R e. ( ( J fLimf L ) ` ( x e. Z |-> A ) ) /\ S e. ( ( K fLimf L ) ` ( x e. Z |-> B ) ) ) ) ) |
25 |
6 7 24
|
mpbir2and |
|- ( ph -> <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) ) ) |
26 |
|
simpr |
|- ( ( ph /\ x e. Z ) -> x e. Z ) |
27 |
|
eqid |
|- ( x e. Z |-> A ) = ( x e. Z |-> A ) |
28 |
27
|
fvmpt2 |
|- ( ( x e. Z /\ A e. X ) -> ( ( x e. Z |-> A ) ` x ) = A ) |
29 |
26 4 28
|
syl2anc |
|- ( ( ph /\ x e. Z ) -> ( ( x e. Z |-> A ) ` x ) = A ) |
30 |
|
eqid |
|- ( x e. Z |-> B ) = ( x e. Z |-> B ) |
31 |
30
|
fvmpt2 |
|- ( ( x e. Z /\ B e. Y ) -> ( ( x e. Z |-> B ) ` x ) = B ) |
32 |
26 5 31
|
syl2anc |
|- ( ( ph /\ x e. Z ) -> ( ( x e. Z |-> B ) ` x ) = B ) |
33 |
29 32
|
opeq12d |
|- ( ( ph /\ x e. Z ) -> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. = <. A , B >. ) |
34 |
33
|
mpteq2dva |
|- ( ph -> ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) = ( x e. Z |-> <. A , B >. ) ) |
35 |
34
|
fveq2d |
|- ( ph -> ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) ) = ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. A , B >. ) ) ) |
36 |
25 35
|
eleqtrd |
|- ( ph -> <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. A , B >. ) ) ) |
37 |
|
flfcnp |
|- ( ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( Fil ` Z ) /\ ( x e. Z |-> <. A , B >. ) : Z --> ( X X. Y ) ) /\ ( <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. A , B >. ) ) /\ O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) ) ) -> ( O ` <. R , S >. ) e. ( ( N fLimf L ) ` ( O o. ( x e. Z |-> <. A , B >. ) ) ) ) |
38 |
11 3 13 36 8 37
|
syl32anc |
|- ( ph -> ( O ` <. R , S >. ) e. ( ( N fLimf L ) ` ( O o. ( x e. Z |-> <. A , B >. ) ) ) ) |
39 |
|
eqidd |
|- ( ph -> ( x e. Z |-> <. A , B >. ) = ( x e. Z |-> <. A , B >. ) ) |
40 |
|
cnptop2 |
|- ( O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) -> N e. Top ) |
41 |
8 40
|
syl |
|- ( ph -> N e. Top ) |
42 |
|
toptopon2 |
|- ( N e. Top <-> N e. ( TopOn ` U. N ) ) |
43 |
41 42
|
sylib |
|- ( ph -> N e. ( TopOn ` U. N ) ) |
44 |
|
cnpf2 |
|- ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ N e. ( TopOn ` U. N ) /\ O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) ) -> O : ( X X. Y ) --> U. N ) |
45 |
11 43 8 44
|
syl3anc |
|- ( ph -> O : ( X X. Y ) --> U. N ) |
46 |
45
|
feqmptd |
|- ( ph -> O = ( y e. ( X X. Y ) |-> ( O ` y ) ) ) |
47 |
|
fveq2 |
|- ( y = <. A , B >. -> ( O ` y ) = ( O ` <. A , B >. ) ) |
48 |
|
df-ov |
|- ( A O B ) = ( O ` <. A , B >. ) |
49 |
47 48
|
eqtr4di |
|- ( y = <. A , B >. -> ( O ` y ) = ( A O B ) ) |
50 |
12 39 46 49
|
fmptco |
|- ( ph -> ( O o. ( x e. Z |-> <. A , B >. ) ) = ( x e. Z |-> ( A O B ) ) ) |
51 |
50
|
fveq2d |
|- ( ph -> ( ( N fLimf L ) ` ( O o. ( x e. Z |-> <. A , B >. ) ) ) = ( ( N fLimf L ) ` ( x e. Z |-> ( A O B ) ) ) ) |
52 |
38 51
|
eleqtrd |
|- ( ph -> ( O ` <. R , S >. ) e. ( ( N fLimf L ) ` ( x e. Z |-> ( A O B ) ) ) ) |
53 |
9 52
|
eqeltrid |
|- ( ph -> ( R O S ) e. ( ( N fLimf L ) ` ( x e. Z |-> ( A O B ) ) ) ) |