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

Theorem txomap 30029
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 827 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝜑)
2 simpllr 815 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝐽)
3 txomap.1 . . . . . . 7 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ 𝐿)
41, 2, 3syl2anc 694 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐹𝑥) ∈ 𝐿)
5 simplr 807 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝐾)
6 txomap.2 . . . . . . 7 ((𝜑𝑦𝐾) → (𝐺𝑦) ∈ 𝑀)
71, 5, 6syl2anc 694 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐺𝑦) ∈ 𝑀)
8 txomap.h . . . . . . . . . 10 𝐻 = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
9 opex 4962 . . . . . . . . . 10 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V
108, 9fnmpt2i 7284 . . . . . . . . 9 𝐻 Fn (𝑋 × 𝑌)
1110a1i 11 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐻 Fn (𝑋 × 𝑌))
12 txomap.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
131, 12syl 17 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
14 toponss 20779 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥𝐽) → 𝑥𝑋)
1513, 2, 14syl2anc 694 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝑋)
16 txomap.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
171, 16syl 17 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐾 ∈ (TopOn‘𝑌))
18 toponss 20779 . . . . . . . . . 10 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑦𝐾) → 𝑦𝑌)
1917, 5, 18syl2anc 694 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝑌)
20 xpss12 5158 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
2115, 19, 20syl2anc 694 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
22 simprl 809 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑧 ∈ (𝑥 × 𝑦))
23 fnfvima 6536 . . . . . . . 8 ((𝐻 Fn (𝑋 × 𝑌) ∧ (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑥 × 𝑦)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
2411, 21, 22, 23syl3anc 1366 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
25 simp-4r 824 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) = 𝑐)
26 txomap.f . . . . . . . . 9 (𝜑𝐹:𝑋𝑍)
27 ffn 6083 . . . . . . . . 9 (𝐹:𝑋𝑍𝐹 Fn 𝑋)
281, 26, 273syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐹 Fn 𝑋)
29 txomap.g . . . . . . . . 9 (𝜑𝐺:𝑌𝑇)
30 ffn 6083 . . . . . . . . 9 (𝐺:𝑌𝑇𝐺 Fn 𝑌)
311, 29, 303syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐺 Fn 𝑌)
328, 28, 31, 15, 19fimaproj 30028 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) = ((𝐹𝑥) × (𝐺𝑦)))
3324, 25, 323eltr3d 2744 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)))
34 imass2 5536 . . . . . . . 8 ((𝑥 × 𝑦) ⊆ 𝐴 → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3534ad2antll 765 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3632, 35eqsstr3d 3673 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))
37 xpeq1 5157 . . . . . . . . 9 (𝑎 = (𝐹𝑥) → (𝑎 × 𝑏) = ((𝐹𝑥) × 𝑏))
3837eleq2d 2716 . . . . . . . 8 (𝑎 = (𝐹𝑥) → (𝑐 ∈ (𝑎 × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × 𝑏)))
3937sseq1d 3665 . . . . . . . 8 (𝑎 = (𝐹𝑥) → ((𝑎 × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)))
4038, 39anbi12d 747 . . . . . . 7 (𝑎 = (𝐹𝑥) → ((𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴))))
41 xpeq2 5163 . . . . . . . . 9 (𝑏 = (𝐺𝑦) → ((𝐹𝑥) × 𝑏) = ((𝐹𝑥) × (𝐺𝑦)))
4241eleq2d 2716 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (𝑐 ∈ ((𝐹𝑥) × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦))))
4341sseq1d 3665 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴)))
4442, 43anbi12d 747 . . . . . . 7 (𝑏 = (𝐺𝑦) → ((𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))))
4540, 44rspc2ev 3355 . . . . . 6 (((𝐹𝑥) ∈ 𝐿 ∧ (𝐺𝑦) ∈ 𝑀 ∧ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
464, 7, 33, 36, 45syl112anc 1370 . . . . 5 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
47 txomap.a . . . . . . . . 9 (𝜑𝐴 ∈ (𝐽 ×t 𝐾))
48 eltx 21419 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
4912, 16, 48syl2anc 694 . . . . . . . . 9 (𝜑 → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
5047, 49mpbid 222 . . . . . . . 8 (𝜑 → ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5150r19.21bi 2961 . . . . . . 7 ((𝜑𝑧𝐴) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5251adantlr 751 . . . . . 6 (((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5352adantr 480 . . . . 5 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5446, 53r19.29vva 3110 . . . 4 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
558mpt2fun 6804 . . . . . 6 Fun 𝐻
56 fvelima 6287 . . . . . 6 ((Fun 𝐻𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5755, 56mpan 706 . . . . 5 (𝑐 ∈ (𝐻𝐴) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5857adantl 481 . . . 4 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5954, 58r19.29a 3107 . . 3 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
6059ralrimiva 2995 . 2 (𝜑 → ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
61 txomap.l . . 3 (𝜑𝐿 ∈ (TopOn‘𝑍))
62 txomap.m . . 3 (𝜑𝑀 ∈ (TopOn‘𝑇))
63 eltx 21419 . . 3 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘𝑇)) → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6461, 62, 63syl2anc 694 . 2 (𝜑 → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6560, 64mpbird 247 1 (𝜑 → (𝐻𝐴) ∈ (𝐿 ×t 𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941  wrex 2942  wss 3607  cop 4216   × cxp 5141  cima 5146  Fun wfun 5920   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692  TopOnctopon 20763   ×t ctx 21411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-topgen 16151  df-topon 20764  df-tx 21413
This theorem is referenced by:  qtophaus  30031
  Copyright terms: Public domain W3C validator