This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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