This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imasubclem1

Description: Lemma for imasubc . (Contributed by Zhi Wang, 6-Nov-2025)

Ref Expression
Hypotheses imasubclem1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
imasubclem1.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
Assertion imasubclem1 ( 𝜑 → ∪ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V )

Proof

Step Hyp Ref Expression
1 imasubclem1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2 imasubclem1.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
3 cnvexg ⊢ ( 𝐹 ∈ 𝑉 → ◡ 𝐹 ∈ V )
4 1 3 syl ⊢ ( 𝜑 → ◡ 𝐹 ∈ V )
5 4 imaexd ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝐴 ) ∈ V )
6 cnvexg ⊢ ( 𝐺 ∈ 𝑊 → ◡ 𝐺 ∈ V )
7 2 6 syl ⊢ ( 𝜑 → ◡ 𝐺 ∈ V )
8 7 imaexd ⊢ ( 𝜑 → ( ◡ 𝐺 “ 𝐵 ) ∈ V )
9 5 8 xpexd ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ∈ V )
10 fvex ⊢ ( 𝐻 ‘ 𝐶 ) ∈ V
11 10 imaex ⊢ ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V
12 11 rgenw ⊢ ∀ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V
13 iunexg ⊢ ( ( ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ∈ V ∧ ∀ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V ) → ∪ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V )
14 9 12 13 sylancl ⊢ ( 𝜑 → ∪ 𝑥 ∈ ( ( ◡ 𝐹 “ 𝐴 ) × ( ◡ 𝐺 “ 𝐵 ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V )