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