Metamath Proof Explorer

Theorem bj-opabco

Description: Composition of ordered-pair class abstractions. (Contributed by BJ, 22-May-2024)

Ref Expression
Assertion bj-opabco 
|- ( { <. y , z >. | ps } o. { <. x , y >. | ph } ) = { <. x , z >. | E. y ( ph /\ ps ) }

Proof

Step Hyp Ref Expression
1 df-co 
 |-  ( { <. y , z >. | ps } o. { <. x , y >. | ph } ) = { <. a , b >. | E. c ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b ) }
2 nfcv 
 |-  F/_ x a
3 nfopab1 
 |-  F/_ x { <. x , y >. | ph }
4 nfcv 
 |-  F/_ x c
5 2 3 4 nfbr 
 |-  F/ x a { <. x , y >. | ph } c
6 nfv 
 |-  F/ x c { <. y , z >. | ps } b
7 5 6 nfan 
 |-  F/ x ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b )
8 7 nfex 
 |-  F/ x E. c ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b )
9 nfv 
 |-  F/ z a { <. x , y >. | ph } c
10 nfcv 
 |-  F/_ z c
11 nfopab2 
 |-  F/_ z { <. y , z >. | ps }
12 nfcv 
 |-  F/_ z b
13 10 11 12 nfbr 
 |-  F/ z c { <. y , z >. | ps } b
14 9 13 nfan 
 |-  F/ z ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b )
15 14 nfex 
 |-  F/ z E. c ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b )
16 nfv 
 |-  F/ a E. y ( x { <. x , y >. | ph } y /\ y { <. y , z >. | ps } z )
17 nfv 
 |-  F/ b E. y ( x { <. x , y >. | ph } y /\ y { <. y , z >. | ps } z )
18 nfv 
 |-  F/ y ( a = x /\ b = z )
19 nfcv 
 |-  F/_ y a
20 nfopab2 
 |-  F/_ y { <. x , y >. | ph }
21 nfcv 
 |-  F/_ y c
22 19 20 21 nfbr 
 |-  F/ y a { <. x , y >. | ph } c
23 nfopab1 
 |-  F/_ y { <. y , z >. | ps }
24 nfcv 
 |-  F/_ y b
25 21 23 24 nfbr 
 |-  F/ y c { <. y , z >. | ps } b
26 22 25 nfan 
 |-  F/ y ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b )
27 26 a1i 
 |-  ( ( a = x /\ b = z ) -> F/ y ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b ) )
28 simpll 
 |-  ( ( ( a = x /\ b = z ) /\ c = y ) -> a = x )
29 simpr 
 |-  ( ( ( a = x /\ b = z ) /\ c = y ) -> c = y )
30 28 29 breq12d 
 |-  ( ( ( a = x /\ b = z ) /\ c = y ) -> ( a { <. x , y >. | ph } c <-> x { <. x , y >. | ph } y ) )
31 simplr 
 |-  ( ( ( a = x /\ b = z ) /\ c = y ) -> b = z )
32 29 31 breq12d 
 |-  ( ( ( a = x /\ b = z ) /\ c = y ) -> ( c { <. y , z >. | ps } b <-> y { <. y , z >. | ps } z ) )
33 30 32 anbi12d 
 |-  ( ( ( a = x /\ b = z ) /\ c = y ) -> ( ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b ) <-> ( x { <. x , y >. | ph } y /\ y { <. y , z >. | ps } z ) ) )
34 33 ex 
 |-  ( ( a = x /\ b = z ) -> ( c = y -> ( ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b ) <-> ( x { <. x , y >. | ph } y /\ y { <. y , z >. | ps } z ) ) ) )
35 18 27 34 cbvexdw 
 |-  ( ( a = x /\ b = z ) -> ( E. c ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b ) <-> E. y ( x { <. x , y >. | ph } y /\ y { <. y , z >. | ps } z ) ) )
36 8 15 16 17 35 cbvopab 
 |-  { <. a , b >. | E. c ( a { <. x , y >. | ph } c /\ c { <. y , z >. | ps } b ) } = { <. x , z >. | E. y ( x { <. x , y >. | ph } y /\ y { <. y , z >. | ps } z ) }
37 bj-opelopabid 
 |-  ( x { <. x , y >. | ph } y <-> ph )
38 bj-opelopabid 
 |-  ( y { <. y , z >. | ps } z <-> ps )
39 37 38 anbi12i 
 |-  ( ( x { <. x , y >. | ph } y /\ y { <. y , z >. | ps } z ) <-> ( ph /\ ps ) )
40 39 exbii 
 |-  ( E. y ( x { <. x , y >. | ph } y /\ y { <. y , z >. | ps } z ) <-> E. y ( ph /\ ps ) )
41 40 opabbii 
 |-  { <. x , z >. | E. y ( x { <. x , y >. | ph } y /\ y { <. y , z >. | ps } z ) } = { <. x , z >. | E. y ( ph /\ ps ) }
42 1 36 41 3eqtri 
 |-  ( { <. y , z >. | ps } o. { <. x , y >. | ph } ) = { <. x , z >. | E. y ( ph /\ ps ) }