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 )