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 ) )