Metamath Proof Explorer


Theorem asymref2

Description: Two ways of saying a relation is antisymmetric and reflexive. (Contributed by NM, 6-May-2008) (Proof shortened by Mario Carneiro, 4-Dec-2016)

Ref Expression
Assertion asymref2 ( ( 𝑅 𝑅 ) = ( I ↾ 𝑅 ) ↔ ( ∀ 𝑥 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 asymref ( ( 𝑅 𝑅 ) = ( I ↾ 𝑅 ) ↔ ∀ 𝑥 𝑅𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) )
2 albiim ( ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ↔ ( ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ) )
3 2 ralbii ( ∀ 𝑥 𝑅𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 𝑅 ( ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ) )
4 r19.26 ( ∀ 𝑥 𝑅 ( ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ) ↔ ( ∀ 𝑥 𝑅𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 𝑅𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ) )
5 ancom ( ( ∀ 𝑥 𝑅𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 𝑅𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ) ↔ ( ∀ 𝑥 𝑅𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ∧ ∀ 𝑥 𝑅𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) )
6 equcom ( 𝑥 = 𝑦𝑦 = 𝑥 )
7 6 imbi1i ( ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ↔ ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )
8 7 albii ( ∀ 𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) )
9 breq2 ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦𝑥 𝑅 𝑥 ) )
10 breq1 ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑥 ) )
11 9 10 anbi12d ( 𝑦 = 𝑥 → ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑥𝑥 𝑅 𝑥 ) ) )
12 anidm ( ( 𝑥 𝑅 𝑥𝑥 𝑅 𝑥 ) ↔ 𝑥 𝑅 𝑥 )
13 11 12 bitrdi ( 𝑦 = 𝑥 → ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ↔ 𝑥 𝑅 𝑥 ) )
14 13 equsalvw ( ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ↔ 𝑥 𝑅 𝑥 )
15 8 14 bitri ( ∀ 𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ↔ 𝑥 𝑅 𝑥 )
16 15 ralbii ( ∀ 𝑥 𝑅𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ↔ ∀ 𝑥 𝑅 𝑥 𝑅 𝑥 )
17 df-ral ( ∀ 𝑥 𝑅𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝑥 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) )
18 df-br ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
19 vex 𝑥 ∈ V
20 vex 𝑦 ∈ V
21 19 20 opeluu ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ( 𝑥 𝑅𝑦 𝑅 ) )
22 21 simpld ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅𝑥 𝑅 )
23 18 22 sylbi ( 𝑥 𝑅 𝑦𝑥 𝑅 )
24 23 adantr ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 𝑅 )
25 24 pm2.24d ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → ( ¬ 𝑥 𝑅𝑥 = 𝑦 ) )
26 25 com12 ( ¬ 𝑥 𝑅 → ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
27 26 alrimiv ( ¬ 𝑥 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
28 id ( ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
29 27 28 ja ( ( 𝑥 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
30 ax-1 ( ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) → ( 𝑥 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) )
31 29 30 impbii ( ( 𝑥 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) ↔ ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
32 31 albii ( ∀ 𝑥 ( 𝑥 𝑅 → ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) ↔ ∀ 𝑥𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
33 17 32 bitri ( ∀ 𝑥 𝑅𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
34 16 33 anbi12i ( ( ∀ 𝑥 𝑅𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ∧ ∀ 𝑥 𝑅𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑥 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) )
35 4 5 34 3bitri ( ∀ 𝑥 𝑅 ( ∀ 𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑦 ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) ) ) ↔ ( ∀ 𝑥 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) )
36 1 3 35 3bitri ( ( 𝑅 𝑅 ) = ( I ↾ 𝑅 ) ↔ ( ∀ 𝑥 𝑅 𝑥 𝑅 𝑥 ∧ ∀ 𝑥𝑦 ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) ) )