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 𝑀 ) ) |