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

Metamath Proof Explorer

Theorem imasubclem1

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

Ref Expression
Hypotheses imasubclem1.f 
|- ( ph -> F e. V )
imasubclem1.g 
|- ( ph -> G e. W )
Assertion imasubclem1 
|- ( ph -> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V )

Proof

Step Hyp Ref Expression
1 imasubclem1.f 
 |-  ( ph -> F e. V )
2 imasubclem1.g 
 |-  ( ph -> G e. W )
3 cnvexg 
 |-  ( F e. V -> `' F e. _V )
4 1 3 syl 
 |-  ( ph -> `' F e. _V )
5 4 imaexd 
 |-  ( ph -> ( `' F " A ) e. _V )
6 cnvexg 
 |-  ( G e. W -> `' G e. _V )
7 2 6 syl 
 |-  ( ph -> `' G e. _V )
8 7 imaexd 
 |-  ( ph -> ( `' G " B ) e. _V )
9 5 8 xpexd 
 |-  ( ph -> ( ( `' F " A ) X. ( `' G " B ) ) e. _V )
10 fvex 
 |-  ( H ` C ) e. _V
11 10 imaex 
 |-  ( ( H ` C ) " D ) e. _V
12 11 rgenw 
 |-  A. x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V
13 iunexg 
 |-  ( ( ( ( `' F " A ) X. ( `' G " B ) ) e. _V /\ A. x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V ) -> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V )
14 9 12 13 sylancl 
 |-  ( ph -> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V )