Metamath Proof Explorer

Theorem noxpordpred

Description: Next we calculate the predecessor class of the relationship. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses noxpord.1 
|- R = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) }
noxpord.2 
|- S = { <. x , y >. | ( x e. ( No X. No ) /\ y e. ( No X. No ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) R ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
Assertion noxpordpred 
|- ( ( A e. No /\ B e. No ) -> Pred ( S , ( No X. No ) , <. A , B >. ) = ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) )

Proof

Step Hyp Ref Expression
1 noxpord.1 
 |-  R = { <. a , b >. | a e. ( ( _L ` b ) u. ( _R ` b ) ) }
2 noxpord.2 
 |-  S = { <. x , y >. | ( x e. ( No X. No ) /\ y e. ( No X. No ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) R ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
3 2 xpord2pred 
 |-  ( ( A e. No /\ B e. No ) -> Pred ( S , ( No X. No ) , <. A , B >. ) = ( ( ( Pred ( R , No , A ) u. { A } ) X. ( Pred ( R , No , B ) u. { B } ) ) \ { <. A , B >. } ) )
4 1 lrrecpred 
 |-  ( A e. No -> Pred ( R , No , A ) = ( ( _L ` A ) u. ( _R ` A ) ) )
5 4 adantr 
 |-  ( ( A e. No /\ B e. No ) -> Pred ( R , No , A ) = ( ( _L ` A ) u. ( _R ` A ) ) )
6 5 uneq1d 
 |-  ( ( A e. No /\ B e. No ) -> ( Pred ( R , No , A ) u. { A } ) = ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) )
7 1 lrrecpred 
 |-  ( B e. No -> Pred ( R , No , B ) = ( ( _L ` B ) u. ( _R ` B ) ) )
8 7 adantl 
 |-  ( ( A e. No /\ B e. No ) -> Pred ( R , No , B ) = ( ( _L ` B ) u. ( _R ` B ) ) )
9 8 uneq1d 
 |-  ( ( A e. No /\ B e. No ) -> ( Pred ( R , No , B ) u. { B } ) = ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) )
10 6 9 xpeq12d 
 |-  ( ( A e. No /\ B e. No ) -> ( ( Pred ( R , No , A ) u. { A } ) X. ( Pred ( R , No , B ) u. { B } ) ) = ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) )
11 10 difeq1d 
 |-  ( ( A e. No /\ B e. No ) -> ( ( ( Pred ( R , No , A ) u. { A } ) X. ( Pred ( R , No , B ) u. { B } ) ) \ { <. A , B >. } ) = ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) )
12 3 11 eqtrd 
 |-  ( ( A e. No /\ B e. No ) -> Pred ( S , ( No X. No ) , <. A , B >. ) = ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) )