Metamath Proof Explorer

Theorem imasubc3lem2

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

Ref Expression
Hypotheses imasubc3lem1.s 
|- S = ( F " A )
imasubc3lem1.f 
|- ( ph -> F : B -1-1-> C )
imasubc3lem1.x 
|- ( ph -> X e. S )
imasubc3lem2.y 
|- ( ph -> Y e. S )
imasubc3lem2.f 
|- ( ph -> F e. V )
imasubc3lem2.k 
|- K = ( x e. S , y e. S |-> U_ p e. ( ( `' F " { x } ) X. ( `' F " { y } ) ) ( ( G ` p ) " ( H ` p ) ) )
Assertion imasubc3lem2 
|- ( ph -> ( X K Y ) = ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 imasubc3lem1.s 
 |-  S = ( F " A )
2 imasubc3lem1.f 
 |-  ( ph -> F : B -1-1-> C )
3 imasubc3lem1.x 
 |-  ( ph -> X e. S )
4 imasubc3lem2.y 
 |-  ( ph -> Y e. S )
5 imasubc3lem2.f 
 |-  ( ph -> F e. V )
6 imasubc3lem2.k 
 |-  K = ( x e. S , y e. S |-> U_ p e. ( ( `' F " { x } ) X. ( `' F " { y } ) ) ( ( G ` p ) " ( H ` p ) ) )
7 5 5 3 4 6 imasubclem3 
 |-  ( ph -> ( X K Y ) = U_ p e. ( ( `' F " { X } ) X. ( `' F " { Y } ) ) ( ( G ` p ) " ( H ` p ) ) )
8 1 2 3 imasubc3lem1 
 |-  ( ph -> ( { ( `' F ` X ) } = ( `' F " { X } ) /\ ( F ` ( `' F ` X ) ) = X /\ ( `' F ` X ) e. B ) )
9 8 simp1d 
 |-  ( ph -> { ( `' F ` X ) } = ( `' F " { X } ) )
10 1 2 4 imasubc3lem1 
 |-  ( ph -> ( { ( `' F ` Y ) } = ( `' F " { Y } ) /\ ( F ` ( `' F ` Y ) ) = Y /\ ( `' F ` Y ) e. B ) )
11 10 simp1d 
 |-  ( ph -> { ( `' F ` Y ) } = ( `' F " { Y } ) )
12 9 11 xpeq12d 
 |-  ( ph -> ( { ( `' F ` X ) } X. { ( `' F ` Y ) } ) = ( ( `' F " { X } ) X. ( `' F " { Y } ) ) )
13 fvex 
 |-  ( `' F ` X ) e. _V
14 fvex 
 |-  ( `' F ` Y ) e. _V
15 13 14 xpsn 
 |-  ( { ( `' F ` X ) } X. { ( `' F ` Y ) } ) = { <. ( `' F ` X ) , ( `' F ` Y ) >. }
16 12 15 eqtr3di 
 |-  ( ph -> ( ( `' F " { X } ) X. ( `' F " { Y } ) ) = { <. ( `' F ` X ) , ( `' F ` Y ) >. } )
17 16 iuneq1d 
 |-  ( ph -> U_ p e. ( ( `' F " { X } ) X. ( `' F " { Y } ) ) ( ( G ` p ) " ( H ` p ) ) = U_ p e. { <. ( `' F ` X ) , ( `' F ` Y ) >. } ( ( G ` p ) " ( H ` p ) ) )
18 7 17 eqtrd 
 |-  ( ph -> ( X K Y ) = U_ p e. { <. ( `' F ` X ) , ( `' F ` Y ) >. } ( ( G ` p ) " ( H ` p ) ) )
19 opex 
 |-  <. ( `' F ` X ) , ( `' F ` Y ) >. e. _V
20 fveq2 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( G ` p ) = ( G ` <. ( `' F ` X ) , ( `' F ` Y ) >. ) )
21 df-ov 
 |-  ( ( `' F ` X ) G ( `' F ` Y ) ) = ( G ` <. ( `' F ` X ) , ( `' F ` Y ) >. )
22 20 21 eqtr4di 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( G ` p ) = ( ( `' F ` X ) G ( `' F ` Y ) ) )
23 fveq2 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( H ` p ) = ( H ` <. ( `' F ` X ) , ( `' F ` Y ) >. ) )
24 df-ov 
 |-  ( ( `' F ` X ) H ( `' F ` Y ) ) = ( H ` <. ( `' F ` X ) , ( `' F ` Y ) >. )
25 23 24 eqtr4di 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( H ` p ) = ( ( `' F ` X ) H ( `' F ` Y ) ) )
26 22 25 imaeq12d 
 |-  ( p = <. ( `' F ` X ) , ( `' F ` Y ) >. -> ( ( G ` p ) " ( H ` p ) ) = ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) ) )
27 19 26 iunxsn 
 |-  U_ p e. { <. ( `' F ` X ) , ( `' F ` Y ) >. } ( ( G ` p ) " ( H ` p ) ) = ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) )
28 18 27 eqtrdi 
 |-  ( ph -> ( X K Y ) = ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) ) )