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

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