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

Metamath Proof Explorer

Theorem imasubclem2

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

Ref Expression
Hypotheses imasubclem1.f ⊢ φ → F ∈ V
imasubclem1.g ⊢ φ → G ∈ W
imasubclem2.k ⊢ K = y ∈ X , z ∈ Y ⟼ ⋃ x ∈ F -1 A × G -1 B H ⁡ C D
Assertion imasubclem2 ⊢ φ → K Fn X × Y

Proof

Step Hyp Ref Expression
1 imasubclem1.f ⊢ φ → F ∈ V
2 imasubclem1.g ⊢ φ → G ∈ W
3 imasubclem2.k ⊢ K = y ∈ X , z ∈ Y ⟼ ⋃ x ∈ F -1 A × G -1 B H ⁡ C D
4 1 2 imasubclem1 ⊢ φ → ⋃ x ∈ F -1 A × G -1 B H ⁡ C D ∈ V
5 4 adantr ⊢ φ ∧ y ∈ X ∧ z ∈ Y → ⋃ x ∈ F -1 A × G -1 B H ⁡ C D ∈ V
6 5 ralrimivva ⊢ φ → ∀ y ∈ X ∀ z ∈ Y ⋃ x ∈ F -1 A × G -1 B H ⁡ C D ∈ V
7 3 fnmpo ⊢ ∀ y ∈ X ∀ z ∈ Y ⋃ x ∈ F -1 A × G -1 B H ⁡ C D ∈ V → K Fn X × Y
8 6 7 syl ⊢ φ → K Fn X × Y