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

Metamath Proof Explorer

Theorem asymref

Description: Two ways of saying a relation is antisymmetric and reflexive. U. U. R is the field of a relation by relfld . (Contributed by NM, 6-May-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion asymref ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ↔ ∀ 𝑥 ∈ ∪ ∪ 𝑅 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 df-br ⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 opeluu ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑦 ∈ ∪ ∪ 𝑅 ) )
5 1 4 sylbi ⊢ ( 𝑥 𝑅 𝑦 → ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑦 ∈ ∪ ∪ 𝑅 ) )
6 5 simpld ⊢ ( 𝑥 𝑅 𝑦 → 𝑥 ∈ ∪ ∪ 𝑅 )
7 6 adantr ⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 ∈ ∪ ∪ 𝑅 )
8 7 pm4.71ri ⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
9 8 bibi1i ⊢ ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) ) ↔ ( ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) ) )
10 elin ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 ) )
11 2 3 brcnv ⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
12 df-br ⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 )
13 11 12 bitr3i ⊢ ( 𝑦 𝑅 𝑥 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 )
14 1 13 anbi12i ⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ 𝑅 ) )
15 10 14 bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) )
16 3 opelresi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) )
17 df-br ⊢ ( 𝑥 I 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ I )
18 3 ideq ⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
19 17 18 bitr3i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ I ↔ 𝑥 = 𝑦 )
20 19 anbi2i ⊢ ( ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ I ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) )
21 16 20 bitri ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) )
22 15 21 bibi12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) ) )
23 pm5.32 ⊢ ( ( 𝑥 ∈ ∪ ∪ 𝑅 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) ↔ ( ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 ∧ 𝑥 = 𝑦 ) ) )
24 9 22 23 3bitr4i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
25 24 albii ⊢ ( ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ∀ 𝑦 ( 𝑥 ∈ ∪ ∪ 𝑅 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
26 19.21v ⊢ ( ∀ 𝑦 ( 𝑥 ∈ ∪ ∪ 𝑅 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
27 25 26 bitri ⊢ ( ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ( 𝑥 ∈ ∪ ∪ 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
28 27 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ ∪ 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
29 relcnv ⊢ Rel ◡ 𝑅
30 relin2 ⊢ ( Rel ◡ 𝑅 → Rel ( 𝑅 ∩ ◡ 𝑅 ) )
31 29 30 ax-mp ⊢ Rel ( 𝑅 ∩ ◡ 𝑅 )
32 relres ⊢ Rel ( I ↾ ∪ ∪ 𝑅 )
33 eqrel ⊢ ( ( Rel ( 𝑅 ∩ ◡ 𝑅 ) ∧ Rel ( I ↾ ∪ ∪ 𝑅 ) ) → ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) ) )
34 31 32 33 mp2an ⊢ ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∩ ◡ 𝑅 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( I ↾ ∪ ∪ 𝑅 ) ) )
35 df-ral ⊢ ( ∀ 𝑥 ∈ ∪ ∪ 𝑅 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ∪ ∪ 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ) )
36 28 34 35 3bitr4i ⊢ ( ( 𝑅 ∩ ◡ 𝑅 ) = ( I ↾ ∪ ∪ 𝑅 ) ↔ ∀ 𝑥 ∈ ∪ ∪ 𝑅 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) )