Metamath Proof Explorer

Theorem txomap

Description: Given two open maps F and G , H mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019)

Ref Expression
Hypotheses 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 txomap ( 𝜑 → ( 𝐻 “ 𝐴 ) ∈ ( 𝐿 ×t 𝑀 ) )

Proof

Step Hyp Ref Expression
1 txomap.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑍 )
2 txomap.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑇 )
3 txomap.j ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 txomap.k ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
5 txomap.l ⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
6 txomap.m ⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ 𝑇 ) )
7 txomap.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐿 )
8 txomap.2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐺 “ 𝑦 ) ∈ 𝑀 )
9 txomap.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐽 ×t 𝐾 ) )
10 txomap.h ⊢ 𝐻 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ )
11 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝜑 )
12 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑥 ∈ 𝐽 )
13 11 12 7 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐹 “ 𝑥 ) ∈ 𝐿 )
14 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑦 ∈ 𝐾 )
15 11 14 8 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐺 “ 𝑦 ) ∈ 𝑀 )
16 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ∈ V
17 10 16 fnmpoi ⊢ 𝐻 Fn ( 𝑋 × 𝑌 )
18 3 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
19 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 )
20 18 12 19 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑥 ⊆ 𝑋 )
21 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
22 toponss ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑦 ∈ 𝐾 ) → 𝑦 ⊆ 𝑌 )
23 21 14 22 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑦 ⊆ 𝑌 )
24 xpss12 ⊢ ( ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) → ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) )
25 20 23 24 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) )
26 simprl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑧 ∈ ( 𝑥 × 𝑦 ) )
27 fnfvima ⊢ ( ( 𝐻 Fn ( 𝑋 × 𝑌 ) ∧ ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ( 𝑥 × 𝑦 ) ) → ( 𝐻 ‘ 𝑧 ) ∈ ( 𝐻 “ ( 𝑥 × 𝑦 ) ) )
28 17 25 26 27 mp3an2i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐻 ‘ 𝑧 ) ∈ ( 𝐻 “ ( 𝑥 × 𝑦 ) ) )
29 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐻 ‘ 𝑧 ) = 𝑐 )
30 ffn ⊢ ( 𝐹 : 𝑋 ⟶ 𝑍 → 𝐹 Fn 𝑋 )
31 11 1 30 3syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝐹 Fn 𝑋 )
32 ffn ⊢ ( 𝐺 : 𝑌 ⟶ 𝑇 → 𝐺 Fn 𝑌 )
33 11 2 32 3syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝐺 Fn 𝑌 )
34 10 31 33 20 23 fimaproj ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐻 “ ( 𝑥 × 𝑦 ) ) = ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) )
35 28 29 34 3eltr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → 𝑐 ∈ ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) )
36 imass2 ⊢ ( ( 𝑥 × 𝑦 ) ⊆ 𝐴 → ( 𝐻 “ ( 𝑥 × 𝑦 ) ) ⊆ ( 𝐻 “ 𝐴 ) )
37 36 ad2antll ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( 𝐻 “ ( 𝑥 × 𝑦 ) ) ⊆ ( 𝐻 “ 𝐴 ) )
38 34 37 eqsstrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) ⊆ ( 𝐻 “ 𝐴 ) )
39 xpeq1 ⊢ ( 𝑎 = ( 𝐹 “ 𝑥 ) → ( 𝑎 × 𝑏 ) = ( ( 𝐹 “ 𝑥 ) × 𝑏 ) )
40 39 eleq2d ⊢ ( 𝑎 = ( 𝐹 “ 𝑥 ) → ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ↔ 𝑐 ∈ ( ( 𝐹 “ 𝑥 ) × 𝑏 ) ) )
41 39 sseq1d ⊢ ( 𝑎 = ( 𝐹 “ 𝑥 ) → ( ( 𝑎 × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ↔ ( ( 𝐹 “ 𝑥 ) × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) )
42 40 41 anbi12d ⊢ ( 𝑎 = ( 𝐹 “ 𝑥 ) → ( ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) ↔ ( 𝑐 ∈ ( ( 𝐹 “ 𝑥 ) × 𝑏 ) ∧ ( ( 𝐹 “ 𝑥 ) × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) ) )
43 xpeq2 ⊢ ( 𝑏 = ( 𝐺 “ 𝑦 ) → ( ( 𝐹 “ 𝑥 ) × 𝑏 ) = ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) )
44 43 eleq2d ⊢ ( 𝑏 = ( 𝐺 “ 𝑦 ) → ( 𝑐 ∈ ( ( 𝐹 “ 𝑥 ) × 𝑏 ) ↔ 𝑐 ∈ ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) ) )
45 43 sseq1d ⊢ ( 𝑏 = ( 𝐺 “ 𝑦 ) → ( ( ( 𝐹 “ 𝑥 ) × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ↔ ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) ⊆ ( 𝐻 “ 𝐴 ) ) )
46 44 45 anbi12d ⊢ ( 𝑏 = ( 𝐺 “ 𝑦 ) → ( ( 𝑐 ∈ ( ( 𝐹 “ 𝑥 ) × 𝑏 ) ∧ ( ( 𝐹 “ 𝑥 ) × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) ↔ ( 𝑐 ∈ ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) ∧ ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) ⊆ ( 𝐻 “ 𝐴 ) ) ) )
47 42 46 rspc2ev ⊢ ( ( ( 𝐹 “ 𝑥 ) ∈ 𝐿 ∧ ( 𝐺 “ 𝑦 ) ∈ 𝑀 ∧ ( 𝑐 ∈ ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) ∧ ( ( 𝐹 “ 𝑥 ) × ( 𝐺 “ 𝑦 ) ) ⊆ ( 𝐻 “ 𝐴 ) ) ) → ∃ 𝑎 ∈ 𝐿 ∃ 𝑏 ∈ 𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) )
48 13 15 35 38 47 syl112anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) → ∃ 𝑎 ∈ 𝐿 ∃ 𝑏 ∈ 𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) )
49 eltx ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐴 ∈ ( 𝐽 ×t 𝐾 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) )
50 3 4 49 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐽 ×t 𝐾 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) ) )
51 9 50 mpbid ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) )
52 51 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) )
53 52 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐾 ( 𝑧 ∈ ( 𝑥 × 𝑦 ) ∧ ( 𝑥 × 𝑦 ) ⊆ 𝐴 ) )
54 48 53 r19.29vva ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝑧 ) = 𝑐 ) → ∃ 𝑎 ∈ 𝐿 ∃ 𝑏 ∈ 𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) )
55 10 mpofun ⊢ Fun 𝐻
56 fvelima ⊢ ( ( Fun 𝐻 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) → ∃ 𝑧 ∈ 𝐴 ( 𝐻 ‘ 𝑧 ) = 𝑐 )
57 55 56 mpan ⊢ ( 𝑐 ∈ ( 𝐻 “ 𝐴 ) → ∃ 𝑧 ∈ 𝐴 ( 𝐻 ‘ 𝑧 ) = 𝑐 )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) → ∃ 𝑧 ∈ 𝐴 ( 𝐻 ‘ 𝑧 ) = 𝑐 )
59 54 58 r19.29a ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ) → ∃ 𝑎 ∈ 𝐿 ∃ 𝑏 ∈ 𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) )
60 59 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ∃ 𝑎 ∈ 𝐿 ∃ 𝑏 ∈ 𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) )
61 eltx ⊢ ( ( 𝐿 ∈ ( TopOn ‘ 𝑍 ) ∧ 𝑀 ∈ ( TopOn ‘ 𝑇 ) ) → ( ( 𝐻 “ 𝐴 ) ∈ ( 𝐿 ×t 𝑀 ) ↔ ∀ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ∃ 𝑎 ∈ 𝐿 ∃ 𝑏 ∈ 𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) ) )
62 5 6 61 syl2anc ⊢ ( 𝜑 → ( ( 𝐻 “ 𝐴 ) ∈ ( 𝐿 ×t 𝑀 ) ↔ ∀ 𝑐 ∈ ( 𝐻 “ 𝐴 ) ∃ 𝑎 ∈ 𝐿 ∃ 𝑏 ∈ 𝑀 ( 𝑐 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐻 “ 𝐴 ) ) ) )
63 60 62 mpbird ⊢ ( 𝜑 → ( 𝐻 “ 𝐴 ) ∈ ( 𝐿 ×t 𝑀 ) )