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 ( ( 𝑅 𝑅 ) ⊆ I ↔ ∀ 𝑥𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 relcnv Rel 𝑅
2 relin2 ( Rel 𝑅 → Rel ( 𝑅 𝑅 ) )
3 ssrel ( Rel ( 𝑅 𝑅 ) → ( ( 𝑅 𝑅 ) ⊆ I ↔ ∀ 𝑥𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 𝑅 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ) )
4 1 2 3 mp2b ( ( 𝑅 𝑅 ) ⊆ I ↔ ∀ 𝑥𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 𝑅 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
5 elin ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 𝑅 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
6 df-br ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
7 vex 𝑥 ∈ V
8 vex 𝑦 ∈ V
9 7 8 brcnv ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 )
10 df-br ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
11 9 10 bitr3i ( 𝑦 𝑅 𝑥 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
12 6 11 anbi12i ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
13 5 12 bitr4i ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 𝑅 ) ↔ ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) )
14 df-br ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
15 8 ideq ( 𝑥 I 𝑦𝑥 = 𝑦 )
16 14 15 bitr3i ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ↔ 𝑥 = 𝑦 )
17 13 16 imbi12i ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 𝑅 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
18 17 2albii ( ∀ 𝑥𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 𝑅 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ∀ 𝑥𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
19 4 18 bitri ( ( 𝑅 𝑅 ) ⊆ I ↔ ∀ 𝑥𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )