Metamath Proof Explorer

Theorem txss12

Description: Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion txss12 
|- ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( A tX C ) C_ ( B tX D ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran ( x e. B , y e. D |-> ( x X. y ) ) = ran ( x e. B , y e. D |-> ( x X. y ) )
2 1 txbasex 
 |-  ( ( B e. V /\ D e. W ) -> ran ( x e. B , y e. D |-> ( x X. y ) ) e. _V )
3 resmpo 
 |-  ( ( A C_ B /\ C C_ D ) -> ( ( x e. B , y e. D |-> ( x X. y ) ) |` ( A X. C ) ) = ( x e. A , y e. C |-> ( x X. y ) ) )
4 resss 
 |-  ( ( x e. B , y e. D |-> ( x X. y ) ) |` ( A X. C ) ) C_ ( x e. B , y e. D |-> ( x X. y ) )
5 3 4 eqsstrrdi 
 |-  ( ( A C_ B /\ C C_ D ) -> ( x e. A , y e. C |-> ( x X. y ) ) C_ ( x e. B , y e. D |-> ( x X. y ) ) )
6 5 adantl 
 |-  ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( x e. A , y e. C |-> ( x X. y ) ) C_ ( x e. B , y e. D |-> ( x X. y ) ) )
7 rnss 
 |-  ( ( x e. A , y e. C |-> ( x X. y ) ) C_ ( x e. B , y e. D |-> ( x X. y ) ) -> ran ( x e. A , y e. C |-> ( x X. y ) ) C_ ran ( x e. B , y e. D |-> ( x X. y ) ) )
8 6 7 syl 
 |-  ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ran ( x e. A , y e. C |-> ( x X. y ) ) C_ ran ( x e. B , y e. D |-> ( x X. y ) ) )
9 tgss 
 |-  ( ( ran ( x e. B , y e. D |-> ( x X. y ) ) e. _V /\ ran ( x e. A , y e. C |-> ( x X. y ) ) C_ ran ( x e. B , y e. D |-> ( x X. y ) ) ) -> ( topGen ` ran ( x e. A , y e. C |-> ( x X. y ) ) ) C_ ( topGen ` ran ( x e. B , y e. D |-> ( x X. y ) ) ) )
10 2 8 9 syl2an2r 
 |-  ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( topGen ` ran ( x e. A , y e. C |-> ( x X. y ) ) ) C_ ( topGen ` ran ( x e. B , y e. D |-> ( x X. y ) ) ) )
11 ssexg 
 |-  ( ( A C_ B /\ B e. V ) -> A e. _V )
12 ssexg 
 |-  ( ( C C_ D /\ D e. W ) -> C e. _V )
13 eqid 
 |-  ran ( x e. A , y e. C |-> ( x X. y ) ) = ran ( x e. A , y e. C |-> ( x X. y ) )
14 13 txval 
 |-  ( ( A e. _V /\ C e. _V ) -> ( A tX C ) = ( topGen ` ran ( x e. A , y e. C |-> ( x X. y ) ) ) )
15 11 12 14 syl2an 
 |-  ( ( ( A C_ B /\ B e. V ) /\ ( C C_ D /\ D e. W ) ) -> ( A tX C ) = ( topGen ` ran ( x e. A , y e. C |-> ( x X. y ) ) ) )
16 15 an4s 
 |-  ( ( ( A C_ B /\ C C_ D ) /\ ( B e. V /\ D e. W ) ) -> ( A tX C ) = ( topGen ` ran ( x e. A , y e. C |-> ( x X. y ) ) ) )
17 16 ancoms 
 |-  ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( A tX C ) = ( topGen ` ran ( x e. A , y e. C |-> ( x X. y ) ) ) )
18 1 txval 
 |-  ( ( B e. V /\ D e. W ) -> ( B tX D ) = ( topGen ` ran ( x e. B , y e. D |-> ( x X. y ) ) ) )
19 18 adantr 
 |-  ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( B tX D ) = ( topGen ` ran ( x e. B , y e. D |-> ( x X. y ) ) ) )
20 10 17 19 3sstr4d 
 |-  ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( A tX C ) C_ ( B tX D ) )