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