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 ⊢ φ → F ∈ V
imasubclem1.g ⊢ φ → G ∈ W
imasubclem3.x ⊢ φ → X ∈ A
imasubclem3.y ⊢ φ → Y ∈ B
imasubclem3.k ⊢ K = x ∈ A , y ∈ B ⟼ ⋃ z ∈ F -1 x × G -1 y H ⁡ C D
Assertion imasubclem3 ⊢ φ → X K Y = ⋃ z ∈ F -1 X × G -1 Y H ⁡ C D

Proof

Step Hyp Ref Expression
1 imasubclem1.f ⊢ φ → F ∈ V
2 imasubclem1.g ⊢ φ → G ∈ W
3 imasubclem3.x ⊢ φ → X ∈ A
4 imasubclem3.y ⊢ φ → Y ∈ B
5 imasubclem3.k ⊢ K = x ∈ A , y ∈ B ⟼ ⋃ z ∈ F -1 x × G -1 y H ⁡ C D
6 1 2 imasubclem1 ⊢ φ → ⋃ z ∈ F -1 X × G -1 Y H ⁡ C D ∈ V
7 simpl ⊢ x = X ∧ y = Y → x = X
8 7 sneqd ⊢ x = X ∧ y = Y → x = X
9 8 imaeq2d ⊢ x = X ∧ y = Y → F -1 x = F -1 X
10 simpr ⊢ x = X ∧ y = Y → y = Y
11 10 sneqd ⊢ x = X ∧ y = Y → y = Y
12 11 imaeq2d ⊢ x = X ∧ y = Y → G -1 y = G -1 Y
13 9 12 xpeq12d ⊢ x = X ∧ y = Y → F -1 x × G -1 y = F -1 X × G -1 Y
14 13 iuneq1d ⊢ x = X ∧ y = Y → ⋃ z ∈ F -1 x × G -1 y H ⁡ C D = ⋃ z ∈ F -1 X × G -1 Y H ⁡ C D
15 14 5 ovmpoga ⊢ X ∈ A ∧ Y ∈ B ∧ ⋃ z ∈ F -1 X × G -1 Y H ⁡ C D ∈ V → X K Y = ⋃ z ∈ F -1 X × G -1 Y H ⁡ C D
16 3 4 6 15 syl3anc ⊢ φ → X K Y = ⋃ z ∈ F -1 X × G -1 Y H ⁡ C D