Metamath Proof Explorer

Theorem imasubclem1

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

Ref Expression
Hypotheses imasubclem1.f ⊢ φ → F ∈ V
imasubclem1.g ⊢ φ → G ∈ W
Assertion imasubclem1 ⊢ φ → ⋃ x ∈ F -1 A × G -1 B H ⁡ C D ∈ V

Proof

Step Hyp Ref Expression
1 imasubclem1.f ⊢ φ → F ∈ V
2 imasubclem1.g ⊢ φ → G ∈ W
3 cnvexg ⊢ F ∈ V → F -1 ∈ V
4 1 3 syl ⊢ φ → F -1 ∈ V
5 4 imaexd ⊢ φ → F -1 A ∈ V
6 cnvexg ⊢ G ∈ W → G -1 ∈ V
7 2 6 syl ⊢ φ → G -1 ∈ V
8 7 imaexd ⊢ φ → G -1 B ∈ V
9 5 8 xpexd ⊢ φ → F -1 A × G -1 B ∈ V
10 fvex ⊢ H ⁡ C ∈ V
11 10 imaex ⊢ H ⁡ C D ∈ V
12 11 rgenw ⊢ ∀ x ∈ F -1 A × G -1 B H ⁡ C D ∈ V
13 iunexg ⊢ F -1 A × G -1 B ∈ V ∧ ∀ x ∈ F -1 A × G -1 B H ⁡ C D ∈ V → ⋃ x ∈ F -1 A × G -1 B H ⁡ C D ∈ V
14 9 12 13 sylancl ⊢ φ → ⋃ x ∈ F -1 A × G -1 B H ⁡ C D ∈ V