Metamath Proof Explorer

Theorem xpord2ind

Description: Induction over the cross product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-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 ) ) }
xpord2ind.1 
|- R Fr A
xpord2ind.2 
|- R Po A
xpord2ind.3 
|- R Se A
xpord2ind.4 
|- S Fr B
xpord2ind.5 
|- S Po B
xpord2ind.6 
|- S Se B
xpord2ind.7 
|- ( a = c -> ( ph <-> ps ) )
xpord2ind.8 
|- ( b = d -> ( ps <-> ch ) )
xpord2ind.9 
|- ( a = c -> ( th <-> ch ) )
xpord2ind.11 
|- ( a = X -> ( ph <-> ta ) )
xpord2ind.12 
|- ( b = Y -> ( ta <-> et ) )
xpord2ind.i 
|- ( ( a e. A /\ b e. B ) -> ( ( A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ch /\ A. c e. Pred ( R , A , a ) ps /\ A. d e. Pred ( S , B , b ) th ) -> ph ) )
Assertion xpord2ind 
|- ( ( X e. A /\ Y e. B ) -> et )

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 xpord2ind.1 
 |-  R Fr A
3 xpord2ind.2 
 |-  R Po A
4 xpord2ind.3 
 |-  R Se A
5 xpord2ind.4 
 |-  S Fr B
6 xpord2ind.5 
 |-  S Po B
7 xpord2ind.6 
 |-  S Se B
8 xpord2ind.7 
 |-  ( a = c -> ( ph <-> ps ) )
9 xpord2ind.8 
 |-  ( b = d -> ( ps <-> ch ) )
10 xpord2ind.9 
 |-  ( a = c -> ( th <-> ch ) )
11 xpord2ind.11 
 |-  ( a = X -> ( ph <-> ta ) )
12 xpord2ind.12 
 |-  ( b = Y -> ( ta <-> et ) )
13 xpord2ind.i 
 |-  ( ( a e. A /\ b e. B ) -> ( ( A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ch /\ A. c e. Pred ( R , A , a ) ps /\ A. d e. Pred ( S , B , b ) th ) -> ph ) )
14 2 a1i 
 |-  ( T. -> R Fr A )
15 5 a1i 
 |-  ( T. -> S Fr B )
16 1 14 15 frxp2 
 |-  ( T. -> T Fr ( A X. B ) )
17 3 a1i 
 |-  ( T. -> R Po A )
18 6 a1i 
 |-  ( T. -> S Po B )
19 1 17 18 poxp2 
 |-  ( T. -> T Po ( A X. B ) )
20 4 a1i 
 |-  ( T. -> R Se A )
21 7 a1i 
 |-  ( T. -> S Se B )
22 1 20 21 sexp2 
 |-  ( T. -> T Se ( A X. B ) )
23 16 19 22 3jca 
 |-  ( T. -> ( T Fr ( A X. B ) /\ T Po ( A X. B ) /\ T Se ( A X. B ) ) )
24 23 mptru 
 |-  ( T Fr ( A X. B ) /\ T Po ( A X. B ) /\ T Se ( A X. B ) )
25 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 >. } ) )
26 25 eleq2d 
 |-  ( ( a e. A /\ b 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 >. } ) ) )
27 26 imbi1d 
 |-  ( ( a e. A /\ b e. B ) -> ( ( <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) -> ch ) <-> ( <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) -> ch ) ) )
28 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 >. } ) )
29 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 } ) ) )
30 opex 
 |-  <. c , d >. e. _V
31 30 elsn 
 |-  ( <. c , d >. e. { <. a , b >. } <-> <. c , d >. = <. a , b >. )
32 31 notbii 
 |-  ( -. <. c , d >. e. { <. a , b >. } <-> -. <. c , d >. = <. a , b >. )
33 df-ne 
 |-  ( <. c , d >. =/= <. a , b >. <-> -. <. c , d >. = <. a , b >. )
34 vex 
 |-  c e. _V
35 vex 
 |-  d e. _V
36 34 35 opthne 
 |-  ( <. c , d >. =/= <. a , b >. <-> ( c =/= a \/ d =/= b ) )
37 32 33 36 3bitr2i 
 |-  ( -. <. c , d >. e. { <. a , b >. } <-> ( c =/= a \/ d =/= b ) )
38 29 37 anbi12i 
 |-  ( ( <. c , d >. e. ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) /\ -. <. c , d >. e. { <. a , b >. } ) <-> ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) /\ ( c =/= a \/ d =/= b ) ) )
39 28 38 bitri 
 |-  ( <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) <-> ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) /\ ( c =/= a \/ d =/= b ) ) )
40 39 imbi1i 
 |-  ( ( <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) -> ch ) <-> ( ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) /\ ( c =/= a \/ d =/= b ) ) -> ch ) )
41 impexp 
 |-  ( ( ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) /\ ( c =/= a \/ d =/= b ) ) -> ch ) <-> ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) -> ( ( c =/= a \/ d =/= b ) -> ch ) ) )
42 40 41 bitri 
 |-  ( ( <. c , d >. e. ( ( ( Pred ( R , A , a ) u. { a } ) X. ( Pred ( S , B , b ) u. { b } ) ) \ { <. a , b >. } ) -> ch ) <-> ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) -> ( ( c =/= a \/ d =/= b ) -> ch ) ) )
43 27 42 bitrdi 
 |-  ( ( a e. A /\ b e. B ) -> ( ( <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) -> ch ) <-> ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) -> ( ( c =/= a \/ d =/= b ) -> ch ) ) ) )
44 43 2albidv 
 |-  ( ( a e. A /\ b e. B ) -> ( A. c A. d ( <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) -> ch ) <-> A. c A. d ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) -> ( ( c =/= a \/ d =/= b ) -> ch ) ) ) )
45 r2al 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) <-> A. c A. d ( ( c e. ( Pred ( R , A , a ) u. { a } ) /\ d e. ( Pred ( S , B , b ) u. { b } ) ) -> ( ( c =/= a \/ d =/= b ) -> ch ) ) )
46 44 45 bitr4di 
 |-  ( ( a e. A /\ b e. B ) -> ( A. c A. d ( <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) -> ch ) <-> A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) ) )
47 ssun1 
 |-  Pred ( R , A , a ) C_ ( Pred ( R , A , a ) u. { a } )
48 ssralv 
 |-  ( Pred ( R , A , a ) C_ ( Pred ( R , A , a ) u. { a } ) -> ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) ) )
49 47 48 ax-mp 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) )
50 ssun1 
 |-  Pred ( S , B , b ) C_ ( Pred ( S , B , b ) u. { b } )
51 ssralv 
 |-  ( Pred ( S , B , b ) C_ ( Pred ( S , B , b ) u. { b } ) -> ( A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) ) )
52 50 51 ax-mp 
 |-  ( A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) )
53 52 ralimi 
 |-  ( A. c e. Pred ( R , A , a ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) )
54 49 53 syl 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) )
55 predpoirr 
 |-  ( S Po B -> -. b e. Pred ( S , B , b ) )
56 6 55 ax-mp 
 |-  -. b e. Pred ( S , B , b )
57 eleq1w 
 |-  ( d = b -> ( d e. Pred ( S , B , b ) <-> b e. Pred ( S , B , b ) ) )
58 56 57 mtbiri 
 |-  ( d = b -> -. d e. Pred ( S , B , b ) )
59 58 necon2ai 
 |-  ( d e. Pred ( S , B , b ) -> d =/= b )
60 59 olcd 
 |-  ( d e. Pred ( S , B , b ) -> ( c =/= a \/ d =/= b ) )
61 pm2.27 
 |-  ( ( c =/= a \/ d =/= b ) -> ( ( ( c =/= a \/ d =/= b ) -> ch ) -> ch ) )
62 60 61 syl 
 |-  ( d e. Pred ( S , B , b ) -> ( ( ( c =/= a \/ d =/= b ) -> ch ) -> ch ) )
63 62 ralimia 
 |-  ( A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. d e. Pred ( S , B , b ) ch )
64 63 ralimi 
 |-  ( A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ch )
65 54 64 syl 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ch )
66 ssun2 
 |-  { b } C_ ( Pred ( S , B , b ) u. { b } )
67 ssralv 
 |-  ( { b } C_ ( Pred ( S , B , b ) u. { b } ) -> ( A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. d e. { b } ( ( c =/= a \/ d =/= b ) -> ch ) ) )
68 66 67 ax-mp 
 |-  ( A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. d e. { b } ( ( c =/= a \/ d =/= b ) -> ch ) )
69 68 ralimi 
 |-  ( A. c e. Pred ( R , A , a ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) A. d e. { b } ( ( c =/= a \/ d =/= b ) -> ch ) )
70 49 69 syl 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) A. d e. { b } ( ( c =/= a \/ d =/= b ) -> ch ) )
71 vex 
 |-  b e. _V
72 neeq1 
 |-  ( d = b -> ( d =/= b <-> b =/= b ) )
73 72 orbi2d 
 |-  ( d = b -> ( ( c =/= a \/ d =/= b ) <-> ( c =/= a \/ b =/= b ) ) )
74 9 equcoms 
 |-  ( d = b -> ( ps <-> ch ) )
75 74 bicomd 
 |-  ( d = b -> ( ch <-> ps ) )
76 73 75 imbi12d 
 |-  ( d = b -> ( ( ( c =/= a \/ d =/= b ) -> ch ) <-> ( ( c =/= a \/ b =/= b ) -> ps ) ) )
77 71 76 ralsn 
 |-  ( A. d e. { b } ( ( c =/= a \/ d =/= b ) -> ch ) <-> ( ( c =/= a \/ b =/= b ) -> ps ) )
78 77 ralbii 
 |-  ( A. c e. Pred ( R , A , a ) A. d e. { b } ( ( c =/= a \/ d =/= b ) -> ch ) <-> A. c e. Pred ( R , A , a ) ( ( c =/= a \/ b =/= b ) -> ps ) )
79 70 78 sylib 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) ( ( c =/= a \/ b =/= b ) -> ps ) )
80 predpoirr 
 |-  ( R Po A -> -. a e. Pred ( R , A , a ) )
81 3 80 ax-mp 
 |-  -. a e. Pred ( R , A , a )
82 eleq1w 
 |-  ( c = a -> ( c e. Pred ( R , A , a ) <-> a e. Pred ( R , A , a ) ) )
83 81 82 mtbiri 
 |-  ( c = a -> -. c e. Pred ( R , A , a ) )
84 83 necon2ai 
 |-  ( c e. Pred ( R , A , a ) -> c =/= a )
85 84 orcd 
 |-  ( c e. Pred ( R , A , a ) -> ( c =/= a \/ b =/= b ) )
86 pm2.27 
 |-  ( ( c =/= a \/ b =/= b ) -> ( ( ( c =/= a \/ b =/= b ) -> ps ) -> ps ) )
87 85 86 syl 
 |-  ( c e. Pred ( R , A , a ) -> ( ( ( c =/= a \/ b =/= b ) -> ps ) -> ps ) )
88 87 ralimia 
 |-  ( A. c e. Pred ( R , A , a ) ( ( c =/= a \/ b =/= b ) -> ps ) -> A. c e. Pred ( R , A , a ) ps )
89 79 88 syl 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. Pred ( R , A , a ) ps )
90 ssun2 
 |-  { a } C_ ( Pred ( R , A , a ) u. { a } )
91 ssralv 
 |-  ( { a } C_ ( Pred ( R , A , a ) u. { a } ) -> ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. { a } A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) ) )
92 90 91 ax-mp 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. { a } A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) )
93 52 ralimi 
 |-  ( A. c e. { a } A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. { a } A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) )
94 92 93 syl 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. c e. { a } A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) )
95 vex 
 |-  a e. _V
96 neeq1 
 |-  ( c = a -> ( c =/= a <-> a =/= a ) )
97 96 orbi1d 
 |-  ( c = a -> ( ( c =/= a \/ d =/= b ) <-> ( a =/= a \/ d =/= b ) ) )
98 10 equcoms 
 |-  ( c = a -> ( th <-> ch ) )
99 98 bicomd 
 |-  ( c = a -> ( ch <-> th ) )
100 97 99 imbi12d 
 |-  ( c = a -> ( ( ( c =/= a \/ d =/= b ) -> ch ) <-> ( ( a =/= a \/ d =/= b ) -> th ) ) )
101 100 ralbidv 
 |-  ( c = a -> ( A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) <-> A. d e. Pred ( S , B , b ) ( ( a =/= a \/ d =/= b ) -> th ) ) )
102 95 101 ralsn 
 |-  ( A. c e. { a } A. d e. Pred ( S , B , b ) ( ( c =/= a \/ d =/= b ) -> ch ) <-> A. d e. Pred ( S , B , b ) ( ( a =/= a \/ d =/= b ) -> th ) )
103 94 102 sylib 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. d e. Pred ( S , B , b ) ( ( a =/= a \/ d =/= b ) -> th ) )
104 59 olcd 
 |-  ( d e. Pred ( S , B , b ) -> ( a =/= a \/ d =/= b ) )
105 pm2.27 
 |-  ( ( a =/= a \/ d =/= b ) -> ( ( ( a =/= a \/ d =/= b ) -> th ) -> th ) )
106 104 105 syl 
 |-  ( d e. Pred ( S , B , b ) -> ( ( ( a =/= a \/ d =/= b ) -> th ) -> th ) )
107 106 ralimia 
 |-  ( A. d e. Pred ( S , B , b ) ( ( a =/= a \/ d =/= b ) -> th ) -> A. d e. Pred ( S , B , b ) th )
108 103 107 syl 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> A. d e. Pred ( S , B , b ) th )
109 65 89 108 3jca 
 |-  ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> ( A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ch /\ A. c e. Pred ( R , A , a ) ps /\ A. d e. Pred ( S , B , b ) th ) )
110 109 13 syl5 
 |-  ( ( a e. A /\ b e. B ) -> ( A. c e. ( Pred ( R , A , a ) u. { a } ) A. d e. ( Pred ( S , B , b ) u. { b } ) ( ( c =/= a \/ d =/= b ) -> ch ) -> ph ) )
111 46 110 sylbid 
 |-  ( ( a e. A /\ b e. B ) -> ( A. c A. d ( <. c , d >. e. Pred ( T , ( A X. B ) , <. a , b >. ) -> ch ) -> ph ) )
112 111 8 9 11 12 frpoins3xpg 
 |-  ( ( ( T Fr ( A X. B ) /\ T Po ( A X. B ) /\ T Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> et )
113 24 112 mpan 
 |-  ( ( X e. A /\ Y e. B ) -> et )