Metamath Proof Explorer


Theorem frxp2

Description: Another way of giving a founded order to a cross product of two classes. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses xpord2.1 T = x y | x A × B y A × B 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y 2 nd x = 2 nd y x y
frxp2.1 φ R Fr A
frxp2.2 φ S Fr B
Assertion frxp2 φ T Fr A × B

Proof

Step Hyp Ref Expression
1 xpord2.1 T = x y | x A × B y A × B 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y 2 nd x = 2 nd y x y
2 frxp2.1 φ R Fr A
3 frxp2.2 φ S Fr B
4 dmss s A × B dom s dom A × B
5 4 ad2antrl φ s A × B s dom s dom A × B
6 dmxpss dom A × B A
7 5 6 sstrdi φ s A × B s dom s A
8 simprr φ s A × B s s
9 relxp Rel A × B
10 relss s A × B Rel A × B Rel s
11 9 10 mpi s A × B Rel s
12 11 ad2antrl φ s A × B s Rel s
13 reldm0 Rel s s = dom s =
14 12 13 syl φ s A × B s s = dom s =
15 14 necon3bid φ s A × B s s dom s
16 8 15 mpbid φ s A × B s dom s
17 2 adantr φ s A × B s R Fr A
18 df-fr R Fr A c c A c a c b c ¬ b R a
19 17 18 sylib φ s A × B s c c A c a c b c ¬ b R a
20 vex s V
21 20 dmex dom s V
22 sseq1 c = dom s c A dom s A
23 neeq1 c = dom s c dom s
24 22 23 anbi12d c = dom s c A c dom s A dom s
25 raleq c = dom s b c ¬ b R a b dom s ¬ b R a
26 25 rexeqbi1dv c = dom s a c b c ¬ b R a a dom s b dom s ¬ b R a
27 24 26 imbi12d c = dom s c A c a c b c ¬ b R a dom s A dom s a dom s b dom s ¬ b R a
28 21 27 spcv c c A c a c b c ¬ b R a dom s A dom s a dom s b dom s ¬ b R a
29 19 28 syl φ s A × B s dom s A dom s a dom s b dom s ¬ b R a
30 7 16 29 mp2and φ s A × B s a dom s b dom s ¬ b R a
31 imassrn s a ran s
32 rnss s A × B ran s ran A × B
33 32 ad2antrl φ s A × B s ran s ran A × B
34 33 adantr φ s A × B s a dom s b dom s ¬ b R a ran s ran A × B
35 rnxpss ran A × B B
36 34 35 sstrdi φ s A × B s a dom s b dom s ¬ b R a ran s B
37 31 36 sstrid φ s A × B s a dom s b dom s ¬ b R a s a B
38 simprl φ s A × B s a dom s b dom s ¬ b R a a dom s
39 imadisj s a = dom s a =
40 disjsn dom s a = ¬ a dom s
41 39 40 bitri s a = ¬ a dom s
42 41 necon2abii a dom s s a
43 38 42 sylib φ s A × B s a dom s b dom s ¬ b R a s a
44 df-fr S Fr B e e B e c e d e ¬ d S c
45 3 44 sylib φ e e B e c e d e ¬ d S c
46 45 ad2antrr φ s A × B s a dom s b dom s ¬ b R a e e B e c e d e ¬ d S c
47 20 imaex s a V
48 sseq1 e = s a e B s a B
49 neeq1 e = s a e s a
50 48 49 anbi12d e = s a e B e s a B s a
51 raleq e = s a d e ¬ d S c d s a ¬ d S c
52 51 rexeqbi1dv e = s a c e d e ¬ d S c c s a d s a ¬ d S c
53 50 52 imbi12d e = s a e B e c e d e ¬ d S c s a B s a c s a d s a ¬ d S c
54 47 53 spcv e e B e c e d e ¬ d S c s a B s a c s a d s a ¬ d S c
55 46 54 syl φ s A × B s a dom s b dom s ¬ b R a s a B s a c s a d s a ¬ d S c
56 37 43 55 mp2and φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c
57 simprl φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c c s a
58 vex a V
59 vex c V
60 58 59 elimasn c s a a c s
61 57 60 sylib φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c a c s
62 12 ad2antrr φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c Rel s
63 elrel Rel s q s e f q = e f
64 62 63 sylan φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c q s e f q = e f
65 breq1 d = f d S c f S c
66 65 notbid d = f ¬ d S c ¬ f S c
67 simplrr φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c a f s d s a ¬ d S c
68 vex f V
69 58 68 elimasn f s a a f s
70 69 biimpri a f s f s a
71 70 adantl φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c a f s f s a
72 66 67 71 rspcdva φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c a f s ¬ f S c
73 72 intnanrd φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c a f s ¬ f S c f c
74 opeq1 e = a e f = a f
75 74 eleq1d e = a e f s a f s
76 75 anbi2d e = a φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c a f s
77 3anass e R a e = a f S c f = c e a f c e R a e = a f S c f = c e a f c
78 olc e = a e R a e = a
79 78 biantrurd e = a f S c f = c e a f c e R a e = a f S c f = c e a f c
80 neeq1 e = a e a a a
81 80 orbi1d e = a e a f c a a f c
82 neirr ¬ a a
83 biorf ¬ a a f c a a f c
84 82 83 ax-mp f c a a f c
85 81 84 bitr4di e = a e a f c f c
86 85 anbi2d e = a f S c f = c e a f c f S c f = c f c
87 andir f S c f = c f c f S c f c f = c f c
88 nonconne ¬ f = c f c
89 88 biorfi f S c f c f S c f c f = c f c
90 87 89 bitr4i f S c f = c f c f S c f c
91 86 90 bitrdi e = a f S c f = c e a f c f S c f c
92 79 91 bitr3d e = a e R a e = a f S c f = c e a f c f S c f c
93 77 92 syl5bb e = a e R a e = a f S c f = c e a f c f S c f c
94 93 notbid e = a ¬ e R a e = a f S c f = c e a f c ¬ f S c f c
95 76 94 imbi12d e = a φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s ¬ e R a e = a f S c f = c e a f c φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c a f s ¬ f S c f c
96 73 95 mpbiri e = a φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s ¬ e R a e = a f S c f = c e a f c
97 96 impcom φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s e = a ¬ e R a e = a f S c f = c e a f c
98 breq1 b = e b R a e R a
99 98 notbid b = e ¬ b R a ¬ e R a
100 simplrr φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c b dom s ¬ b R a
101 100 ad2antrr φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s e a b dom s ¬ b R a
102 vex e V
103 102 68 opeldm e f s e dom s
104 103 adantl φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s e dom s
105 104 adantr φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s e a e dom s
106 99 101 105 rspcdva φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s e a ¬ e R a
107 simpr φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s e a e a
108 107 neneqd φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s e a ¬ e = a
109 ioran ¬ e R a e = a ¬ e R a ¬ e = a
110 106 108 109 sylanbrc φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s e a ¬ e R a e = a
111 110 intn3an1d φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s e a ¬ e R a e = a f S c f = c e a f c
112 97 111 pm2.61dane φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s ¬ e R a e = a f S c f = c e a f c
113 112 intn3an3d φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s ¬ e A f B a A c B e R a e = a f S c f = c e a f c
114 eleq1 q = e f q s e f s
115 114 anbi2d q = e f φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c q s φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s
116 breq1 q = e f q T a c e f T a c
117 1 xpord2lem e f T a c e A f B a A c B e R a e = a f S c f = c e a f c
118 116 117 bitrdi q = e f q T a c e A f B a A c B e R a e = a f S c f = c e a f c
119 118 notbid q = e f ¬ q T a c ¬ e A f B a A c B e R a e = a f S c f = c e a f c
120 115 119 imbi12d q = e f φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c q s ¬ q T a c φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c e f s ¬ e A f B a A c B e R a e = a f S c f = c e a f c
121 113 120 mpbiri q = e f φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c q s ¬ q T a c
122 121 com12 φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c q s q = e f ¬ q T a c
123 122 exlimdvv φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c q s e f q = e f ¬ q T a c
124 64 123 mpd φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c q s ¬ q T a c
125 124 ralrimiva φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c q s ¬ q T a c
126 breq2 p = a c q T p q T a c
127 126 notbid p = a c ¬ q T p ¬ q T a c
128 127 ralbidv p = a c q s ¬ q T p q s ¬ q T a c
129 128 rspcev a c s q s ¬ q T a c p s q s ¬ q T p
130 61 125 129 syl2anc φ s A × B s a dom s b dom s ¬ b R a c s a d s a ¬ d S c p s q s ¬ q T p
131 56 130 rexlimddv φ s A × B s a dom s b dom s ¬ b R a p s q s ¬ q T p
132 30 131 rexlimddv φ s A × B s p s q s ¬ q T p
133 132 ex φ s A × B s p s q s ¬ q T p
134 133 alrimiv φ s s A × B s p s q s ¬ q T p
135 df-fr T Fr A × B s s A × B s p s q s ¬ q T p
136 134 135 sylibr φ T Fr A × B