Metamath Proof Explorer


Theorem dfpo2

Description: Quantifier-free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfpo2 R Po A R I A = R A × A R A × A R

Proof

Step Hyp Ref Expression
1 po0 R Po
2 res0 I =
3 2 ineq2i R I = R
4 in0 R =
5 3 4 eqtri R I =
6 xp0 A × =
7 6 ineq2i R A × = R
8 7 4 eqtri R A × =
9 8 coeq2i R A × A R A × = R A × A
10 co02 R A × A =
11 9 10 eqtri R A × A R A × =
12 0ss R
13 11 12 eqsstri R A × A R A × R
14 5 13 pm3.2i R I = R A × A R A × R
15 1 14 2th R Po R I = R A × A R A × R
16 poeq2 A = R Po A R Po
17 reseq2 A = I A = I
18 17 ineq2d A = R I A = R I
19 18 eqeq1d A = R I A = R I =
20 xpeq2 A = A × A = A ×
21 20 ineq2d A = R A × A = R A ×
22 21 coeq2d A = R A × A R A × A = R A × A R A ×
23 22 sseq1d A = R A × A R A × A R R A × A R A × R
24 19 23 anbi12d A = R I A = R A × A R A × A R R I = R A × A R A × R
25 16 24 bibi12d A = R Po A R I A = R A × A R A × A R R Po R I = R A × A R A × R
26 15 25 mpbiri A = R Po A R I A = R A × A R A × A R
27 r19.28zv A z A ¬ x R x x R y y R z x R z ¬ x R x z A x R y y R z x R z
28 27 ralbidv A y A z A ¬ x R x x R y y R z x R z y A ¬ x R x z A x R y y R z x R z
29 r19.28zv A y A ¬ x R x z A x R y y R z x R z ¬ x R x y A z A x R y y R z x R z
30 28 29 bitrd A y A z A ¬ x R x x R y y R z x R z ¬ x R x y A z A x R y y R z x R z
31 30 ralbidv A x A y A z A ¬ x R x x R y y R z x R z x A ¬ x R x y A z A x R y y R z x R z
32 r19.26 x A ¬ x R x y A z A x R y y R z x R z x A ¬ x R x x A y A z A x R y y R z x R z
33 31 32 bitrdi A x A y A z A ¬ x R x x R y y R z x R z x A ¬ x R x x A y A z A x R y y R z x R z
34 df-po R Po A x A y A z A ¬ x R x x R y y R z x R z
35 disj R I A = w R ¬ w I A
36 df-ral w R ¬ w I A w w R ¬ w I A
37 opex x x V
38 eleq1 w = x x w R x x R
39 df-br x R x x x R
40 38 39 bitr4di w = x x w R x R x
41 eleq1 w = x x w I A x x I A
42 opelidres x V x x I A x A
43 42 elv x x I A x A
44 41 43 bitrdi w = x x w I A x A
45 44 notbid w = x x ¬ w I A ¬ x A
46 40 45 imbi12d w = x x w R ¬ w I A x R x ¬ x A
47 37 46 spcv w w R ¬ w I A x R x ¬ x A
48 47 con2d w w R ¬ w I A x A ¬ x R x
49 48 alrimiv w w R ¬ w I A x x A ¬ x R x
50 relres Rel I A
51 elrel Rel I A w I A y z w = y z
52 50 51 mpan w I A y z w = y z
53 52 ancri w I A y z w = y z w I A
54 eleq1 x = y x A y A
55 breq12 x = y x = y x R x y R y
56 55 anidms x = y x R x y R y
57 56 notbid x = y ¬ x R x ¬ y R y
58 54 57 imbi12d x = y x A ¬ x R x y A ¬ y R y
59 58 spvv x x A ¬ x R x y A ¬ y R y
60 breq2 y = z y R y y R z
61 60 notbid y = z ¬ y R y ¬ y R z
62 61 imbi2d y = z y A ¬ y R y y A ¬ y R z
63 62 biimpcd y A ¬ y R y y = z y A ¬ y R z
64 63 impcomd y A ¬ y R y y A y = z ¬ y R z
65 59 64 syl x x A ¬ x R x y A y = z ¬ y R z
66 eleq1 w = y z w I A y z I A
67 vex z V
68 67 brresi y I A z y A y I z
69 df-br y I A z y z I A
70 67 ideq y I z y = z
71 70 anbi2i y A y I z y A y = z
72 68 69 71 3bitr3ri y A y = z y z I A
73 66 72 bitr4di w = y z w I A y A y = z
74 eleq1 w = y z w R y z R
75 df-br y R z y z R
76 74 75 bitr4di w = y z w R y R z
77 76 notbid w = y z ¬ w R ¬ y R z
78 73 77 imbi12d w = y z w I A ¬ w R y A y = z ¬ y R z
79 65 78 syl5ibrcom x x A ¬ x R x w = y z w I A ¬ w R
80 79 exlimdvv x x A ¬ x R x y z w = y z w I A ¬ w R
81 80 impd x x A ¬ x R x y z w = y z w I A ¬ w R
82 53 81 syl5 x x A ¬ x R x w I A ¬ w R
83 82 con2d x x A ¬ x R x w R ¬ w I A
84 83 alrimiv x x A ¬ x R x w w R ¬ w I A
85 49 84 impbii w w R ¬ w I A x x A ¬ x R x
86 df-ral x A ¬ x R x x x A ¬ x R x
87 85 86 bitr4i w w R ¬ w I A x A ¬ x R x
88 35 36 87 3bitri R I A = x A ¬ x R x
89 ralcom y A z A x R y y R z x R z z A y A x R y y R z x R z
90 r19.23v y A x R y y R z x R z y A x R y y R z x R z
91 90 ralbii z A y A x R y y R z x R z z A y A x R y y R z x R z
92 89 91 bitri y A z A x R y y R z x R z z A y A x R y y R z x R z
93 92 ralbii x A y A z A x R y y R z x R z x A z A y A x R y y R z x R z
94 brin x R A × A y x R y x A × A y
95 brin y R A × A z y R z y A × A z
96 94 95 anbi12i x R A × A y y R A × A z x R y x A × A y y R z y A × A z
97 an4 x R y x A × A y y R z y A × A z x R y y R z x A × A y y A × A z
98 ancom x R y y R z x A × A y y A × A z x A × A y y A × A z x R y y R z
99 ancom x A y A y A x A
100 99 anbi1i x A y A y A z A y A x A y A z A
101 brxp x A × A y x A y A
102 brxp y A × A z y A z A
103 101 102 anbi12i x A × A y y A × A z x A y A y A z A
104 anandi y A x A z A y A x A y A z A
105 100 103 104 3bitr4i x A × A y y A × A z y A x A z A
106 105 anbi1i x A × A y y A × A z x R y y R z y A x A z A x R y y R z
107 97 98 106 3bitri x R y x A × A y y R z y A × A z y A x A z A x R y y R z
108 anass y A x A z A x R y y R z y A x A z A x R y y R z
109 96 107 108 3bitri x R A × A y y R A × A z y A x A z A x R y y R z
110 109 exbii y x R A × A y y R A × A z y y A x A z A x R y y R z
111 vex x V
112 111 67 brco x R A × A R A × A z y x R A × A y y R A × A z
113 df-br x R A × A R A × A z x z R A × A R A × A
114 112 113 bitr3i y x R A × A y y R A × A z x z R A × A R A × A
115 df-rex y A x A z A x R y y R z y y A x A z A x R y y R z
116 r19.42v y A x A z A x R y y R z x A z A y A x R y y R z
117 115 116 bitr3i y y A x A z A x R y y R z x A z A y A x R y y R z
118 110 114 117 3bitr3ri x A z A y A x R y y R z x z R A × A R A × A
119 df-br x R z x z R
120 118 119 imbi12i x A z A y A x R y y R z x R z x z R A × A R A × A x z R
121 120 2albii x z x A z A y A x R y y R z x R z x z x z R A × A R A × A x z R
122 r2al x A z A y A x R y y R z x R z x z x A z A y A x R y y R z x R z
123 impexp x A z A y A x R y y R z x R z x A z A y A x R y y R z x R z
124 123 2albii x z x A z A y A x R y y R z x R z x z x A z A y A x R y y R z x R z
125 122 124 bitr4i x A z A y A x R y y R z x R z x z x A z A y A x R y y R z x R z
126 relco Rel R A × A R A × A
127 ssrel Rel R A × A R A × A R A × A R A × A R x z x z R A × A R A × A x z R
128 126 127 ax-mp R A × A R A × A R x z x z R A × A R A × A x z R
129 121 125 128 3bitr4i x A z A y A x R y y R z x R z R A × A R A × A R
130 93 129 bitr2i R A × A R A × A R x A y A z A x R y y R z x R z
131 88 130 anbi12i R I A = R A × A R A × A R x A ¬ x R x x A y A z A x R y y R z x R z
132 33 34 131 3bitr4g A R Po A R I A = R A × A R A × A R
133 26 132 pm2.61ine R Po A R I A = R A × A R A × A R