Metamath Proof Explorer


Theorem intasym

Description: Two ways of saying a relation is antisymmetric. Definition of antisymmetry in Schechter p. 51. (Contributed by NM, 9-Sep-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

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

Proof

Step Hyp Ref Expression
1 relcnv Rel R -1
2 relin2 Rel R -1 Rel R R -1
3 ssrel Rel R R -1 R R -1 I x y x y R R -1 x y I
4 1 2 3 mp2b R R -1 I x y x y R R -1 x y I
5 elin x y R R -1 x y R x y R -1
6 df-br x R y x y R
7 vex x V
8 vex y V
9 7 8 brcnv x R -1 y y R x
10 df-br x R -1 y x y R -1
11 9 10 bitr3i y R x x y R -1
12 6 11 anbi12i x R y y R x x y R x y R -1
13 5 12 bitr4i x y R R -1 x R y y R x
14 df-br x I y x y I
15 8 ideq x I y x = y
16 14 15 bitr3i x y I x = y
17 13 16 imbi12i x y R R -1 x y I x R y y R x x = y
18 17 2albii x y x y R R -1 x y I x y x R y y R x x = y
19 4 18 bitri R R -1 I x y x R y y R x x = y