Metamath Proof Explorer

Theorem xpord2pred

Description: Calculate the predecessor class in frxp2 . (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypothesis 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 ) ) }
Assertion xpord2pred 
|- ( ( X e. A /\ Y e. B ) -> Pred ( T , ( A X. B ) , <. X , Y >. ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) \ { <. X , Y >. } ) )

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 opeq1 
 |-  ( a = X -> <. a , b >. = <. X , b >. )
3 predeq3 
 |-  ( <. a , b >. = <. X , b >. -> Pred ( T , ( A X. B ) , <. a , b >. ) = Pred ( T , ( A X. B ) , <. X , b >. ) )
4 2 3 syl 
 |-  ( a = X -> Pred ( T , ( A X. B ) , <. a , b >. ) = Pred ( T , ( A X. B ) , <. X , b >. ) )
5 predeq3 
 |-  ( a = X -> Pred ( R , A , a ) = Pred ( R , A , X ) )
6 sneq 
 |-  ( a = X -> { a } = { X } )
7 5 6 uneq12d 
 |-  ( a = X -> ( Pred ( R , A , a ) u. { a } ) = ( Pred ( R , A , X ) u. { X } ) )
8 7 xpeq1d 
 |-  ( a = X -> ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) = ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) )
9 2 sneqd 
 |-  ( a = X -> { <. a , b >. } = { <. X , b >. } )
10 8 9 difeq12d 
 |-  ( a = X -> ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. X , b >. } ) )
11 4 10 eqeq12d 
 |-  ( a = X -> ( Pred ( T , ( A X. B ) , <. a , b >. ) = ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) <-> Pred ( T , ( A X. B ) , <. X , b >. ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. X , b >. } ) ) )
12 opeq2 
 |-  ( b = Y -> <. X , b >. = <. X , Y >. )
13 predeq3 
 |-  ( <. X , b >. = <. X , Y >. -> Pred ( T , ( A X. B ) , <. X , b >. ) = Pred ( T , ( A X. B ) , <. X , Y >. ) )
14 12 13 syl 
 |-  ( b = Y -> Pred ( T , ( A X. B ) , <. X , b >. ) = Pred ( T , ( A X. B ) , <. X , Y >. ) )
15 predeq3 
 |-  ( b = Y -> Pred ( S , B , b ) = Pred ( S , B , Y ) )
16 sneq 
 |-  ( b = Y -> { b } = { Y } )
17 15 16 uneq12d 
 |-  ( b = Y -> ( Pred ( S , B , b ) u. { b } ) = ( Pred ( S , B , Y ) u. { Y } ) )
18 17 xpeq2d 
 |-  ( b = Y -> ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) = ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) )
19 12 sneqd 
 |-  ( b = Y -> { <. X , b >. } = { <. X , Y >. } )
20 18 19 difeq12d 
 |-  ( b = Y -> ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. X , b >. } ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) \ { <. X , Y >. } ) )
21 14 20 eqeq12d 
 |-  ( b = Y -> ( Pred ( T , ( A X. B ) , <. X , b >. ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. X , b >. } ) <-> Pred ( T , ( A X. B ) , <. X , Y >. ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) \ { <. X , Y >. } ) ) )
22 predel 
 |-  ( e e. Pred ( T , ( A X. B ) , <. a , b >. ) -> e e. ( A X. B ) )
23 22 a1i 
 |-  ( ( a e. A /\ b e. B ) -> ( e e. Pred ( T , ( A X. B ) , <. a , b >. ) -> e e. ( A X. B ) ) )
24 eldifi 
 |-  ( e e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) -> e e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) )
25 predss 
 |-  Pred ( R , A , a ) C_ A
26 25 a1i 
 |-  ( a e. A -> Pred ( R , A , a ) C_ A )
27 snssi 
 |-  ( a e. A -> { a } C_ A )
28 26 27 unssd 
 |-  ( a e. A -> ( Pred ( R , A , a ) u. { a } ) C_ A )
29 predss 
 |-  Pred ( S , B , b ) C_ B
30 29 a1i 
 |-  ( b e. B -> Pred ( S , B , b ) C_ B )
31 snssi 
 |-  ( b e. B -> { b } C_ B )
32 30 31 unssd 
 |-  ( b e. B -> ( Pred ( S , B , b ) u. { b } ) C_ B )
33 xpss12 
 |-  ( ( ( Pred ( R , A , a ) u. { a } ) C_ A /\ ( Pred ( S , B , b ) u. { b } ) C_ B ) -> ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) C_ ( A X. B ) )
34 28 32 33 syl2an 
 |-  ( ( a e. A /\ b e. B ) -> ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) C_ ( A X. B ) )
35 34 sseld 
 |-  ( ( a e. A /\ b e. B ) -> ( e e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) -> e e. ( A X. B ) ) )
36 24 35 syl5 
 |-  ( ( a e. A /\ b e. B ) -> ( e e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) -> e e. ( A X. B ) ) )
37 elxp2 
 |-  ( e e. ( A X. B ) <-> E. c e. A E. d e. B e = <. c , d >. )
38 opex 
 |-  <. a , b >. e. _V
39 opex 
 |-  <. c , d >. e. _V
40 39 elpred 
 |-  ( <. a , b >. e. _V -> ( <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> ( <. c , d >. e. ( A X. B ) /\ <. c , d >. T <. a , b >. ) ) )
41 38 40 ax-mp 
 |-  ( <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> ( <. c , d >. e. ( A X. B ) /\ <. c , d >. T <. a , b >. ) )
42 opelxpi 
 |-  ( ( c e. A /\ d e. B ) -> <. c , d >. e. ( A X. B ) )
43 42 adantl 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> <. c , d >. e. ( A X. B ) )
44 43 biantrurd 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( <. c , d >. T <. a , b >. <-> ( <. c , d >. e. ( A X. B ) /\ <. c , d >. T <. a , b >. ) ) )
45 1 xpord2lem 
 |-  ( <. c , d >. T <. a , b >. <-> ( ( c e. A /\ d e. B ) /\ ( a e. A /\ b e. B ) /\ ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) ) )
46 eldif 
 |-  ( <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) <-> ( <. c , d >. e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) /\ -. <. c , d >. e. { <. a , b >. } ) )
47 opelxp 
 |-  ( <. c , d >. e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) <-> ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) )
48 elun 
 |-  ( c e. ( Pred ( R , A , a ) u. { a } ) <-> ( c e. Pred ( R , A , a ) \/ c e. { a } ) )
49 vex 
 |-  c e. _V
50 49 elpred 
 |-  ( a e. _V -> ( c e. Pred ( R , A , a ) <-> ( c e. A /\ c R a ) ) )
51 50 elv 
 |-  ( c e. Pred ( R , A , a ) <-> ( c e. A /\ c R a ) )
52 velsn 
 |-  ( c e. { a } <-> c = a )
53 51 52 orbi12i 
 |-  ( ( c e. Pred ( R , A , a ) \/ c e. { a } ) <-> ( ( c e. A /\ c R a ) \/ c = a ) )
54 48 53 bitri 
 |-  ( c e. ( Pred ( R , A , a ) u. { a } ) <-> ( ( c e. A /\ c R a ) \/ c = a ) )
55 elun 
 |-  ( d e. ( Pred ( S , B , b ) u. { b } ) <-> ( d e. Pred ( S , B , b ) \/ d e. { b } ) )
56 vex 
 |-  d e. _V
57 56 elpred 
 |-  ( b e. _V -> ( d e. Pred ( S , B , b ) <-> ( d e. B /\ d S b ) ) )
58 57 elv 
 |-  ( d e. Pred ( S , B , b ) <-> ( d e. B /\ d S b ) )
59 velsn 
 |-  ( d e. { b } <-> d = b )
60 58 59 orbi12i 
 |-  ( ( d e. Pred ( S , B , b ) \/ d e. { b } ) <-> ( ( d e. B /\ d S b ) \/ d = b ) )
61 55 60 bitri 
 |-  ( d e. ( Pred ( S , B , b ) u. { b } ) <-> ( ( d e. B /\ d S b ) \/ d = b ) )
62 54 61 anbi12i 
 |-  ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) <-> ( ( ( c e. A /\ c R a ) \/ c = a ) /\ ( ( d e. B /\ d S b ) \/ d = b ) ) )
63 47 62 bitri 
 |-  ( <. c , d >. e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) <-> ( ( ( c e. A /\ c R a ) \/ c = a ) /\ ( ( d e. B /\ d S b ) \/ d = b ) ) )
64 39 elsn 
 |-  ( <. c , d >. e. { <. a , b >. } <-> <. c , d >. = <. a , b >. )
65 64 notbii 
 |-  ( -. <. c , d >. e. { <. a , b >. } <-> -. <. c , d >. = <. a , b >. )
66 df-ne 
 |-  ( <. c , d >. =/= <. a , b >. <-> -. <. c , d >. = <. a , b >. )
67 49 56 opthne 
 |-  ( <. c , d >. =/= <. a , b >. <-> ( c =/= a \/ d =/= b ) )
68 65 66 67 3bitr2i 
 |-  ( -. <. c , d >. e. { <. a , b >. } <-> ( c =/= a \/ d =/= b ) )
69 63 68 anbi12i 
 |-  ( ( <. c , d >. e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) /\ -. <. c , d >. e. { <. a , b >. } ) <-> ( ( ( ( c e. A /\ c R a ) \/ c = a ) /\ ( ( d e. B /\ d S b ) \/ d = b ) ) /\ ( c =/= a \/ d =/= b ) ) )
70 46 69 bitri 
 |-  ( <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) <-> ( ( ( ( c e. A /\ c R a ) \/ c = a ) /\ ( ( d e. B /\ d S b ) \/ d = b ) ) /\ ( c =/= a \/ d =/= b ) ) )
71 simprl 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> c e. A )
72 71 biantrurd 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( c R a <-> ( c e. A /\ c R a ) ) )
73 72 orbi1d 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( c R a \/ c = a ) <-> ( ( c e. A /\ c R a ) \/ c = a ) ) )
74 simprr 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> d e. B )
75 74 biantrurd 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( d S b <-> ( d e. B /\ d S b ) ) )
76 75 orbi1d 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( d S b \/ d = b ) <-> ( ( d e. B /\ d S b ) \/ d = b ) ) )
77 73 76 3anbi12d 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) <-> ( ( ( c e. A /\ c R a ) \/ c = a ) /\ ( ( d e. B /\ d S b ) \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) ) )
78 df-3an 
 |-  ( ( ( ( c e. A /\ c R a ) \/ c = a ) /\ ( ( d e. B /\ d S b ) \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) <-> ( ( ( ( c e. A /\ c R a ) \/ c = a ) /\ ( ( d e. B /\ d S b ) \/ d = b ) ) /\ ( c =/= a \/ d =/= b ) ) )
79 77 78 bitr2di 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( ( ( ( c e. A /\ c R a ) \/ c = a ) /\ ( ( d e. B /\ d S b ) \/ d = b ) ) /\ ( c =/= a \/ d =/= b ) ) <-> ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) ) )
80 70 79 syl5bb 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) <-> ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) ) )
81 pm3.22 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( c e. A /\ d e. B ) /\ ( a e. A /\ b e. B ) ) )
82 81 biantrurd 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) <-> ( ( ( c e. A /\ d e. B ) /\ ( a e. A /\ b e. B ) ) /\ ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) ) ) )
83 df-3an 
 |-  ( ( ( c e. A /\ d e. B ) /\ ( a e. A /\ b e. B ) /\ ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) ) <-> ( ( ( c e. A /\ d e. B ) /\ ( a e. A /\ b e. B ) ) /\ ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) ) )
84 82 83 bitr4di 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) <-> ( ( c e. A /\ d e. B ) /\ ( a e. A /\ b e. B ) /\ ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) ) ) )
85 80 84 bitr2d 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( ( c e. A /\ d e. B ) /\ ( a e. A /\ b e. B ) /\ ( ( c R a \/ c = a ) /\ ( d S b \/ d = b ) /\ ( c =/= a \/ d =/= b ) ) ) <-> <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) )
86 45 85 syl5bb 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( <. c , d >. T <. a , b >. <-> <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) )
87 44 86 bitr3d 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( <. c , d >. e. ( A X. B ) /\ <. c , d >. T <. a , b >. ) <-> <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) )
88 41 87 syl5bb 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) )
89 eleq1 
 |-  ( e = <. c , d >. -> ( e e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) ) )
90 eleq1 
 |-  ( e = <. c , d >. -> ( e e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) <-> <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) )
91 89 90 bibi12d 
 |-  ( e = <. c , d >. -> ( ( e e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> e e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) <-> ( <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) ) )
92 88 91 syl5ibrcom 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( e = <. c , d >. -> ( e e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> e e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) ) )
93 92 rexlimdvva 
 |-  ( ( a e. A /\ b e. B ) -> ( E. c e. A E. d e. B e = <. c , d >. -> ( e e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> e e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) ) )
94 37 93 syl5bi 
 |-  ( ( a e. A /\ b e. B ) -> ( e e. ( A X. B ) -> ( e e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> e e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) ) )
95 23 36 94 pm5.21ndd 
 |-  ( ( a e. A /\ b e. B ) -> ( e e. Pred ( T , ( A X. B ) , <. a , b >. ) <-> e e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) ) )
96 95 eqrdv 
 |-  ( ( 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 >. } ) )
97 11 21 96 vtocl2ga 
 |-  ( ( X e. A /\ Y e. B ) -> Pred ( T , ( A X. B ) , <. X , Y >. ) = ( ( ( Pred ( R , A , X ) u. { X } ) X. ( Pred ( S , B , Y ) u. { Y } ) ) \ { <. X , Y >. } ) )