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 32455
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 786 . . . . . . 7 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ πœ‘)
2 simpllr 775 . . . . . . 7 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ π‘₯ ∈ 𝐽)
3 txomap.1 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ 𝐽) β†’ (𝐹 β€œ π‘₯) ∈ 𝐿)
41, 2, 3syl2anc 585 . . . . . 6 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ (𝐹 β€œ π‘₯) ∈ 𝐿)
5 simplr 768 . . . . . . 7 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ 𝑦 ∈ 𝐾)
6 txomap.2 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ 𝐾) β†’ (𝐺 β€œ 𝑦) ∈ 𝑀)
71, 5, 6syl2anc 585 . . . . . 6 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ (𝐺 β€œ 𝑦) ∈ 𝑀)
8 txomap.h . . . . . . . . 9 𝐻 = (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩)
9 opex 5426 . . . . . . . . 9 ⟨(πΉβ€˜π‘₯), (πΊβ€˜π‘¦)⟩ ∈ V
108, 9fnmpoi 8007 . . . . . . . 8 𝐻 Fn (𝑋 Γ— π‘Œ)
11 txomap.j . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
1211ad6antr 735 . . . . . . . . . 10 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
13 toponss 22292 . . . . . . . . . 10 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ π‘₯ ∈ 𝐽) β†’ π‘₯ βŠ† 𝑋)
1412, 2, 13syl2anc 585 . . . . . . . . 9 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ π‘₯ βŠ† 𝑋)
15 txomap.k . . . . . . . . . . 11 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
1615ad6antr 735 . . . . . . . . . 10 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))
17 toponss 22292 . . . . . . . . . 10 ((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝑦 ∈ 𝐾) β†’ 𝑦 βŠ† π‘Œ)
1816, 5, 17syl2anc 585 . . . . . . . . 9 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ 𝑦 βŠ† π‘Œ)
19 xpss12 5653 . . . . . . . . 9 ((π‘₯ βŠ† 𝑋 ∧ 𝑦 βŠ† π‘Œ) β†’ (π‘₯ Γ— 𝑦) βŠ† (𝑋 Γ— π‘Œ))
2014, 18, 19syl2anc 585 . . . . . . . 8 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ (π‘₯ Γ— 𝑦) βŠ† (𝑋 Γ— π‘Œ))
21 simprl 770 . . . . . . . 8 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ 𝑧 ∈ (π‘₯ Γ— 𝑦))
22 fnfvima 7188 . . . . . . . 8 ((𝐻 Fn (𝑋 Γ— π‘Œ) ∧ (π‘₯ Γ— 𝑦) βŠ† (𝑋 Γ— π‘Œ) ∧ 𝑧 ∈ (π‘₯ Γ— 𝑦)) β†’ (π»β€˜π‘§) ∈ (𝐻 β€œ (π‘₯ Γ— 𝑦)))
2310, 20, 21, 22mp3an2i 1467 . . . . . . 7 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ (π»β€˜π‘§) ∈ (𝐻 β€œ (π‘₯ Γ— 𝑦)))
24 simp-4r 783 . . . . . . 7 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ (π»β€˜π‘§) = 𝑐)
25 txomap.f . . . . . . . . 9 (πœ‘ β†’ 𝐹:π‘‹βŸΆπ‘)
26 ffn 6673 . . . . . . . . 9 (𝐹:π‘‹βŸΆπ‘ β†’ 𝐹 Fn 𝑋)
271, 25, 263syl 18 . . . . . . . 8 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ 𝐹 Fn 𝑋)
28 txomap.g . . . . . . . . 9 (πœ‘ β†’ 𝐺:π‘ŒβŸΆπ‘‡)
29 ffn 6673 . . . . . . . . 9 (𝐺:π‘ŒβŸΆπ‘‡ β†’ 𝐺 Fn π‘Œ)
301, 28, 293syl 18 . . . . . . . 8 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ 𝐺 Fn π‘Œ)
318, 27, 30, 14, 18fimaproj 8072 . . . . . . 7 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ (𝐻 β€œ (π‘₯ Γ— 𝑦)) = ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦)))
3223, 24, 313eltr3d 2852 . . . . . 6 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ 𝑐 ∈ ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦)))
33 imass2 6059 . . . . . . . 8 ((π‘₯ Γ— 𝑦) βŠ† 𝐴 β†’ (𝐻 β€œ (π‘₯ Γ— 𝑦)) βŠ† (𝐻 β€œ 𝐴))
3433ad2antll 728 . . . . . . 7 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ (𝐻 β€œ (π‘₯ Γ— 𝑦)) βŠ† (𝐻 β€œ 𝐴))
3531, 34eqsstrrd 3988 . . . . . 6 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦)) βŠ† (𝐻 β€œ 𝐴))
36 xpeq1 5652 . . . . . . . . 9 (π‘Ž = (𝐹 β€œ π‘₯) β†’ (π‘Ž Γ— 𝑏) = ((𝐹 β€œ π‘₯) Γ— 𝑏))
3736eleq2d 2824 . . . . . . . 8 (π‘Ž = (𝐹 β€œ π‘₯) β†’ (𝑐 ∈ (π‘Ž Γ— 𝑏) ↔ 𝑐 ∈ ((𝐹 β€œ π‘₯) Γ— 𝑏)))
3836sseq1d 3980 . . . . . . . 8 (π‘Ž = (𝐹 β€œ π‘₯) β†’ ((π‘Ž Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴) ↔ ((𝐹 β€œ π‘₯) Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴)))
3937, 38anbi12d 632 . . . . . . 7 (π‘Ž = (𝐹 β€œ π‘₯) β†’ ((𝑐 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴)) ↔ (𝑐 ∈ ((𝐹 β€œ π‘₯) Γ— 𝑏) ∧ ((𝐹 β€œ π‘₯) Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴))))
40 xpeq2 5659 . . . . . . . . 9 (𝑏 = (𝐺 β€œ 𝑦) β†’ ((𝐹 β€œ π‘₯) Γ— 𝑏) = ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦)))
4140eleq2d 2824 . . . . . . . 8 (𝑏 = (𝐺 β€œ 𝑦) β†’ (𝑐 ∈ ((𝐹 β€œ π‘₯) Γ— 𝑏) ↔ 𝑐 ∈ ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦))))
4240sseq1d 3980 . . . . . . . 8 (𝑏 = (𝐺 β€œ 𝑦) β†’ (((𝐹 β€œ π‘₯) Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴) ↔ ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦)) βŠ† (𝐻 β€œ 𝐴)))
4341, 42anbi12d 632 . . . . . . 7 (𝑏 = (𝐺 β€œ 𝑦) β†’ ((𝑐 ∈ ((𝐹 β€œ π‘₯) Γ— 𝑏) ∧ ((𝐹 β€œ π‘₯) Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴)) ↔ (𝑐 ∈ ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦)) ∧ ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦)) βŠ† (𝐻 β€œ 𝐴))))
4439, 43rspc2ev 3595 . . . . . 6 (((𝐹 β€œ π‘₯) ∈ 𝐿 ∧ (𝐺 β€œ 𝑦) ∈ 𝑀 ∧ (𝑐 ∈ ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦)) ∧ ((𝐹 β€œ π‘₯) Γ— (𝐺 β€œ 𝑦)) βŠ† (𝐻 β€œ 𝐴))) β†’ βˆƒπ‘Ž ∈ 𝐿 βˆƒπ‘ ∈ 𝑀 (𝑐 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴)))
454, 7, 32, 35, 44syl112anc 1375 . . . . 5 (((((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) ∧ π‘₯ ∈ 𝐽) ∧ 𝑦 ∈ 𝐾) ∧ (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)) β†’ βˆƒπ‘Ž ∈ 𝐿 βˆƒπ‘ ∈ 𝑀 (𝑐 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴)))
46 txomap.a . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ (𝐽 Γ—t 𝐾))
47 eltx 22935 . . . . . . . . 9 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐴 ∈ (𝐽 Γ—t 𝐾) ↔ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘₯ ∈ 𝐽 βˆƒπ‘¦ ∈ 𝐾 (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)))
4811, 15, 47syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (𝐴 ∈ (𝐽 Γ—t 𝐾) ↔ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘₯ ∈ 𝐽 βˆƒπ‘¦ ∈ 𝐾 (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴)))
4946, 48mpbid 231 . . . . . . 7 (πœ‘ β†’ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘₯ ∈ 𝐽 βˆƒπ‘¦ ∈ 𝐾 (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴))
5049r19.21bi 3237 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝐴) β†’ βˆƒπ‘₯ ∈ 𝐽 βˆƒπ‘¦ ∈ 𝐾 (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴))
5150ad4ant13 750 . . . . 5 ((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) β†’ βˆƒπ‘₯ ∈ 𝐽 βˆƒπ‘¦ ∈ 𝐾 (𝑧 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝐴))
5245, 51r19.29vva 3208 . . . 4 ((((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) ∧ 𝑧 ∈ 𝐴) ∧ (π»β€˜π‘§) = 𝑐) β†’ βˆƒπ‘Ž ∈ 𝐿 βˆƒπ‘ ∈ 𝑀 (𝑐 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴)))
538mpofun 7485 . . . . . 6 Fun 𝐻
54 fvelima 6913 . . . . . 6 ((Fun 𝐻 ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) β†’ βˆƒπ‘§ ∈ 𝐴 (π»β€˜π‘§) = 𝑐)
5553, 54mpan 689 . . . . 5 (𝑐 ∈ (𝐻 β€œ 𝐴) β†’ βˆƒπ‘§ ∈ 𝐴 (π»β€˜π‘§) = 𝑐)
5655adantl 483 . . . 4 ((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) β†’ βˆƒπ‘§ ∈ 𝐴 (π»β€˜π‘§) = 𝑐)
5752, 56r19.29a 3160 . . 3 ((πœ‘ ∧ 𝑐 ∈ (𝐻 β€œ 𝐴)) β†’ βˆƒπ‘Ž ∈ 𝐿 βˆƒπ‘ ∈ 𝑀 (𝑐 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴)))
5857ralrimiva 3144 . 2 (πœ‘ β†’ βˆ€π‘ ∈ (𝐻 β€œ 𝐴)βˆƒπ‘Ž ∈ 𝐿 βˆƒπ‘ ∈ 𝑀 (𝑐 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴)))
59 txomap.l . . 3 (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜π‘))
60 txomap.m . . 3 (πœ‘ β†’ 𝑀 ∈ (TopOnβ€˜π‘‡))
61 eltx 22935 . . 3 ((𝐿 ∈ (TopOnβ€˜π‘) ∧ 𝑀 ∈ (TopOnβ€˜π‘‡)) β†’ ((𝐻 β€œ 𝐴) ∈ (𝐿 Γ—t 𝑀) ↔ βˆ€π‘ ∈ (𝐻 β€œ 𝐴)βˆƒπ‘Ž ∈ 𝐿 βˆƒπ‘ ∈ 𝑀 (𝑐 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴))))
6259, 60, 61syl2anc 585 . 2 (πœ‘ β†’ ((𝐻 β€œ 𝐴) ∈ (𝐿 Γ—t 𝑀) ↔ βˆ€π‘ ∈ (𝐻 β€œ 𝐴)βˆƒπ‘Ž ∈ 𝐿 βˆƒπ‘ ∈ 𝑀 (𝑐 ∈ (π‘Ž Γ— 𝑏) ∧ (π‘Ž Γ— 𝑏) βŠ† (𝐻 β€œ 𝐴))))
6358, 62mpbird 257 1 (πœ‘ β†’ (𝐻 β€œ 𝐴) ∈ (𝐿 Γ—t 𝑀))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3065  βˆƒwrex 3074   βŠ† wss 3915  βŸ¨cop 4597   Γ— cxp 5636   β€œ cima 5641  Fun wfun 6495   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ∈ cmpo 7364  TopOnctopon 22275   Γ—t ctx 22927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7926  df-2nd 7927  df-topgen 17332  df-topon 22276  df-tx 22929
This theorem is referenced by:  qtophaus  32457
  Copyright terms: Public domain W3C validator