Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  txomap Structured version   Visualization version   GIF version

Theorem txomap 29229
 Description: Given two open maps 𝐹 and 𝐺, 𝐻 mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019.)
Hypotheses
Ref Expression
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
Ref Expression
txomap (𝜑 → (𝐻𝐴) ∈ (𝐿 ×t 𝑀))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦   𝑥,𝐻,𝑦   𝑥,𝐽,𝑦   𝑥,𝐾,𝑦   𝑥,𝐿,𝑦   𝑥,𝑀,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦)   𝑍(𝑥,𝑦)

Proof of Theorem txomap
Dummy variables 𝑎 𝑏 𝑐 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp-6l 806 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝜑)
2 simpllr 795 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝐽)
3 txomap.1 . . . . . . 7 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ 𝐿)
41, 2, 3syl2anc 691 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐹𝑥) ∈ 𝐿)
5 simplr 788 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝐾)
6 txomap.2 . . . . . . 7 ((𝜑𝑦𝐾) → (𝐺𝑦) ∈ 𝑀)
71, 5, 6syl2anc 691 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐺𝑦) ∈ 𝑀)
8 txomap.h . . . . . . . . . 10 𝐻 = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
9 opex 4859 . . . . . . . . . 10 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V
108, 9fnmpt2i 7128 . . . . . . . . 9 𝐻 Fn (𝑋 × 𝑌)
1110a1i 11 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐻 Fn (𝑋 × 𝑌))
12 txomap.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
131, 12syl 17 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
14 toponss 20544 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥𝐽) → 𝑥𝑋)
1513, 2, 14syl2anc 691 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝑋)
16 txomap.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
171, 16syl 17 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐾 ∈ (TopOn‘𝑌))
18 toponss 20544 . . . . . . . . . 10 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑦𝐾) → 𝑦𝑌)
1917, 5, 18syl2anc 691 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝑌)
20 xpss12 5148 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
2115, 19, 20syl2anc 691 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
22 simprl 790 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑧 ∈ (𝑥 × 𝑦))
23 fnfvima 6400 . . . . . . . 8 ((𝐻 Fn (𝑋 × 𝑌) ∧ (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑥 × 𝑦)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
2411, 21, 22, 23syl3anc 1318 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
25 simp-4r 803 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) = 𝑐)
26 txomap.f . . . . . . . . 9 (𝜑𝐹:𝑋𝑍)
27 ffn 5958 . . . . . . . . 9 (𝐹:𝑋𝑍𝐹 Fn 𝑋)
281, 26, 273syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐹 Fn 𝑋)
29 txomap.g . . . . . . . . 9 (𝜑𝐺:𝑌𝑇)
30 ffn 5958 . . . . . . . . 9 (𝐺:𝑌𝑇𝐺 Fn 𝑌)
311, 29, 303syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐺 Fn 𝑌)
328, 28, 31, 15, 19fimaproj 29228 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) = ((𝐹𝑥) × (𝐺𝑦)))
3324, 25, 323eltr3d 2702 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)))
34 imass2 5420 . . . . . . . 8 ((𝑥 × 𝑦) ⊆ 𝐴 → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3534ad2antll 761 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3632, 35eqsstr3d 3603 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))
37 xpeq1 5052 . . . . . . . . 9 (𝑎 = (𝐹𝑥) → (𝑎 × 𝑏) = ((𝐹𝑥) × 𝑏))
3837eleq2d 2673 . . . . . . . 8 (𝑎 = (𝐹𝑥) → (𝑐 ∈ (𝑎 × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × 𝑏)))
3937sseq1d 3595 . . . . . . . 8 (𝑎 = (𝐹𝑥) → ((𝑎 × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)))
4038, 39anbi12d 743 . . . . . . 7 (𝑎 = (𝐹𝑥) → ((𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴))))
41 xpeq2 5053 . . . . . . . . 9 (𝑏 = (𝐺𝑦) → ((𝐹𝑥) × 𝑏) = ((𝐹𝑥) × (𝐺𝑦)))
4241eleq2d 2673 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (𝑐 ∈ ((𝐹𝑥) × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦))))
4341sseq1d 3595 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴)))
4442, 43anbi12d 743 . . . . . . 7 (𝑏 = (𝐺𝑦) → ((𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))))
4540, 44rspc2ev 3295 . . . . . 6 (((𝐹𝑥) ∈ 𝐿 ∧ (𝐺𝑦) ∈ 𝑀 ∧ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
464, 7, 33, 36, 45syl112anc 1322 . . . . 5 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
47 txomap.a . . . . . . . . 9 (𝜑𝐴 ∈ (𝐽 ×t 𝐾))
48 eltx 21181 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
4912, 16, 48syl2anc 691 . . . . . . . . 9 (𝜑 → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
5047, 49mpbid 221 . . . . . . . 8 (𝜑 → ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5150r19.21bi 2916 . . . . . . 7 ((𝜑𝑧𝐴) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5251adantlr 747 . . . . . 6 (((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5352adantr 480 . . . . 5 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5446, 53r19.29vva 3062 . . . 4 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
558mpt2fun 6660 . . . . . 6 Fun 𝐻
56 fvelima 6158 . . . . . 6 ((Fun 𝐻𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5755, 56mpan 702 . . . . 5 (𝑐 ∈ (𝐻𝐴) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5857adantl 481 . . . 4 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5954, 58r19.29a 3060 . . 3 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
6059ralrimiva 2949 . 2 (𝜑 → ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
61 txomap.l . . 3 (𝜑𝐿 ∈ (TopOn‘𝑍))
62 txomap.m . . 3 (𝜑𝑀 ∈ (TopOn‘𝑇))
63 eltx 21181 . . 3 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘𝑇)) → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6461, 62, 63syl2anc 691 . 2 (𝜑 → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6560, 64mpbird 246 1 (𝜑 → (𝐻𝐴) ∈ (𝐿 ×t 𝑀))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ⟨cop 4131   × cxp 5036   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  TopOnctopon 20518   ×t ctx 21173 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-topgen 15927  df-topon 20523  df-tx 21175 This theorem is referenced by:  qtophaus  29231
 Copyright terms: Public domain W3C validator