Metamath Proof Explorer

Theorem sexp3

Description: Show that the triple order is set-like. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypotheses xpord3.1 
|- U = { <. x , y >. | ( x e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) }
sexp3.1 
|- ( ph -> R Se A )
sexp3.2 
|- ( ph -> S Se B )
sexp3.3 
|- ( ph -> T Se C )
Assertion sexp3 
|- ( ph -> U Se ( ( A X. B ) X. C ) )

Proof

Step Hyp Ref Expression
1 xpord3.1 
 |-  U = { <. x , y >. | ( x e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) }
2 sexp3.1 
 |-  ( ph -> R Se A )
3 sexp3.2 
 |-  ( ph -> S Se B )
4 sexp3.3 
 |-  ( ph -> T Se C )
5 elxpxp 
 |-  ( p e. ( ( A X. B ) X. C ) <-> E. a e. A E. b e. B E. c e. C p = <. <. a , b >. , c >. )
6 df-3an 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) <-> ( ( a e. A /\ b e. B ) /\ c e. C ) )
7 1 xpord3pred 
 |-  ( ( a e. A /\ b e. B /\ c e. C ) -> Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) = ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) )
8 7 adantl 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) = ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) )
9 simpr1 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> a e. A )
10 2 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> R Se A )
11 setlikespec 
 |-  ( ( a e. A /\ R Se A ) -> Pred ( R , A , a ) e. _V )
12 9 10 11 syl2anc 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> Pred ( R , A , a ) e. _V )
13 snex 
 |-  { a } e. _V
14 13 a1i 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> { a } e. _V )
15 12 14 unexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> ( Pred ( R , A , a ) u. { a } ) e. _V )
16 simpr2 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> b e. B )
17 3 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> S Se B )
18 setlikespec 
 |-  ( ( b e. B /\ S Se B ) -> Pred ( S , B , b ) e. _V )
19 16 17 18 syl2anc 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> Pred ( S , B , b ) e. _V )
20 snex 
 |-  { b } e. _V
21 20 a1i 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> { b } e. _V )
22 19 21 unexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> ( Pred ( S , B , b ) u. { b } ) e. _V )
23 15 22 xpexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) e. _V )
24 simpr3 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> c e. C )
25 4 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> T Se C )
26 setlikespec 
 |-  ( ( c e. C /\ T Se C ) -> Pred ( T , C , c ) e. _V )
27 24 25 26 syl2anc 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> Pred ( T , C , c ) e. _V )
28 snex 
 |-  { c } e. _V
29 28 a1i 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> { c } e. _V )
30 27 29 unexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> ( Pred ( T , C , c ) u. { c } ) e. _V )
31 23 30 xpexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) e. _V )
32 31 difexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> ( ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) X. ( Pred ( T , C , c ) u. { c } ) ) \ { <. <. a , b >. , c >. } ) e. _V )
33 8 32 eqeltrd 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) e. _V )
34 predeq3 
 |-  ( p = <. <. a , b >. , c >. -> Pred ( U , ( ( A X. B ) X. C ) , p ) = Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) )
35 34 eleq1d 
 |-  ( p = <. <. a , b >. , c >. -> ( Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V <-> Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) e. _V ) )
36 35 biimprd 
 |-  ( p = <. <. a , b >. , c >. -> ( Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) e. _V -> Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V ) )
37 36 com12 
 |-  ( Pred ( U , ( ( A X. B ) X. C ) , <. <. a , b >. , c >. ) e. _V -> ( p = <. <. a , b >. , c >. -> Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V ) )
38 33 37 syl 
 |-  ( ( ph /\ ( a e. A /\ b e. B /\ c e. C ) ) -> ( p = <. <. a , b >. , c >. -> Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V ) )
39 6 38 sylan2br 
 |-  ( ( ph /\ ( ( a e. A /\ b e. B ) /\ c e. C ) ) -> ( p = <. <. a , b >. , c >. -> Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V ) )
40 39 anassrs 
 |-  ( ( ( ph /\ ( a e. A /\ b e. B ) ) /\ c e. C ) -> ( p = <. <. a , b >. , c >. -> Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V ) )
41 40 rexlimdva 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> ( E. c e. C p = <. <. a , b >. , c >. -> Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V ) )
42 41 rexlimdvva 
 |-  ( ph -> ( E. a e. A E. b e. B E. c e. C p = <. <. a , b >. , c >. -> Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V ) )
43 5 42 syl5bi 
 |-  ( ph -> ( p e. ( ( A X. B ) X. C ) -> Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V ) )
44 43 ralrimiv 
 |-  ( ph -> A. p e. ( ( A X. B ) X. C ) Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V )
45 dfse3 
 |-  ( U Se ( ( A X. B ) X. C ) <-> A. p e. ( ( A X. B ) X. C ) Pred ( U , ( ( A X. B ) X. C ) , p ) e. _V )
46 44 45 sylibr 
 |-  ( ph -> U Se ( ( A X. B ) X. C ) )