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 29701
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 798 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝐽)
3 txomap.1 . . . . . . 7 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ 𝐿)
41, 2, 3syl2anc 692 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐹𝑥) ∈ 𝐿)
5 simplr 791 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝐾)
6 txomap.2 . . . . . . 7 ((𝜑𝑦𝐾) → (𝐺𝑦) ∈ 𝑀)
71, 5, 6syl2anc 692 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐺𝑦) ∈ 𝑀)
8 txomap.h . . . . . . . . . 10 𝐻 = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
9 opex 4898 . . . . . . . . . 10 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V
108, 9fnmpt2i 7191 . . . . . . . . 9 𝐻 Fn (𝑋 × 𝑌)
1110a1i 11 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐻 Fn (𝑋 × 𝑌))
12 txomap.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
131, 12syl 17 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
14 toponss 20649 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥𝐽) → 𝑥𝑋)
1513, 2, 14syl2anc 692 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝑋)
16 txomap.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
171, 16syl 17 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐾 ∈ (TopOn‘𝑌))
18 toponss 20649 . . . . . . . . . 10 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑦𝐾) → 𝑦𝑌)
1917, 5, 18syl2anc 692 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝑌)
20 xpss12 5191 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
2115, 19, 20syl2anc 692 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
22 simprl 793 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑧 ∈ (𝑥 × 𝑦))
23 fnfvima 6456 . . . . . . . 8 ((𝐻 Fn (𝑋 × 𝑌) ∧ (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑥 × 𝑦)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
2411, 21, 22, 23syl3anc 1323 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
25 simp-4r 806 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) = 𝑐)
26 txomap.f . . . . . . . . 9 (𝜑𝐹:𝑋𝑍)
27 ffn 6007 . . . . . . . . 9 (𝐹:𝑋𝑍𝐹 Fn 𝑋)
281, 26, 273syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐹 Fn 𝑋)
29 txomap.g . . . . . . . . 9 (𝜑𝐺:𝑌𝑇)
30 ffn 6007 . . . . . . . . 9 (𝐺:𝑌𝑇𝐺 Fn 𝑌)
311, 29, 303syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐺 Fn 𝑌)
328, 28, 31, 15, 19fimaproj 29700 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) = ((𝐹𝑥) × (𝐺𝑦)))
3324, 25, 323eltr3d 2712 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)))
34 imass2 5465 . . . . . . . 8 ((𝑥 × 𝑦) ⊆ 𝐴 → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3534ad2antll 764 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3632, 35eqsstr3d 3624 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))
37 xpeq1 5093 . . . . . . . . 9 (𝑎 = (𝐹𝑥) → (𝑎 × 𝑏) = ((𝐹𝑥) × 𝑏))
3837eleq2d 2684 . . . . . . . 8 (𝑎 = (𝐹𝑥) → (𝑐 ∈ (𝑎 × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × 𝑏)))
3937sseq1d 3616 . . . . . . . 8 (𝑎 = (𝐹𝑥) → ((𝑎 × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)))
4038, 39anbi12d 746 . . . . . . 7 (𝑎 = (𝐹𝑥) → ((𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴))))
41 xpeq2 5094 . . . . . . . . 9 (𝑏 = (𝐺𝑦) → ((𝐹𝑥) × 𝑏) = ((𝐹𝑥) × (𝐺𝑦)))
4241eleq2d 2684 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (𝑐 ∈ ((𝐹𝑥) × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦))))
4341sseq1d 3616 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴)))
4442, 43anbi12d 746 . . . . . . 7 (𝑏 = (𝐺𝑦) → ((𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))))
4540, 44rspc2ev 3312 . . . . . 6 (((𝐹𝑥) ∈ 𝐿 ∧ (𝐺𝑦) ∈ 𝑀 ∧ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
464, 7, 33, 36, 45syl112anc 1327 . . . . 5 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
47 txomap.a . . . . . . . . 9 (𝜑𝐴 ∈ (𝐽 ×t 𝐾))
48 eltx 21290 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
4912, 16, 48syl2anc 692 . . . . . . . . 9 (𝜑 → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
5047, 49mpbid 222 . . . . . . . 8 (𝜑 → ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5150r19.21bi 2927 . . . . . . 7 ((𝜑𝑧𝐴) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5251adantlr 750 . . . . . 6 (((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5352adantr 481 . . . . 5 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5446, 53r19.29vva 3074 . . . 4 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
558mpt2fun 6722 . . . . . 6 Fun 𝐻
56 fvelima 6210 . . . . . 6 ((Fun 𝐻𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5755, 56mpan 705 . . . . 5 (𝑐 ∈ (𝐻𝐴) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5857adantl 482 . . . 4 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5954, 58r19.29a 3072 . . 3 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
6059ralrimiva 2961 . 2 (𝜑 → ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
61 txomap.l . . 3 (𝜑𝐿 ∈ (TopOn‘𝑍))
62 txomap.m . . 3 (𝜑𝑀 ∈ (TopOn‘𝑇))
63 eltx 21290 . . 3 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘𝑇)) → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6461, 62, 63syl2anc 692 . 2 (𝜑 → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6560, 64mpbird 247 1 (𝜑 → (𝐻𝐴) ∈ (𝐿 ×t 𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  wrex 2908  wss 3559  cop 4159   × cxp 5077  cima 5082  Fun wfun 5846   Fn wfn 5847  wf 5848  cfv 5852  (class class class)co 6610  cmpt2 6612  TopOnctopon 20643   ×t ctx 21282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-1st 7120  df-2nd 7121  df-topgen 16032  df-topon 20644  df-tx 21284
This theorem is referenced by:  qtophaus  29703
  Copyright terms: Public domain W3C validator