Theorem imasubclem3

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

	Ref	Expression
Hypotheses	imasubclem1.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	imasubclem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	imasubclem3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	imasubclem3.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	imasubclem3.k	⊢ 𝐾 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐺 “ { 𝑦 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) )
Assertion	imasubclem3	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐺 “ { 𝑌 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		imasubclem1.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		imasubclem1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
3		imasubclem3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4		imasubclem3.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5		imasubclem3.k	⊢ 𝐾 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐺 “ { 𝑦 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) )
6	1 2	imasubclem1	⊢ ( 𝜑 → ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐺 “ { 𝑌 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V )
7		simpl	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑥 = 𝑋 )
8	7	sneqd	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 𝑥 } = { 𝑋 } )
9	8	imaeq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ◡ 𝐹 “ { 𝑥 } ) = ( ◡ 𝐹 “ { 𝑋 } ) )
10		simpr	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
11	10	sneqd	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 𝑦 } = { 𝑌 } )
12	11	imaeq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ◡ 𝐺 “ { 𝑦 } ) = ( ◡ 𝐺 “ { 𝑌 } ) )
13	9 12	xpeq12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐺 “ { 𝑦 } ) ) = ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐺 “ { 𝑌 } ) ) )
14	13	iuneq1d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐺 “ { 𝑦 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) = ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐺 “ { 𝑌 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) )
15	14 5	ovmpoga	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐺 “ { 𝑌 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) ∈ V ) → ( 𝑋 𝐾 𝑌 ) = ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐺 “ { 𝑌 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) )
16	3 4 6 15	syl3anc	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐺 “ { 𝑌 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) )