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 ( 𝜑𝐹 : 𝑋𝑍 )
txomap.g ( 𝜑𝐺 : 𝑌𝑇 )
txomap.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
txomap.k ( 𝜑𝐾 ∈ ( TopOn ‘ 𝑌 ) )
txomap.l ( 𝜑𝐿 ∈ ( TopOn ‘ 𝑍 ) )
txomap.m ( 𝜑𝑀 ∈ ( TopOn ‘ 𝑇 ) )
txomap.1 ( ( 𝜑𝑥𝐽 ) → ( 𝐹𝑥 ) ∈ 𝐿 )
txomap.2 ( ( 𝜑𝑦𝐾 ) → ( 𝐺𝑦 ) ∈ 𝑀 )
txomap.a ( 𝜑𝐴 ∈ ( 𝐽 ×t 𝐾 ) )
txomap.h 𝐻 = ( 𝑥𝑋 , 𝑦𝑌 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑦 ) ⟩ )
Assertion txomap ( 𝜑 → ( 𝐻𝐴 ) ∈ ( 𝐿 ×t 𝑀 ) )

Proof

Step Hyp Ref Expression
1 txomap.f ( 𝜑𝐹 : 𝑋𝑍 )
2 txomap.g ( 𝜑𝐺 : 𝑌𝑇 )
3 txomap.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 txomap.k ( 𝜑𝐾 ∈ ( TopOn ‘ 𝑌 ) )
5 txomap.l ( 𝜑𝐿 ∈ ( TopOn ‘ 𝑍 ) )
6 txomap.m ( 𝜑𝑀 ∈ ( TopOn ‘ 𝑇 ) )
7 txomap.1 ( ( 𝜑𝑥𝐽 ) → ( 𝐹𝑥 ) ∈ 𝐿 )
8 txomap.2 ( ( 𝜑𝑦𝐾 ) → ( 𝐺𝑦 ) ∈ 𝑀 )
9 txomap.a ( 𝜑𝐴 ∈ ( 𝐽 ×t 𝐾 ) )
10 txomap.h 𝐻 = ( 𝑥𝑋 , 𝑦𝑌 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑦 ) ⟩ )
11 simp-6l ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝜑 )
12 simpllr ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑥𝐽 )
13 11 12 7 syl2anc ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐹𝑥 ) ∈ 𝐿 )
14 simplr ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑦𝐾 )
15 11 14 8 syl2anc ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐺𝑦 ) ∈ 𝑀 )
16 opex ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑦 ) ⟩ ∈ V
17 10 16 fnmpoi 𝐻 Fn ( 𝑋 × 𝑌 )
18 3 ad6antr ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19 toponss ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥𝐽 ) → 𝑥𝑋 )
20 18 12 19 syl2anc ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑥𝑋 )
21 4 ad6antr ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
22 toponss ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑦𝐾 ) → 𝑦𝑌 )
23 21 14 22 syl2anc ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑦𝑌 )
24 xpss12 ( ( 𝑥𝑋𝑦𝑌 ) → ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) )
25 20 23 24 syl2anc ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) )
26 simprl ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑧 ∈ ( 𝑥 × 𝑦 ) )
27 fnfvima ( ( 𝐻 Fn ( 𝑋 × 𝑌 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ( 𝑥 × 𝑦 ) ) → ( 𝐻𝑧 ) ∈ ( 𝐻 “ ( 𝑥 × 𝑦 ) ) )
28 17 25 26 27 mp3an2i ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐻𝑧 ) ∈ ( 𝐻 “ ( 𝑥 × 𝑦 ) ) )
29 simp-4r ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐻𝑧 ) = 𝑐 )
30 ffn ( 𝐹 : 𝑋𝑍𝐹 Fn 𝑋 )
31 11 1 30 3syl ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝐹 Fn 𝑋 )
32 ffn ( 𝐺 : 𝑌𝑇𝐺 Fn 𝑌 )
33 11 2 32 3syl ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝐺 Fn 𝑌 )
34 10 31 33 20 23 fimaproj ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐻 “ ( 𝑥 × 𝑦 ) ) = ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) )
35 28 29 34 3eltr3d ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑐 ∈ ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) )
36 imass2 ( ( 𝑥 × 𝑦 ) ⊆ 𝐴 → ( 𝐻 “ ( 𝑥 × 𝑦 ) ) ⊆ ( 𝐻𝐴 ) )
37 36 ad2antll ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐻 “ ( 𝑥 × 𝑦 ) ) ⊆ ( 𝐻𝐴 ) )
38 34 37 eqsstrrd ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) ⊆ ( 𝐻𝐴 ) )
39 xpeq1 ( 𝑎 = ( 𝐹𝑥 ) → ( 𝑎 × 𝑏 ) = ( ( 𝐹𝑥 ) × 𝑏 ) )
40 39 eleq2d ( 𝑎 = ( 𝐹𝑥 ) → ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ↔ 𝑐 ∈ ( ( 𝐹𝑥 ) × 𝑏 ) ) )
41 39 sseq1d ( 𝑎 = ( 𝐹𝑥 ) → ( ( 𝑎 × 𝑏 ) ⊆ ( 𝐻𝐴 ) ↔ ( ( 𝐹𝑥 ) × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) )
42 40 41 anbi12d ( 𝑎 = ( 𝐹𝑥 ) → ( ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) ↔ ( 𝑐 ∈ ( ( 𝐹𝑥 ) × 𝑏 ) ∧ ( ( 𝐹𝑥 ) × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) ) )
43 xpeq2 ( 𝑏 = ( 𝐺𝑦 ) → ( ( 𝐹𝑥 ) × 𝑏 ) = ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) )
44 43 eleq2d ( 𝑏 = ( 𝐺𝑦 ) → ( 𝑐 ∈ ( ( 𝐹𝑥 ) × 𝑏 ) ↔ 𝑐 ∈ ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) ) )
45 43 sseq1d ( 𝑏 = ( 𝐺𝑦 ) → ( ( ( 𝐹𝑥 ) × 𝑏 ) ⊆ ( 𝐻𝐴 ) ↔ ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) ⊆ ( 𝐻𝐴 ) ) )
46 44 45 anbi12d ( 𝑏 = ( 𝐺𝑦 ) → ( ( 𝑐 ∈ ( ( 𝐹𝑥 ) × 𝑏 ) ∧ ( ( 𝐹𝑥 ) × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) ↔ ( 𝑐 ∈ ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) ∧ ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) ⊆ ( 𝐻𝐴 ) ) ) )
47 42 46 rspc2ev ( ( ( 𝐹𝑥 ) ∈ 𝐿 ∧ ( 𝐺𝑦 ) ∈ 𝑀 ∧ ( 𝑐 ∈ ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) ∧ ( ( 𝐹𝑥 ) × ( 𝐺𝑦 ) ) ⊆ ( 𝐻𝐴 ) ) ) → ∃ 𝑎𝐿𝑏𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) )
48 13 15 35 38 47 syl112anc ( ( ( ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) ∧ 𝑥𝐽 ) ∧ 𝑦𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ∃ 𝑎𝐿𝑏𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) )
49 eltx ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐴 ∈ ( 𝐽 ×t 𝐾 ) ↔ ∀ 𝑧𝐴𝑥𝐽𝑦𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) )
50 3 4 49 syl2anc ( 𝜑 → ( 𝐴 ∈ ( 𝐽 ×t 𝐾 ) ↔ ∀ 𝑧𝐴𝑥𝐽𝑦𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) )
51 9 50 mpbid ( 𝜑 → ∀ 𝑧𝐴𝑥𝐽𝑦𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) )
52 51 r19.21bi ( ( 𝜑𝑧𝐴 ) → ∃ 𝑥𝐽𝑦𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) )
53 52 ad4ant13 ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) → ∃ 𝑥𝐽𝑦𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) )
54 48 53 r19.29vva ( ( ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) ∧ 𝑧𝐴 ) ∧ ( 𝐻𝑧 ) = 𝑐 ) → ∃ 𝑎𝐿𝑏𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) )
55 10 mpofun Fun 𝐻
56 fvelima ( ( Fun 𝐻𝑐 ∈ ( 𝐻𝐴 ) ) → ∃ 𝑧𝐴 ( 𝐻𝑧 ) = 𝑐 )
57 55 56 mpan ( 𝑐 ∈ ( 𝐻𝐴 ) → ∃ 𝑧𝐴 ( 𝐻𝑧 ) = 𝑐 )
58 57 adantl ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) → ∃ 𝑧𝐴 ( 𝐻𝑧 ) = 𝑐 )
59 54 58 r19.29a ( ( 𝜑𝑐 ∈ ( 𝐻𝐴 ) ) → ∃ 𝑎𝐿𝑏𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) )
60 59 ralrimiva ( 𝜑 → ∀ 𝑐 ∈ ( 𝐻𝐴 ) ∃ 𝑎𝐿𝑏𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) )
61 eltx ( ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ 𝑀 ∈ ( TopOn ‘ 𝑇 ) ) → ( ( 𝐻𝐴 ) ∈ ( 𝐿 ×t 𝑀 ) ↔ ∀ 𝑐 ∈ ( 𝐻𝐴 ) ∃ 𝑎𝐿𝑏𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) ) )
62 5 6 61 syl2anc ( 𝜑 → ( ( 𝐻𝐴 ) ∈ ( 𝐿 ×t 𝑀 ) ↔ ∀ 𝑐 ∈ ( 𝐻𝐴 ) ∃ 𝑎𝐿𝑏𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻𝐴 ) ) ) )
63 60 62 mpbird ( 𝜑 → ( 𝐻𝐴 ) ∈ ( 𝐿 ×t 𝑀 ) )