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 33795
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 787 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝜑)
2 simpllr 776 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝐽)
3 txomap.1 . . . . . . 7 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ 𝐿)
41, 2, 3syl2anc 584 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐹𝑥) ∈ 𝐿)
5 simplr 769 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝐾)
6 txomap.2 . . . . . . 7 ((𝜑𝑦𝐾) → (𝐺𝑦) ∈ 𝑀)
71, 5, 6syl2anc 584 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐺𝑦) ∈ 𝑀)
8 txomap.h . . . . . . . . 9 𝐻 = (𝑥𝑋, 𝑦𝑌 ↦ ⟨(𝐹𝑥), (𝐺𝑦)⟩)
9 opex 5475 . . . . . . . . 9 ⟨(𝐹𝑥), (𝐺𝑦)⟩ ∈ V
108, 9fnmpoi 8094 . . . . . . . 8 𝐻 Fn (𝑋 × 𝑌)
11 txomap.j . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
1211ad6antr 736 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐽 ∈ (TopOn‘𝑋))
13 toponss 22949 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥𝐽) → 𝑥𝑋)
1412, 2, 13syl2anc 584 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑥𝑋)
15 txomap.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (TopOn‘𝑌))
1615ad6antr 736 . . . . . . . . . 10 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐾 ∈ (TopOn‘𝑌))
17 toponss 22949 . . . . . . . . . 10 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑦𝐾) → 𝑦𝑌)
1816, 5, 17syl2anc 584 . . . . . . . . 9 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑦𝑌)
19 xpss12 5704 . . . . . . . . 9 ((𝑥𝑋𝑦𝑌) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
2014, 18, 19syl2anc 584 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
21 simprl 771 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑧 ∈ (𝑥 × 𝑦))
22 fnfvima 7253 . . . . . . . 8 ((𝐻 Fn (𝑋 × 𝑌) ∧ (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌) ∧ 𝑧 ∈ (𝑥 × 𝑦)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
2310, 20, 21, 22mp3an2i 1465 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) ∈ (𝐻 “ (𝑥 × 𝑦)))
24 simp-4r 784 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻𝑧) = 𝑐)
25 txomap.f . . . . . . . . 9 (𝜑𝐹:𝑋𝑍)
26 ffn 6737 . . . . . . . . 9 (𝐹:𝑋𝑍𝐹 Fn 𝑋)
271, 25, 263syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐹 Fn 𝑋)
28 txomap.g . . . . . . . . 9 (𝜑𝐺:𝑌𝑇)
29 ffn 6737 . . . . . . . . 9 (𝐺:𝑌𝑇𝐺 Fn 𝑌)
301, 28, 293syl 18 . . . . . . . 8 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝐺 Fn 𝑌)
318, 27, 30, 14, 18fimaproj 8159 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) = ((𝐹𝑥) × (𝐺𝑦)))
3223, 24, 313eltr3d 2853 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)))
33 imass2 6123 . . . . . . . 8 ((𝑥 × 𝑦) ⊆ 𝐴 → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3433ad2antll 729 . . . . . . 7 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → (𝐻 “ (𝑥 × 𝑦)) ⊆ (𝐻𝐴))
3531, 34eqsstrrd 4035 . . . . . 6 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))
36 xpeq1 5703 . . . . . . . . 9 (𝑎 = (𝐹𝑥) → (𝑎 × 𝑏) = ((𝐹𝑥) × 𝑏))
3736eleq2d 2825 . . . . . . . 8 (𝑎 = (𝐹𝑥) → (𝑐 ∈ (𝑎 × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × 𝑏)))
3836sseq1d 4027 . . . . . . . 8 (𝑎 = (𝐹𝑥) → ((𝑎 × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)))
3937, 38anbi12d 632 . . . . . . 7 (𝑎 = (𝐹𝑥) → ((𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴))))
40 xpeq2 5710 . . . . . . . . 9 (𝑏 = (𝐺𝑦) → ((𝐹𝑥) × 𝑏) = ((𝐹𝑥) × (𝐺𝑦)))
4140eleq2d 2825 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (𝑐 ∈ ((𝐹𝑥) × 𝑏) ↔ 𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦))))
4240sseq1d 4027 . . . . . . . 8 (𝑏 = (𝐺𝑦) → (((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴) ↔ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴)))
4341, 42anbi12d 632 . . . . . . 7 (𝑏 = (𝐺𝑦) → ((𝑐 ∈ ((𝐹𝑥) × 𝑏) ∧ ((𝐹𝑥) × 𝑏) ⊆ (𝐻𝐴)) ↔ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))))
4439, 43rspc2ev 3635 . . . . . 6 (((𝐹𝑥) ∈ 𝐿 ∧ (𝐺𝑦) ∈ 𝑀 ∧ (𝑐 ∈ ((𝐹𝑥) × (𝐺𝑦)) ∧ ((𝐹𝑥) × (𝐺𝑦)) ⊆ (𝐻𝐴))) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
454, 7, 32, 35, 44syl112anc 1373 . . . . 5 (((((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) ∧ 𝑥𝐽) ∧ 𝑦𝐾) ∧ (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
46 txomap.a . . . . . . . 8 (𝜑𝐴 ∈ (𝐽 ×t 𝐾))
47 eltx 23592 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
4811, 15, 47syl2anc 584 . . . . . . . 8 (𝜑 → (𝐴 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴)))
4946, 48mpbid 232 . . . . . . 7 (𝜑 → ∀𝑧𝐴𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5049r19.21bi 3249 . . . . . 6 ((𝜑𝑧𝐴) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5150ad4ant13 751 . . . . 5 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑥𝐽𝑦𝐾 (𝑧 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝐴))
5245, 51r19.29vva 3214 . . . 4 ((((𝜑𝑐 ∈ (𝐻𝐴)) ∧ 𝑧𝐴) ∧ (𝐻𝑧) = 𝑐) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
538mpofun 7557 . . . . . 6 Fun 𝐻
54 fvelima 6974 . . . . . 6 ((Fun 𝐻𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5553, 54mpan 690 . . . . 5 (𝑐 ∈ (𝐻𝐴) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5655adantl 481 . . . 4 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑧𝐴 (𝐻𝑧) = 𝑐)
5752, 56r19.29a 3160 . . 3 ((𝜑𝑐 ∈ (𝐻𝐴)) → ∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
5857ralrimiva 3144 . 2 (𝜑 → ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴)))
59 txomap.l . . 3 (𝜑𝐿 ∈ (TopOn‘𝑍))
60 txomap.m . . 3 (𝜑𝑀 ∈ (TopOn‘𝑇))
61 eltx 23592 . . 3 ((𝐿 ∈ (TopOn‘𝑍) ∧ 𝑀 ∈ (TopOn‘𝑇)) → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6259, 60, 61syl2anc 584 . 2 (𝜑 → ((𝐻𝐴) ∈ (𝐿 ×t 𝑀) ↔ ∀𝑐 ∈ (𝐻𝐴)∃𝑎𝐿𝑏𝑀 (𝑐 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐻𝐴))))
6358, 62mpbird 257 1 (𝜑 → (𝐻𝐴) ∈ (𝐿 ×t 𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wral 3059  wrex 3068  wss 3963  cop 4637   × cxp 5687  cima 5692  Fun wfun 6557   Fn wfn 6558  wf 6559  cfv 6563  (class class class)co 7431  cmpo 7433  TopOnctopon 22932   ×t ctx 23584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-topgen 17490  df-topon 22933  df-tx 23586
This theorem is referenced by:  qtophaus  33797
  Copyright terms: Public domain W3C validator