Metamath Proof Explorer

Theorem txomap

Description: Given two open maps F and G , H mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019)

Ref Expression
Hypotheses txomap.f 
|- ( ph -> F : X --> Z )
txomap.g 
|- ( ph -> G : Y --> T )
txomap.j 
|- ( ph -> J e. ( TopOn ` X ) )
txomap.k 
|- ( ph -> K e. ( TopOn ` Y ) )
txomap.l 
|- ( ph -> L e. ( TopOn ` Z ) )
txomap.m 
|- ( ph -> M e. ( TopOn ` T ) )
txomap.1 
|- ( ( ph /\ x e. J ) -> ( F " x ) e. L )
txomap.2 
|- ( ( ph /\ y e. K ) -> ( G " y ) e. M )
txomap.a 
|- ( ph -> A e. ( J tX K ) )
txomap.h 
|- H = ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. )
Assertion txomap 
|- ( ph -> ( H " A ) e. ( L tX M ) )

Proof

Step Hyp Ref Expression
1 txomap.f 
 |-  ( ph -> F : X --> Z )
2 txomap.g 
 |-  ( ph -> G : Y --> T )
3 txomap.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 txomap.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
5 txomap.l 
 |-  ( ph -> L e. ( TopOn ` Z ) )
6 txomap.m 
 |-  ( ph -> M e. ( TopOn ` T ) )
7 txomap.1 
 |-  ( ( ph /\ x e. J ) -> ( F " x ) e. L )
8 txomap.2 
 |-  ( ( ph /\ y e. K ) -> ( G " y ) e. M )
9 txomap.a 
 |-  ( ph -> A e. ( J tX K ) )
10 txomap.h 
 |-  H = ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. )
11 simp-6l 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> ph )
12 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> x e. J )
13 11 12 7 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> ( F " x ) e. L )
14 simplr 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> y e. K )
15 11 14 8 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> ( G " y ) e. M )
16 opex 
 |-  <. ( F ` x ) , ( G ` y ) >. e. _V
17 10 16 fnmpoi 
 |-  H Fn ( X X. Y )
18 3 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> J e. ( TopOn ` X ) )
19 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X )
20 18 12 19 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> x C_ X )
21 4 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> K e. ( TopOn ` Y ) )
22 toponss 
 |-  ( ( K e. ( TopOn ` Y ) /\ y e. K ) -> y C_ Y )
23 21 14 22 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> y C_ Y )
24 xpss12 
 |-  ( ( x C_ X /\ y C_ Y ) -> ( x X. y ) C_ ( X X. Y ) )
25 20 23 24 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> ( x X. y ) C_ ( X X. Y ) )
26 simprl 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> z e. ( x X. y ) )
27 fnfvima 
 |-  ( ( H Fn ( X X. Y ) /\ ( x X. y ) C_ ( X X. Y ) /\ z e. ( x X. y ) ) -> ( H ` z ) e. ( H " ( x X. y ) ) )
28 17 25 26 27 mp3an2i 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> ( H ` z ) e. ( H " ( x X. y ) ) )
29 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> ( H ` z ) = c )
30 ffn 
 |-  ( F : X --> Z -> F Fn X )
31 11 1 30 3syl 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> F Fn X )
32 ffn 
 |-  ( G : Y --> T -> G Fn Y )
33 11 2 32 3syl 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> G Fn Y )
34 10 31 33 20 23 fimaproj 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> ( H " ( x X. y ) ) = ( ( F " x ) X. ( G " y ) ) )
35 28 29 34 3eltr3d 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> c e. ( ( F " x ) X. ( G " y ) ) )
36 imass2 
 |-  ( ( x X. y ) C_ A -> ( H " ( x X. y ) ) C_ ( H " A ) )
37 36 ad2antll 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> ( H " ( x X. y ) ) C_ ( H " A ) )
38 34 37 eqsstrrd 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> ( ( F " x ) X. ( G " y ) ) C_ ( H " A ) )
39 xpeq1 
 |-  ( a = ( F " x ) -> ( a X. b ) = ( ( F " x ) X. b ) )
40 39 eleq2d 
 |-  ( a = ( F " x ) -> ( c e. ( a X. b ) <-> c e. ( ( F " x ) X. b ) ) )
41 39 sseq1d 
 |-  ( a = ( F " x ) -> ( ( a X. b ) C_ ( H " A ) <-> ( ( F " x ) X. b ) C_ ( H " A ) ) )
42 40 41 anbi12d 
 |-  ( a = ( F " x ) -> ( ( c e. ( a X. b ) /\ ( a X. b ) C_ ( H " A ) ) <-> ( c e. ( ( F " x ) X. b ) /\ ( ( F " x ) X. b ) C_ ( H " A ) ) ) )
43 xpeq2 
 |-  ( b = ( G " y ) -> ( ( F " x ) X. b ) = ( ( F " x ) X. ( G " y ) ) )
44 43 eleq2d 
 |-  ( b = ( G " y ) -> ( c e. ( ( F " x ) X. b ) <-> c e. ( ( F " x ) X. ( G " y ) ) ) )
45 43 sseq1d 
 |-  ( b = ( G " y ) -> ( ( ( F " x ) X. b ) C_ ( H " A ) <-> ( ( F " x ) X. ( G " y ) ) C_ ( H " A ) ) )
46 44 45 anbi12d 
 |-  ( b = ( G " y ) -> ( ( c e. ( ( F " x ) X. b ) /\ ( ( F " x ) X. b ) C_ ( H " A ) ) <-> ( c e. ( ( F " x ) X. ( G " y ) ) /\ ( ( F " x ) X. ( G " y ) ) C_ ( H " A ) ) ) )
47 42 46 rspc2ev 
 |-  ( ( ( F " x ) e. L /\ ( G " y ) e. M /\ ( c e. ( ( F " x ) X. ( G " y ) ) /\ ( ( F " x ) X. ( G " y ) ) C_ ( H " A ) ) ) -> E. a e. L E. b e. M ( c e. ( a X. b ) /\ ( a X. b ) C_ ( H " A ) ) )
48 13 15 35 38 47 syl112anc 
 |-  ( ( ( ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) /\ x e. J ) /\ y e. K ) /\ ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) -> E. a e. L E. b e. M ( c e. ( a X. b ) /\ ( a X. b ) C_ ( H " A ) ) )
49 eltx 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( A e. ( J tX K ) <-> A. z e. A E. x e. J E. y e. K ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) )
50 3 4 49 syl2anc 
 |-  ( ph -> ( A e. ( J tX K ) <-> A. z e. A E. x e. J E. y e. K ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) ) )
51 9 50 mpbid 
 |-  ( ph -> A. z e. A E. x e. J E. y e. K ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) )
52 51 r19.21bi 
 |-  ( ( ph /\ z e. A ) -> E. x e. J E. y e. K ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) )
53 52 ad4ant13 
 |-  ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) -> E. x e. J E. y e. K ( z e. ( x X. y ) /\ ( x X. y ) C_ A ) )
54 48 53 r19.29vva 
 |-  ( ( ( ( ph /\ c e. ( H " A ) ) /\ z e. A ) /\ ( H ` z ) = c ) -> E. a e. L E. b e. M ( c e. ( a X. b ) /\ ( a X. b ) C_ ( H " A ) ) )
55 10 mpofun 
 |-  Fun H
56 fvelima 
 |-  ( ( Fun H /\ c e. ( H " A ) ) -> E. z e. A ( H ` z ) = c )
57 55 56 mpan 
 |-  ( c e. ( H " A ) -> E. z e. A ( H ` z ) = c )
58 57 adantl 
 |-  ( ( ph /\ c e. ( H " A ) ) -> E. z e. A ( H ` z ) = c )
59 54 58 r19.29a 
 |-  ( ( ph /\ c e. ( H " A ) ) -> E. a e. L E. b e. M ( c e. ( a X. b ) /\ ( a X. b ) C_ ( H " A ) ) )
60 59 ralrimiva 
 |-  ( ph -> A. c e. ( H " A ) E. a e. L E. b e. M ( c e. ( a X. b ) /\ ( a X. b ) C_ ( H " A ) ) )
61 eltx 
 |-  ( ( L e. ( TopOn ` Z ) /\ M e. ( TopOn ` T ) ) -> ( ( H " A ) e. ( L tX M ) <-> A. c e. ( H " A ) E. a e. L E. b e. M ( c e. ( a X. b ) /\ ( a X. b ) C_ ( H " A ) ) ) )
62 5 6 61 syl2anc 
 |-  ( ph -> ( ( H " A ) e. ( L tX M ) <-> A. c e. ( H " A ) E. a e. L E. b e. M ( c e. ( a X. b ) /\ ( a X. b ) C_ ( H " A ) ) ) )
63 60 62 mpbird 
 |-  ( ph -> ( H " A ) e. ( L tX M ) )