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 30348
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 809 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝜑)
2 simpllr 793 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝐽)
3 txomap.1 . . . . . . 7 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ 𝐿)
41, 2, 3syl2anc 579 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐹𝑥) ∈ 𝐿)
5 simplr 785 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝐾)
6 txomap.2 . . . . . . 7 ((𝜑𝑦𝐾) → (𝐺𝑦) ∈ 𝑀)
71, 5, 6syl2anc 579 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐺𝑦) ∈ 𝑀)
8 txomap.h . . . . . . . . . 10 𝐻 = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
9 opex 5088 . . . . . . . . . 10 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V
108, 9fnmpt2i 7440 . . . . . . . . 9 𝐻 Fn (𝑋 × 𝑌)
1110a1i 11 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐻 Fn (𝑋 × 𝑌))
12 txomap.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
131, 12syl 17 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
14 toponss 21011 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥𝐽) → 𝑥𝑋)
1513, 2, 14syl2anc 579 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝑋)
16 txomap.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
171, 16syl 17 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐾 ∈ (TopOn‘𝑌))
18 toponss 21011 . . . . . . . . . 10 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑦𝐾) → 𝑦𝑌)
1917, 5, 18syl2anc 579 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝑌)
20 xpss12 5292 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
2115, 19, 20syl2anc 579 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
22 simprl 787 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑧 ∈ (𝑥 × 𝑦))
23 fnfvima 6689 . . . . . . . 8 ((𝐻 Fn (𝑋 × 𝑌) ∧ (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑥 × 𝑦)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
2411, 21, 22, 23syl3anc 1490 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
25 simp-4r 803 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) = 𝑐)
26 txomap.f . . . . . . . . 9 (𝜑𝐹:𝑋𝑍)
27 ffn 6223 . . . . . . . . 9 (𝐹:𝑋𝑍𝐹 Fn 𝑋)
281, 26, 273syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐹 Fn 𝑋)
29 txomap.g . . . . . . . . 9 (𝜑𝐺:𝑌𝑇)
30 ffn 6223 . . . . . . . . 9 (𝐺:𝑌𝑇𝐺 Fn 𝑌)
311, 29, 303syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐺 Fn 𝑌)
328, 28, 31, 15, 19fimaproj 30347 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) = ((𝐹𝑥) × (𝐺𝑦)))
3324, 25, 323eltr3d 2858 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)))
34 imass2 5683 . . . . . . . 8 ((𝑥 × 𝑦) ⊆ 𝐴 → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3534ad2antll 720 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3632, 35eqsstr3d 3800 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))
37 xpeq1 5291 . . . . . . . . 9 (𝑎 = (𝐹𝑥) → (𝑎 × 𝑏) = ((𝐹𝑥) × 𝑏))
3837eleq2d 2830 . . . . . . . 8 (𝑎 = (𝐹𝑥) → (𝑐 ∈ (𝑎 × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × 𝑏)))
3937sseq1d 3792 . . . . . . . 8 (𝑎 = (𝐹𝑥) → ((𝑎 × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)))
4038, 39anbi12d 624 . . . . . . 7 (𝑎 = (𝐹𝑥) → ((𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴))))
41 xpeq2 5298 . . . . . . . . 9 (𝑏 = (𝐺𝑦) → ((𝐹𝑥) × 𝑏) = ((𝐹𝑥) × (𝐺𝑦)))
4241eleq2d 2830 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (𝑐 ∈ ((𝐹𝑥) × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦))))
4341sseq1d 3792 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴)))
4442, 43anbi12d 624 . . . . . . 7 (𝑏 = (𝐺𝑦) → ((𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))))
4540, 44rspc2ev 3476 . . . . . 6 (((𝐹𝑥) ∈ 𝐿 ∧ (𝐺𝑦) ∈ 𝑀 ∧ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
464, 7, 33, 36, 45syl112anc 1493 . . . . 5 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
47 txomap.a . . . . . . . . 9 (𝜑𝐴 ∈ (𝐽 ×t 𝐾))
48 eltx 21651 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
4912, 16, 48syl2anc 579 . . . . . . . . 9 (𝜑 → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
5047, 49mpbid 223 . . . . . . . 8 (𝜑 → ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5150r19.21bi 3079 . . . . . . 7 ((𝜑𝑧𝐴) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5251adantlr 706 . . . . . 6 (((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5352adantr 472 . . . . 5 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5446, 53r19.29vva 3228 . . . 4 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
558mpt2fun 6960 . . . . . 6 Fun 𝐻
56 fvelima 6437 . . . . . 6 ((Fun 𝐻𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5755, 56mpan 681 . . . . 5 (𝑐 ∈ (𝐻𝐴) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5857adantl 473 . . . 4 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5954, 58r19.29a 3225 . . 3 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
6059ralrimiva 3113 . 2 (𝜑 → ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
61 txomap.l . . 3 (𝜑𝐿 ∈ (TopOn‘𝑍))
62 txomap.m . . 3 (𝜑𝑀 ∈ (TopOn‘𝑇))
63 eltx 21651 . . 3 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘𝑇)) → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6461, 62, 63syl2anc 579 . 2 (𝜑 → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6560, 64mpbird 248 1 (𝜑 → (𝐻𝐴) ∈ (𝐿 ×t 𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  wrex 3056  wss 3732  cop 4340   × cxp 5275  cima 5280  Fun wfun 6062   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  cmpt2 6844  TopOnctopon 20994   ×t ctx 21643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-1st 7366  df-2nd 7367  df-topgen 16370  df-topon 20995  df-tx 21645
This theorem is referenced by:  qtophaus  30350
  Copyright terms: Public domain W3C validator