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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ∪ 𝑧 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐺 “ { 𝑌 } ) ) ( ( 𝐻 ‘ 𝐶 ) “ 𝐷 ) )