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

Metamath Proof Explorer

Theorem antisymressn

Description: Every class ' R ' restricted to the singleton of the class ' A ' (see ressn2 ) is antisymmetric. (Contributed by Peter Mazsa, 11-Jun-2024)

Ref Expression
Assertion antisymressn ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ) → 𝑥 = 𝑦 )

Proof

Step Hyp Ref Expression
1 brressn ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
2 1 el2v ⊢ ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
3 2 simplbi ⊢ ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 → 𝑥 = 𝐴 )
4 brressn ⊢ ( ( 𝑦 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ↔ ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑥 ) ) )
5 4 el2v ⊢ ( 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ↔ ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑥 ) )
6 5 simplbi ⊢ ( 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 → 𝑦 = 𝐴 )
7 eqtr3 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → 𝑥 = 𝑦 )
8 3 6 7 syl2an ⊢ ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ) → 𝑥 = 𝑦 )
9 8 gen2 ⊢ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ) → 𝑥 = 𝑦 )