Metamath Proof Explorer

Theorem bj-imdirco

Description: Functorial property of the direct image: the direct image by a composition is the composition of the direct images. (Contributed by BJ, 23-May-2024)

Ref Expression
Hypotheses bj-imdirco.exa 
|- ( ph -> A e. U )
bj-imdirco.exb 
|- ( ph -> B e. V )
bj-imdirco.exc 
|- ( ph -> C e. W )
bj-imdirco.arg1 
|- ( ph -> R C_ ( A X. B ) )
bj-imdirco.arg2 
|- ( ph -> S C_ ( B X. C ) )
Assertion bj-imdirco 
|- ( ph -> ( ( A ~P_* C ) ` ( S o. R ) ) = ( ( ( B ~P_* C ) ` S ) o. ( ( A ~P_* B ) ` R ) ) )

Proof

Step Hyp Ref Expression
1 bj-imdirco.exa 
 |-  ( ph -> A e. U )
2 bj-imdirco.exb 
 |-  ( ph -> B e. V )
3 bj-imdirco.exc 
 |-  ( ph -> C e. W )
4 bj-imdirco.arg1 
 |-  ( ph -> R C_ ( A X. B ) )
5 bj-imdirco.arg2 
 |-  ( ph -> S C_ ( B X. C ) )
6 imaco 
 |-  ( ( S o. R ) " x ) = ( S " ( R " x ) )
7 6 eqeq1i 
 |-  ( ( ( S o. R ) " x ) = z <-> ( S " ( R " x ) ) = z )
8 7 anbi2i 
 |-  ( ( ( x C_ A /\ z C_ C ) /\ ( ( S o. R ) " x ) = z ) <-> ( ( x C_ A /\ z C_ C ) /\ ( S " ( R " x ) ) = z ) )
9 8 a1i 
 |-  ( ph -> ( ( ( x C_ A /\ z C_ C ) /\ ( ( S o. R ) " x ) = z ) <-> ( ( x C_ A /\ z C_ C ) /\ ( S " ( R " x ) ) = z ) ) )
10 1 2 xpexd 
 |-  ( ph -> ( A X. B ) e. _V )
11 10 4 ssexd 
 |-  ( ph -> R e. _V )
12 imaexg 
 |-  ( R e. _V -> ( R " x ) e. _V )
13 11 12 syl 
 |-  ( ph -> ( R " x ) e. _V )
14 imass1 
 |-  ( R C_ ( A X. B ) -> ( R " x ) C_ ( ( A X. B ) " x ) )
15 xpima 
 |-  ( ( A X. B ) " x ) = if ( ( A i^i x ) = (/) , (/) , B )
16 simpr 
 |-  ( ( ( A i^i x ) = (/) /\ u e. (/) ) -> u e. (/) )
17 simpr 
 |-  ( ( -. ( A i^i x ) = (/) /\ u e. B ) -> u e. B )
18 16 17 orim12i 
 |-  ( ( ( ( A i^i x ) = (/) /\ u e. (/) ) \/ ( -. ( A i^i x ) = (/) /\ u e. B ) ) -> ( u e. (/) \/ u e. B ) )
19 elif 
 |-  ( u e. if ( ( A i^i x ) = (/) , (/) , B ) <-> ( ( ( A i^i x ) = (/) /\ u e. (/) ) \/ ( -. ( A i^i x ) = (/) /\ u e. B ) ) )
20 elun 
 |-  ( u e. ( (/) u. B ) <-> ( u e. (/) \/ u e. B ) )
21 18 19 20 3imtr4i 
 |-  ( u e. if ( ( A i^i x ) = (/) , (/) , B ) -> u e. ( (/) u. B ) )
22 21 ssriv 
 |-  if ( ( A i^i x ) = (/) , (/) , B ) C_ ( (/) u. B )
23 0ss 
 |-  (/) C_ B
24 ssid 
 |-  B C_ B
25 23 24 unssi 
 |-  ( (/) u. B ) C_ B
26 22 25 sstri 
 |-  if ( ( A i^i x ) = (/) , (/) , B ) C_ B
27 15 26 eqsstri 
 |-  ( ( A X. B ) " x ) C_ B
28 14 27 sstrdi 
 |-  ( R C_ ( A X. B ) -> ( R " x ) C_ B )
29 4 28 syl 
 |-  ( ph -> ( R " x ) C_ B )
30 eqidd 
 |-  ( ph -> ( R " x ) = ( R " x ) )
31 29 30 jca 
 |-  ( ph -> ( ( R " x ) C_ B /\ ( R " x ) = ( R " x ) ) )
32 sseq1 
 |-  ( y = ( R " x ) -> ( y C_ B <-> ( R " x ) C_ B ) )
33 eqeq2 
 |-  ( y = ( R " x ) -> ( ( R " x ) = y <-> ( R " x ) = ( R " x ) ) )
34 32 33 anbi12d 
 |-  ( y = ( R " x ) -> ( ( y C_ B /\ ( R " x ) = y ) <-> ( ( R " x ) C_ B /\ ( R " x ) = ( R " x ) ) ) )
35 13 31 34 spcedv 
 |-  ( ph -> E. y ( y C_ B /\ ( R " x ) = y ) )
36 35 biantrurd 
 |-  ( ph -> ( ( S " ( R " x ) ) = z <-> ( E. y ( y C_ B /\ ( R " x ) = y ) /\ ( S " ( R " x ) ) = z ) ) )
37 19.41v 
 |-  ( E. y ( ( y C_ B /\ ( R " x ) = y ) /\ ( S " ( R " x ) ) = z ) <-> ( E. y ( y C_ B /\ ( R " x ) = y ) /\ ( S " ( R " x ) ) = z ) )
38 anass 
 |-  ( ( ( y C_ B /\ ( R " x ) = y ) /\ ( S " ( R " x ) ) = z ) <-> ( y C_ B /\ ( ( R " x ) = y /\ ( S " ( R " x ) ) = z ) ) )
39 38 exbii 
 |-  ( E. y ( ( y C_ B /\ ( R " x ) = y ) /\ ( S " ( R " x ) ) = z ) <-> E. y ( y C_ B /\ ( ( R " x ) = y /\ ( S " ( R " x ) ) = z ) ) )
40 37 39 bitr3i 
 |-  ( ( E. y ( y C_ B /\ ( R " x ) = y ) /\ ( S " ( R " x ) ) = z ) <-> E. y ( y C_ B /\ ( ( R " x ) = y /\ ( S " ( R " x ) ) = z ) ) )
41 36 40 bitrdi 
 |-  ( ph -> ( ( S " ( R " x ) ) = z <-> E. y ( y C_ B /\ ( ( R " x ) = y /\ ( S " ( R " x ) ) = z ) ) ) )
42 imaeq2 
 |-  ( ( R " x ) = y -> ( S " ( R " x ) ) = ( S " y ) )
43 42 eqeq1d 
 |-  ( ( R " x ) = y -> ( ( S " ( R " x ) ) = z <-> ( S " y ) = z ) )
44 43 pm5.32i 
 |-  ( ( ( R " x ) = y /\ ( S " ( R " x ) ) = z ) <-> ( ( R " x ) = y /\ ( S " y ) = z ) )
45 44 bianass 
 |-  ( ( y C_ B /\ ( ( R " x ) = y /\ ( S " ( R " x ) ) = z ) ) <-> ( ( y C_ B /\ ( R " x ) = y ) /\ ( S " y ) = z ) )
46 45 biancomi 
 |-  ( ( y C_ B /\ ( ( R " x ) = y /\ ( S " ( R " x ) ) = z ) ) <-> ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) )
47 46 exbii 
 |-  ( E. y ( y C_ B /\ ( ( R " x ) = y /\ ( S " ( R " x ) ) = z ) ) <-> E. y ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) )
48 47 a1i 
 |-  ( ph -> ( E. y ( y C_ B /\ ( ( R " x ) = y /\ ( S " ( R " x ) ) = z ) ) <-> E. y ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) )
49 pm4.24 
 |-  ( y C_ B <-> ( y C_ B /\ y C_ B ) )
50 49 anbi1i 
 |-  ( ( y C_ B /\ ( R " x ) = y ) <-> ( ( y C_ B /\ y C_ B ) /\ ( R " x ) = y ) )
51 anass 
 |-  ( ( ( y C_ B /\ y C_ B ) /\ ( R " x ) = y ) <-> ( y C_ B /\ ( y C_ B /\ ( R " x ) = y ) ) )
52 50 51 bitri 
 |-  ( ( y C_ B /\ ( R " x ) = y ) <-> ( y C_ B /\ ( y C_ B /\ ( R " x ) = y ) ) )
53 52 anbi2i 
 |-  ( ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) <-> ( ( S " y ) = z /\ ( y C_ B /\ ( y C_ B /\ ( R " x ) = y ) ) ) )
54 an12 
 |-  ( ( ( S " y ) = z /\ ( y C_ B /\ ( y C_ B /\ ( R " x ) = y ) ) ) <-> ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) )
55 53 54 bitri 
 |-  ( ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) <-> ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) )
56 55 exbii 
 |-  ( E. y ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) <-> E. y ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) )
57 56 a1i 
 |-  ( ph -> ( E. y ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) <-> E. y ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) )
58 41 48 57 3bitrd 
 |-  ( ph -> ( ( S " ( R " x ) ) = z <-> E. y ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) )
59 58 anbi2d 
 |-  ( ph -> ( ( ( x C_ A /\ z C_ C ) /\ ( S " ( R " x ) ) = z ) <-> ( ( x C_ A /\ z C_ C ) /\ E. y ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) ) )
60 19.42v 
 |-  ( E. y ( ( x C_ A /\ z C_ C ) /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> ( ( x C_ A /\ z C_ C ) /\ E. y ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) )
61 anass 
 |-  ( ( ( x C_ A /\ z C_ C ) /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> ( x C_ A /\ ( z C_ C /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) ) )
62 ancom 
 |-  ( ( ( ( R " x ) = y /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) /\ y C_ B ) <-> ( y C_ B /\ ( ( R " x ) = y /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) ) )
63 62 bianass 
 |-  ( ( x C_ A /\ ( ( ( R " x ) = y /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) /\ y C_ B ) ) <-> ( ( x C_ A /\ y C_ B ) /\ ( ( R " x ) = y /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) ) )
64 ancom 
 |-  ( ( ( ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) /\ y C_ B ) /\ ( R " x ) = y ) <-> ( ( R " x ) = y /\ ( ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) /\ y C_ B ) ) )
65 ancom 
 |-  ( ( z C_ C /\ y C_ B ) <-> ( y C_ B /\ z C_ C ) )
66 65 anbi1i 
 |-  ( ( ( z C_ C /\ y C_ B ) /\ ( S " y ) = z ) <-> ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) )
67 66 anbi1i 
 |-  ( ( ( ( z C_ C /\ y C_ B ) /\ ( S " y ) = z ) /\ ( y C_ B /\ ( R " x ) = y ) ) <-> ( ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) /\ ( y C_ B /\ ( R " x ) = y ) ) )
68 biid 
 |-  ( ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) <-> ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) )
69 68 bianass 
 |-  ( ( z C_ C /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> ( ( z C_ C /\ y C_ B ) /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) )
70 anass 
 |-  ( ( ( ( z C_ C /\ y C_ B ) /\ ( S " y ) = z ) /\ ( y C_ B /\ ( R " x ) = y ) ) <-> ( ( z C_ C /\ y C_ B ) /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) )
71 69 70 bitr4i 
 |-  ( ( z C_ C /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> ( ( ( z C_ C /\ y C_ B ) /\ ( S " y ) = z ) /\ ( y C_ B /\ ( R " x ) = y ) ) )
72 anass 
 |-  ( ( ( ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) /\ y C_ B ) /\ ( R " x ) = y ) <-> ( ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) /\ ( y C_ B /\ ( R " x ) = y ) ) )
73 67 71 72 3bitr4i 
 |-  ( ( z C_ C /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> ( ( ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) /\ y C_ B ) /\ ( R " x ) = y ) )
74 anass 
 |-  ( ( ( ( R " x ) = y /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) /\ y C_ B ) <-> ( ( R " x ) = y /\ ( ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) /\ y C_ B ) ) )
75 64 73 74 3bitr4i 
 |-  ( ( z C_ C /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> ( ( ( R " x ) = y /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) /\ y C_ B ) )
76 75 anbi2i 
 |-  ( ( x C_ A /\ ( z C_ C /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) ) <-> ( x C_ A /\ ( ( ( R " x ) = y /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) /\ y C_ B ) ) )
77 anass 
 |-  ( ( ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) <-> ( ( x C_ A /\ y C_ B ) /\ ( ( R " x ) = y /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) ) )
78 63 76 77 3bitr4i 
 |-  ( ( x C_ A /\ ( z C_ C /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) ) <-> ( ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) )
79 61 78 bitri 
 |-  ( ( ( x C_ A /\ z C_ C ) /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> ( ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) )
80 79 exbii 
 |-  ( E. y ( ( x C_ A /\ z C_ C ) /\ ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> E. y ( ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) )
81 60 80 bitr3i 
 |-  ( ( ( x C_ A /\ z C_ C ) /\ E. y ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> E. y ( ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) )
82 81 a1i 
 |-  ( ph -> ( ( ( x C_ A /\ z C_ C ) /\ E. y ( y C_ B /\ ( ( S " y ) = z /\ ( y C_ B /\ ( R " x ) = y ) ) ) ) <-> E. y ( ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) ) )
83 9 59 82 3bitrd 
 |-  ( ph -> ( ( ( x C_ A /\ z C_ C ) /\ ( ( S o. R ) " x ) = z ) <-> E. y ( ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) ) )
84 83 opabbidv 
 |-  ( ph -> { <. x , z >. | ( ( x C_ A /\ z C_ C ) /\ ( ( S o. R ) " x ) = z ) } = { <. x , z >. | E. y ( ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) } )
85 bj-opabco 
 |-  ( { <. y , z >. | ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) } o. { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } ) = { <. x , z >. | E. y ( ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) /\ ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) ) }
86 84 85 eqtr4di 
 |-  ( ph -> { <. x , z >. | ( ( x C_ A /\ z C_ C ) /\ ( ( S o. R ) " x ) = z ) } = ( { <. y , z >. | ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) } o. { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } ) )
87 5 4 coss12d 
 |-  ( ph -> ( S o. R ) C_ ( ( B X. C ) o. ( A X. B ) ) )
88 bj-xpcossxp 
 |-  ( ( B X. C ) o. ( A X. B ) ) C_ ( A X. C )
89 87 88 sstrdi 
 |-  ( ph -> ( S o. R ) C_ ( A X. C ) )
90 1 3 89 bj-imdirval2 
 |-  ( ph -> ( ( A ~P_* C ) ` ( S o. R ) ) = { <. x , z >. | ( ( x C_ A /\ z C_ C ) /\ ( ( S o. R ) " x ) = z ) } )
91 2 3 5 bj-imdirval2 
 |-  ( ph -> ( ( B ~P_* C ) ` S ) = { <. y , z >. | ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) } )
92 1 2 4 bj-imdirval2 
 |-  ( ph -> ( ( A ~P_* B ) ` R ) = { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } )
93 91 92 coeq12d 
 |-  ( ph -> ( ( ( B ~P_* C ) ` S ) o. ( ( A ~P_* B ) ` R ) ) = ( { <. y , z >. | ( ( y C_ B /\ z C_ C ) /\ ( S " y ) = z ) } o. { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ( R " x ) = y ) } ) )
94 86 90 93 3eqtr4d 
 |-  ( ph -> ( ( A ~P_* C ) ` ( S o. R ) ) = ( ( ( B ~P_* C ) ` S ) o. ( ( A ~P_* B ) ` R ) ) )