Metamath Proof Explorer

Theorem sexp2

Description: Condition for the relationship in frxp2 to be set-like. (Contributed by Scott Fenton, 19-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 xpord2.1 
 |-  T = { <. x , y >. | ( x e. ( A X. B ) /\ y e. ( A X. B ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) S ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
2 sexp2.1 
 |-  ( ph -> R Se A )
3 sexp2.2 
 |-  ( ph -> S Se B )
4 elxp2 
 |-  ( p e. ( A X. B ) <-> E. a e. A E. b e. B p = <. a , b >. )
5 1 xpord2pred 
 |-  ( ( a e. A /\ b e. B ) -> Pred ( T , ( A X. B ) , <. a , b >. ) = ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) )
6 5 adantl 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> Pred ( T , ( A X. B ) , <. a , b >. ) = ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) )
7 setlikespec 
 |-  ( ( a e. A /\ R Se A ) -> Pred ( R , A , a ) e. _V )
8 7 ancoms 
 |-  ( ( R Se A /\ a e. A ) -> Pred ( R , A , a ) e. _V )
9 2 8 sylan 
 |-  ( ( ph /\ a e. A ) -> Pred ( R , A , a ) e. _V )
10 9 adantrr 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> Pred ( R , A , a ) e. _V )
11 snex 
 |-  { a } e. _V
12 11 a1i 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> { a } e. _V )
13 10 12 unexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> ( Pred ( R , A , a ) u. { a } ) e. _V )
14 setlikespec 
 |-  ( ( b e. B /\ S Se B ) -> Pred ( S , B , b ) e. _V )
15 14 ancoms 
 |-  ( ( S Se B /\ b e. B ) -> Pred ( S , B , b ) e. _V )
16 3 15 sylan 
 |-  ( ( ph /\ b e. B ) -> Pred ( S , B , b ) e. _V )
17 16 adantrl 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> Pred ( S , B , b ) e. _V )
18 snex 
 |-  { b } e. _V
19 18 a1i 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> { b } e. _V )
20 17 19 unexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> ( Pred ( S , B , b ) u. { b } ) e. _V )
21 13 20 xpexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) e. _V )
22 21 difexd 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) e. _V )
23 6 22 eqeltrd 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> Pred ( T , ( A X. B ) , <. a , b >. ) e. _V )
24 predeq3 
 |-  ( p = <. a , b >. -> Pred ( T , ( A X. B ) , p ) = Pred ( T , ( A X. B ) , <. a , b >. ) )
25 24 eleq1d 
 |-  ( p = <. a , b >. -> ( Pred ( T , ( A X. B ) , p ) e. _V <-> Pred ( T , ( A X. B ) , <. a , b >. ) e. _V ) )
26 23 25 syl5ibrcom 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> ( p = <. a , b >. -> Pred ( T , ( A X. B ) , p ) e. _V ) )
27 26 rexlimdvva 
 |-  ( ph -> ( E. a e. A E. b e. B p = <. a , b >. -> Pred ( T , ( A X. B ) , p ) e. _V ) )
28 4 27 syl5bi 
 |-  ( ph -> ( p e. ( A X. B ) -> Pred ( T , ( A X. B ) , p ) e. _V ) )
29 28 ralrimiv 
 |-  ( ph -> A. p e. ( A X. B ) Pred ( T , ( A X. B ) , p ) e. _V )
30 dfse3 
 |-  ( T Se ( A X. B ) <-> A. p e. ( A X. B ) Pred ( T , ( A X. B ) , p ) e. _V )
31 29 30 sylibr 
 |-  ( ph -> T Se ( A X. B ) )