Metamath Proof Explorer


Theorem txcnp

Description: If two functions are continuous at D , then the ordered pair of them is continuous at D into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses txcnp.4
|- ( ph -> J e. ( TopOn ` X ) )
txcnp.5
|- ( ph -> K e. ( TopOn ` Y ) )
txcnp.6
|- ( ph -> L e. ( TopOn ` Z ) )
txcnp.7
|- ( ph -> D e. X )
txcnp.8
|- ( ph -> ( x e. X |-> A ) e. ( ( J CnP K ) ` D ) )
txcnp.9
|- ( ph -> ( x e. X |-> B ) e. ( ( J CnP L ) ` D ) )
Assertion txcnp
|- ( ph -> ( x e. X |-> <. A , B >. ) e. ( ( J CnP ( K tX L ) ) ` D ) )

Proof

Step Hyp Ref Expression
1 txcnp.4
 |-  ( ph -> J e. ( TopOn ` X ) )
2 txcnp.5
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 txcnp.6
 |-  ( ph -> L e. ( TopOn ` Z ) )
4 txcnp.7
 |-  ( ph -> D e. X )
5 txcnp.8
 |-  ( ph -> ( x e. X |-> A ) e. ( ( J CnP K ) ` D ) )
6 txcnp.9
 |-  ( ph -> ( x e. X |-> B ) e. ( ( J CnP L ) ` D ) )
7 cnpf2
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ ( x e. X |-> A ) e. ( ( J CnP K ) ` D ) ) -> ( x e. X |-> A ) : X --> Y )
8 1 2 5 7 syl3anc
 |-  ( ph -> ( x e. X |-> A ) : X --> Y )
9 8 fvmptelrn
 |-  ( ( ph /\ x e. X ) -> A e. Y )
10 cnpf2
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( TopOn ` Z ) /\ ( x e. X |-> B ) e. ( ( J CnP L ) ` D ) ) -> ( x e. X |-> B ) : X --> Z )
11 1 3 6 10 syl3anc
 |-  ( ph -> ( x e. X |-> B ) : X --> Z )
12 11 fvmptelrn
 |-  ( ( ph /\ x e. X ) -> B e. Z )
13 9 12 opelxpd
 |-  ( ( ph /\ x e. X ) -> <. A , B >. e. ( Y X. Z ) )
14 13 fmpttd
 |-  ( ph -> ( x e. X |-> <. A , B >. ) : X --> ( Y X. Z ) )
15 simpr
 |-  ( ( ph /\ x e. X ) -> x e. X )
16 opex
 |-  <. A , B >. e. _V
17 eqid
 |-  ( x e. X |-> <. A , B >. ) = ( x e. X |-> <. A , B >. )
18 17 fvmpt2
 |-  ( ( x e. X /\ <. A , B >. e. _V ) -> ( ( x e. X |-> <. A , B >. ) ` x ) = <. A , B >. )
19 15 16 18 sylancl
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> <. A , B >. ) ` x ) = <. A , B >. )
20 eqid
 |-  ( x e. X |-> A ) = ( x e. X |-> A )
21 20 fvmpt2
 |-  ( ( x e. X /\ A e. Y ) -> ( ( x e. X |-> A ) ` x ) = A )
22 15 9 21 syl2anc
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> A ) ` x ) = A )
23 eqid
 |-  ( x e. X |-> B ) = ( x e. X |-> B )
24 23 fvmpt2
 |-  ( ( x e. X /\ B e. Z ) -> ( ( x e. X |-> B ) ` x ) = B )
25 15 12 24 syl2anc
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> B ) ` x ) = B )
26 22 25 opeq12d
 |-  ( ( ph /\ x e. X ) -> <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. = <. A , B >. )
27 19 26 eqtr4d
 |-  ( ( ph /\ x e. X ) -> ( ( x e. X |-> <. A , B >. ) ` x ) = <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. )
28 27 ralrimiva
 |-  ( ph -> A. x e. X ( ( x e. X |-> <. A , B >. ) ` x ) = <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. )
29 nffvmpt1
 |-  F/_ x ( ( x e. X |-> <. A , B >. ) ` D )
30 nffvmpt1
 |-  F/_ x ( ( x e. X |-> A ) ` D )
31 nffvmpt1
 |-  F/_ x ( ( x e. X |-> B ) ` D )
32 30 31 nfop
 |-  F/_ x <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >.
33 29 32 nfeq
 |-  F/ x ( ( x e. X |-> <. A , B >. ) ` D ) = <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >.
34 fveq2
 |-  ( x = D -> ( ( x e. X |-> <. A , B >. ) ` x ) = ( ( x e. X |-> <. A , B >. ) ` D ) )
35 fveq2
 |-  ( x = D -> ( ( x e. X |-> A ) ` x ) = ( ( x e. X |-> A ) ` D ) )
36 fveq2
 |-  ( x = D -> ( ( x e. X |-> B ) ` x ) = ( ( x e. X |-> B ) ` D ) )
37 35 36 opeq12d
 |-  ( x = D -> <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. = <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >. )
38 34 37 eqeq12d
 |-  ( x = D -> ( ( ( x e. X |-> <. A , B >. ) ` x ) = <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. <-> ( ( x e. X |-> <. A , B >. ) ` D ) = <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >. ) )
39 33 38 rspc
 |-  ( D e. X -> ( A. x e. X ( ( x e. X |-> <. A , B >. ) ` x ) = <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. -> ( ( x e. X |-> <. A , B >. ) ` D ) = <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >. ) )
40 4 28 39 sylc
 |-  ( ph -> ( ( x e. X |-> <. A , B >. ) ` D ) = <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >. )
41 40 eleq1d
 |-  ( ph -> ( ( ( x e. X |-> <. A , B >. ) ` D ) e. ( v X. w ) <-> <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >. e. ( v X. w ) ) )
42 41 adantr
 |-  ( ( ph /\ ( v e. K /\ w e. L ) ) -> ( ( ( x e. X |-> <. A , B >. ) ` D ) e. ( v X. w ) <-> <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >. e. ( v X. w ) ) )
43 5 ad2antrr
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) ) -> ( x e. X |-> A ) e. ( ( J CnP K ) ` D ) )
44 simplrl
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) ) -> v e. K )
45 simprl
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) ) -> ( ( x e. X |-> A ) ` D ) e. v )
46 cnpimaex
 |-  ( ( ( x e. X |-> A ) e. ( ( J CnP K ) ` D ) /\ v e. K /\ ( ( x e. X |-> A ) ` D ) e. v ) -> E. r e. J ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) )
47 43 44 45 46 syl3anc
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) ) -> E. r e. J ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) )
48 6 ad2antrr
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) ) -> ( x e. X |-> B ) e. ( ( J CnP L ) ` D ) )
49 simplrr
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) ) -> w e. L )
50 simprr
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) ) -> ( ( x e. X |-> B ) ` D ) e. w )
51 cnpimaex
 |-  ( ( ( x e. X |-> B ) e. ( ( J CnP L ) ` D ) /\ w e. L /\ ( ( x e. X |-> B ) ` D ) e. w ) -> E. s e. J ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) )
52 48 49 50 51 syl3anc
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) ) -> E. s e. J ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) )
53 47 52 jca
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) ) -> ( E. r e. J ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ E. s e. J ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) )
54 53 ex
 |-  ( ( ph /\ ( v e. K /\ w e. L ) ) -> ( ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) -> ( E. r e. J ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ E. s e. J ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) ) )
55 opelxp
 |-  ( <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >. e. ( v X. w ) <-> ( ( ( x e. X |-> A ) ` D ) e. v /\ ( ( x e. X |-> B ) ` D ) e. w ) )
56 reeanv
 |-  ( E. r e. J E. s e. J ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) <-> ( E. r e. J ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ E. s e. J ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) )
57 54 55 56 3imtr4g
 |-  ( ( ph /\ ( v e. K /\ w e. L ) ) -> ( <. ( ( x e. X |-> A ) ` D ) , ( ( x e. X |-> B ) ` D ) >. e. ( v X. w ) -> E. r e. J E. s e. J ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) ) )
58 42 57 sylbid
 |-  ( ( ph /\ ( v e. K /\ w e. L ) ) -> ( ( ( x e. X |-> <. A , B >. ) ` D ) e. ( v X. w ) -> E. r e. J E. s e. J ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) ) )
59 an4
 |-  ( ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) <-> ( ( D e. r /\ D e. s ) /\ ( ( ( x e. X |-> A ) " r ) C_ v /\ ( ( x e. X |-> B ) " s ) C_ w ) ) )
60 elin
 |-  ( D e. ( r i^i s ) <-> ( D e. r /\ D e. s ) )
61 60 biimpri
 |-  ( ( D e. r /\ D e. s ) -> D e. ( r i^i s ) )
62 61 a1i
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( r e. J /\ s e. J ) ) -> ( ( D e. r /\ D e. s ) -> D e. ( r i^i s ) ) )
63 simpl
 |-  ( ( r e. J /\ s e. J ) -> r e. J )
64 toponss
 |-  ( ( J e. ( TopOn ` X ) /\ r e. J ) -> r C_ X )
65 1 63 64 syl2an
 |-  ( ( ph /\ ( r e. J /\ s e. J ) ) -> r C_ X )
66 ssinss1
 |-  ( r C_ X -> ( r i^i s ) C_ X )
67 66 adantl
 |-  ( ( ph /\ r C_ X ) -> ( r i^i s ) C_ X )
68 67 sselda
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> t e. X )
69 28 ad2antrr
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> A. x e. X ( ( x e. X |-> <. A , B >. ) ` x ) = <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. )
70 nffvmpt1
 |-  F/_ x ( ( x e. X |-> <. A , B >. ) ` t )
71 nffvmpt1
 |-  F/_ x ( ( x e. X |-> A ) ` t )
72 nffvmpt1
 |-  F/_ x ( ( x e. X |-> B ) ` t )
73 71 72 nfop
 |-  F/_ x <. ( ( x e. X |-> A ) ` t ) , ( ( x e. X |-> B ) ` t ) >.
74 70 73 nfeq
 |-  F/ x ( ( x e. X |-> <. A , B >. ) ` t ) = <. ( ( x e. X |-> A ) ` t ) , ( ( x e. X |-> B ) ` t ) >.
75 fveq2
 |-  ( x = t -> ( ( x e. X |-> <. A , B >. ) ` x ) = ( ( x e. X |-> <. A , B >. ) ` t ) )
76 fveq2
 |-  ( x = t -> ( ( x e. X |-> A ) ` x ) = ( ( x e. X |-> A ) ` t ) )
77 fveq2
 |-  ( x = t -> ( ( x e. X |-> B ) ` x ) = ( ( x e. X |-> B ) ` t ) )
78 76 77 opeq12d
 |-  ( x = t -> <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. = <. ( ( x e. X |-> A ) ` t ) , ( ( x e. X |-> B ) ` t ) >. )
79 75 78 eqeq12d
 |-  ( x = t -> ( ( ( x e. X |-> <. A , B >. ) ` x ) = <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. <-> ( ( x e. X |-> <. A , B >. ) ` t ) = <. ( ( x e. X |-> A ) ` t ) , ( ( x e. X |-> B ) ` t ) >. ) )
80 74 79 rspc
 |-  ( t e. X -> ( A. x e. X ( ( x e. X |-> <. A , B >. ) ` x ) = <. ( ( x e. X |-> A ) ` x ) , ( ( x e. X |-> B ) ` x ) >. -> ( ( x e. X |-> <. A , B >. ) ` t ) = <. ( ( x e. X |-> A ) ` t ) , ( ( x e. X |-> B ) ` t ) >. ) )
81 68 69 80 sylc
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( ( x e. X |-> <. A , B >. ) ` t ) = <. ( ( x e. X |-> A ) ` t ) , ( ( x e. X |-> B ) ` t ) >. )
82 simpr
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> t e. ( r i^i s ) )
83 82 elin1d
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> t e. r )
84 8 ad2antrr
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( x e. X |-> A ) : X --> Y )
85 84 ffund
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> Fun ( x e. X |-> A ) )
86 67 adantr
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( r i^i s ) C_ X )
87 84 fdmd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> dom ( x e. X |-> A ) = X )
88 86 87 sseqtrrd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( r i^i s ) C_ dom ( x e. X |-> A ) )
89 88 82 sseldd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> t e. dom ( x e. X |-> A ) )
90 funfvima
 |-  ( ( Fun ( x e. X |-> A ) /\ t e. dom ( x e. X |-> A ) ) -> ( t e. r -> ( ( x e. X |-> A ) ` t ) e. ( ( x e. X |-> A ) " r ) ) )
91 85 89 90 syl2anc
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( t e. r -> ( ( x e. X |-> A ) ` t ) e. ( ( x e. X |-> A ) " r ) ) )
92 83 91 mpd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( ( x e. X |-> A ) ` t ) e. ( ( x e. X |-> A ) " r ) )
93 82 elin2d
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> t e. s )
94 11 ad2antrr
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( x e. X |-> B ) : X --> Z )
95 94 ffund
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> Fun ( x e. X |-> B ) )
96 94 fdmd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> dom ( x e. X |-> B ) = X )
97 86 96 sseqtrrd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( r i^i s ) C_ dom ( x e. X |-> B ) )
98 97 82 sseldd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> t e. dom ( x e. X |-> B ) )
99 funfvima
 |-  ( ( Fun ( x e. X |-> B ) /\ t e. dom ( x e. X |-> B ) ) -> ( t e. s -> ( ( x e. X |-> B ) ` t ) e. ( ( x e. X |-> B ) " s ) ) )
100 95 98 99 syl2anc
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( t e. s -> ( ( x e. X |-> B ) ` t ) e. ( ( x e. X |-> B ) " s ) ) )
101 93 100 mpd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( ( x e. X |-> B ) ` t ) e. ( ( x e. X |-> B ) " s ) )
102 92 101 opelxpd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> <. ( ( x e. X |-> A ) ` t ) , ( ( x e. X |-> B ) ` t ) >. e. ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) )
103 81 102 eqeltrd
 |-  ( ( ( ph /\ r C_ X ) /\ t e. ( r i^i s ) ) -> ( ( x e. X |-> <. A , B >. ) ` t ) e. ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) )
104 103 ralrimiva
 |-  ( ( ph /\ r C_ X ) -> A. t e. ( r i^i s ) ( ( x e. X |-> <. A , B >. ) ` t ) e. ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) )
105 14 ffund
 |-  ( ph -> Fun ( x e. X |-> <. A , B >. ) )
106 105 adantr
 |-  ( ( ph /\ r C_ X ) -> Fun ( x e. X |-> <. A , B >. ) )
107 14 fdmd
 |-  ( ph -> dom ( x e. X |-> <. A , B >. ) = X )
108 107 adantr
 |-  ( ( ph /\ r C_ X ) -> dom ( x e. X |-> <. A , B >. ) = X )
109 67 108 sseqtrrd
 |-  ( ( ph /\ r C_ X ) -> ( r i^i s ) C_ dom ( x e. X |-> <. A , B >. ) )
110 funimass4
 |-  ( ( Fun ( x e. X |-> <. A , B >. ) /\ ( r i^i s ) C_ dom ( x e. X |-> <. A , B >. ) ) -> ( ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) <-> A. t e. ( r i^i s ) ( ( x e. X |-> <. A , B >. ) ` t ) e. ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) ) )
111 106 109 110 syl2anc
 |-  ( ( ph /\ r C_ X ) -> ( ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) <-> A. t e. ( r i^i s ) ( ( x e. X |-> <. A , B >. ) ` t ) e. ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) ) )
112 104 111 mpbird
 |-  ( ( ph /\ r C_ X ) -> ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) )
113 65 112 syldan
 |-  ( ( ph /\ ( r e. J /\ s e. J ) ) -> ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) )
114 113 adantlr
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( r e. J /\ s e. J ) ) -> ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) )
115 xpss12
 |-  ( ( ( ( x e. X |-> A ) " r ) C_ v /\ ( ( x e. X |-> B ) " s ) C_ w ) -> ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) C_ ( v X. w ) )
116 sstr2
 |-  ( ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) -> ( ( ( ( x e. X |-> A ) " r ) X. ( ( x e. X |-> B ) " s ) ) C_ ( v X. w ) -> ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( v X. w ) ) )
117 114 115 116 syl2im
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( r e. J /\ s e. J ) ) -> ( ( ( ( x e. X |-> A ) " r ) C_ v /\ ( ( x e. X |-> B ) " s ) C_ w ) -> ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( v X. w ) ) )
118 62 117 anim12d
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( r e. J /\ s e. J ) ) -> ( ( ( D e. r /\ D e. s ) /\ ( ( ( x e. X |-> A ) " r ) C_ v /\ ( ( x e. X |-> B ) " s ) C_ w ) ) -> ( D e. ( r i^i s ) /\ ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( v X. w ) ) ) )
119 59 118 syl5bi
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( r e. J /\ s e. J ) ) -> ( ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) -> ( D e. ( r i^i s ) /\ ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( v X. w ) ) ) )
120 topontop
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
121 1 120 syl
 |-  ( ph -> J e. Top )
122 inopn
 |-  ( ( J e. Top /\ r e. J /\ s e. J ) -> ( r i^i s ) e. J )
123 122 3expb
 |-  ( ( J e. Top /\ ( r e. J /\ s e. J ) ) -> ( r i^i s ) e. J )
124 121 123 sylan
 |-  ( ( ph /\ ( r e. J /\ s e. J ) ) -> ( r i^i s ) e. J )
125 124 adantlr
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( r e. J /\ s e. J ) ) -> ( r i^i s ) e. J )
126 119 125 jctild
 |-  ( ( ( ph /\ ( v e. K /\ w e. L ) ) /\ ( r e. J /\ s e. J ) ) -> ( ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) -> ( ( r i^i s ) e. J /\ ( D e. ( r i^i s ) /\ ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( v X. w ) ) ) ) )
127 126 expimpd
 |-  ( ( ph /\ ( v e. K /\ w e. L ) ) -> ( ( ( r e. J /\ s e. J ) /\ ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) ) -> ( ( r i^i s ) e. J /\ ( D e. ( r i^i s ) /\ ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( v X. w ) ) ) ) )
128 eleq2
 |-  ( z = ( r i^i s ) -> ( D e. z <-> D e. ( r i^i s ) ) )
129 imaeq2
 |-  ( z = ( r i^i s ) -> ( ( x e. X |-> <. A , B >. ) " z ) = ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) )
130 129 sseq1d
 |-  ( z = ( r i^i s ) -> ( ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) <-> ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( v X. w ) ) )
131 128 130 anbi12d
 |-  ( z = ( r i^i s ) -> ( ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) <-> ( D e. ( r i^i s ) /\ ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( v X. w ) ) ) )
132 131 rspcev
 |-  ( ( ( r i^i s ) e. J /\ ( D e. ( r i^i s ) /\ ( ( x e. X |-> <. A , B >. ) " ( r i^i s ) ) C_ ( v X. w ) ) ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) )
133 127 132 syl6
 |-  ( ( ph /\ ( v e. K /\ w e. L ) ) -> ( ( ( r e. J /\ s e. J ) /\ ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) )
134 133 expd
 |-  ( ( ph /\ ( v e. K /\ w e. L ) ) -> ( ( r e. J /\ s e. J ) -> ( ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) ) )
135 134 rexlimdvv
 |-  ( ( ph /\ ( v e. K /\ w e. L ) ) -> ( E. r e. J E. s e. J ( ( D e. r /\ ( ( x e. X |-> A ) " r ) C_ v ) /\ ( D e. s /\ ( ( x e. X |-> B ) " s ) C_ w ) ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) )
136 58 135 syld
 |-  ( ( ph /\ ( v e. K /\ w e. L ) ) -> ( ( ( x e. X |-> <. A , B >. ) ` D ) e. ( v X. w ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) )
137 136 ralrimivva
 |-  ( ph -> A. v e. K A. w e. L ( ( ( x e. X |-> <. A , B >. ) ` D ) e. ( v X. w ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) )
138 vex
 |-  v e. _V
139 vex
 |-  w e. _V
140 138 139 xpex
 |-  ( v X. w ) e. _V
141 140 rgen2w
 |-  A. v e. K A. w e. L ( v X. w ) e. _V
142 eqid
 |-  ( v e. K , w e. L |-> ( v X. w ) ) = ( v e. K , w e. L |-> ( v X. w ) )
143 eleq2
 |-  ( y = ( v X. w ) -> ( ( ( x e. X |-> <. A , B >. ) ` D ) e. y <-> ( ( x e. X |-> <. A , B >. ) ` D ) e. ( v X. w ) ) )
144 sseq2
 |-  ( y = ( v X. w ) -> ( ( ( x e. X |-> <. A , B >. ) " z ) C_ y <-> ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) )
145 144 anbi2d
 |-  ( y = ( v X. w ) -> ( ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ y ) <-> ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) )
146 145 rexbidv
 |-  ( y = ( v X. w ) -> ( E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ y ) <-> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) )
147 143 146 imbi12d
 |-  ( y = ( v X. w ) -> ( ( ( ( x e. X |-> <. A , B >. ) ` D ) e. y -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ y ) ) <-> ( ( ( x e. X |-> <. A , B >. ) ` D ) e. ( v X. w ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) ) )
148 142 147 ralrnmpo
 |-  ( A. v e. K A. w e. L ( v X. w ) e. _V -> ( A. y e. ran ( v e. K , w e. L |-> ( v X. w ) ) ( ( ( x e. X |-> <. A , B >. ) ` D ) e. y -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ y ) ) <-> A. v e. K A. w e. L ( ( ( x e. X |-> <. A , B >. ) ` D ) e. ( v X. w ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) ) )
149 141 148 ax-mp
 |-  ( A. y e. ran ( v e. K , w e. L |-> ( v X. w ) ) ( ( ( x e. X |-> <. A , B >. ) ` D ) e. y -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ y ) ) <-> A. v e. K A. w e. L ( ( ( x e. X |-> <. A , B >. ) ` D ) e. ( v X. w ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ ( v X. w ) ) ) )
150 137 149 sylibr
 |-  ( ph -> A. y e. ran ( v e. K , w e. L |-> ( v X. w ) ) ( ( ( x e. X |-> <. A , B >. ) ` D ) e. y -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ y ) ) )
151 topontop
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
152 2 151 syl
 |-  ( ph -> K e. Top )
153 topontop
 |-  ( L e. ( TopOn ` Z ) -> L e. Top )
154 3 153 syl
 |-  ( ph -> L e. Top )
155 eqid
 |-  ran ( v e. K , w e. L |-> ( v X. w ) ) = ran ( v e. K , w e. L |-> ( v X. w ) )
156 155 txval
 |-  ( ( K e. Top /\ L e. Top ) -> ( K tX L ) = ( topGen ` ran ( v e. K , w e. L |-> ( v X. w ) ) ) )
157 152 154 156 syl2anc
 |-  ( ph -> ( K tX L ) = ( topGen ` ran ( v e. K , w e. L |-> ( v X. w ) ) ) )
158 txtopon
 |-  ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` Z ) ) -> ( K tX L ) e. ( TopOn ` ( Y X. Z ) ) )
159 2 3 158 syl2anc
 |-  ( ph -> ( K tX L ) e. ( TopOn ` ( Y X. Z ) ) )
160 1 157 159 4 tgcnp
 |-  ( ph -> ( ( x e. X |-> <. A , B >. ) e. ( ( J CnP ( K tX L ) ) ` D ) <-> ( ( x e. X |-> <. A , B >. ) : X --> ( Y X. Z ) /\ A. y e. ran ( v e. K , w e. L |-> ( v X. w ) ) ( ( ( x e. X |-> <. A , B >. ) ` D ) e. y -> E. z e. J ( D e. z /\ ( ( x e. X |-> <. A , B >. ) " z ) C_ y ) ) ) ) )
161 14 150 160 mpbir2and
 |-  ( ph -> ( x e. X |-> <. A , B >. ) e. ( ( J CnP ( K tX L ) ) ` D ) )