Metamath Proof Explorer


Theorem asymref2

Description: Two ways of saying a relation is antisymmetric and reflexive. (Contributed by NM, 6-May-2008) (Proof shortened by Mario Carneiro, 4-Dec-2016)

Ref Expression
Assertion asymref2 R R -1 = I R x R x R x x y x R y y R x x = y

Proof

Step Hyp Ref Expression
1 asymref R R -1 = I R x R y x R y y R x x = y
2 albiim y x R y y R x x = y y x R y y R x x = y y x = y x R y y R x
3 2 ralbii x R y x R y y R x x = y x R y x R y y R x x = y y x = y x R y y R x
4 r19.26 x R y x R y y R x x = y y x = y x R y y R x x R y x R y y R x x = y x R y x = y x R y y R x
5 ancom x R y x R y y R x x = y x R y x = y x R y y R x x R y x = y x R y y R x x R y x R y y R x x = y
6 equcom x = y y = x
7 6 imbi1i x = y x R y y R x y = x x R y y R x
8 7 albii y x = y x R y y R x y y = x x R y y R x
9 breq2 y = x x R y x R x
10 breq1 y = x y R x x R x
11 9 10 anbi12d y = x x R y y R x x R x x R x
12 anidm x R x x R x x R x
13 11 12 bitrdi y = x x R y y R x x R x
14 13 equsalvw y y = x x R y y R x x R x
15 8 14 bitri y x = y x R y y R x x R x
16 15 ralbii x R y x = y x R y y R x x R x R x
17 df-ral x R y x R y y R x x = y x x R y x R y y R x x = y
18 df-br x R y x y R
19 vex x V
20 vex y V
21 19 20 opeluu x y R x R y R
22 21 simpld x y R x R
23 18 22 sylbi x R y x R
24 23 adantr x R y y R x x R
25 24 pm2.24d x R y y R x ¬ x R x = y
26 25 com12 ¬ x R x R y y R x x = y
27 26 alrimiv ¬ x R y x R y y R x x = y
28 id y x R y y R x x = y y x R y y R x x = y
29 27 28 ja x R y x R y y R x x = y y x R y y R x x = y
30 ax-1 y x R y y R x x = y x R y x R y y R x x = y
31 29 30 impbii x R y x R y y R x x = y y x R y y R x x = y
32 31 albii x x R y x R y y R x x = y x y x R y y R x x = y
33 17 32 bitri x R y x R y y R x x = y x y x R y y R x x = y
34 16 33 anbi12i x R y x = y x R y y R x x R y x R y y R x x = y x R x R x x y x R y y R x x = y
35 4 5 34 3bitri x R y x R y y R x x = y y x = y x R y y R x x R x R x x y x R y y R x x = y
36 1 3 35 3bitri R R -1 = I R x R x R x x y x R y y R x x = y