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 φ F : X Z
txomap.g φ G : Y T
txomap.j φ J TopOn X
txomap.k φ K TopOn Y
txomap.l φ L TopOn Z
txomap.m φ M TopOn T
txomap.1 φ x J F x L
txomap.2 φ y K G y M
txomap.a φ A J × t K
txomap.h H = x X , y Y F x G y
Assertion txomap φ H A L × t M

Proof

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