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

Metamath Proof Explorer

Theorem refressn

Description: Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 ) is reflexive, see also refrelressn . (Contributed by Peter Mazsa, 12-Jun-2024)

Ref Expression
Assertion refressn ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑥 )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) ↔ ( 𝑥 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ∧ 𝑥 ∈ ran ( 𝑅 ↾ { 𝐴 } ) ) )
2 eldmressnALTV ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ↔ ( 𝑥 = 𝐴 ∧ 𝐴 ∈ dom 𝑅 ) ) )
3 2 elv ⊢ ( 𝑥 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ↔ ( 𝑥 = 𝐴 ∧ 𝐴 ∈ dom 𝑅 ) )
4 3 simplbi ⊢ ( 𝑥 ∈ dom ( 𝑅 ↾ { 𝐴 } ) → 𝑥 = 𝐴 )
5 4 adantr ⊢ ( ( 𝑥 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ∧ 𝑥 ∈ ran ( 𝑅 ↾ { 𝐴 } ) ) → 𝑥 = 𝐴 )
6 1 5 sylbi ⊢ ( 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) → 𝑥 = 𝐴 )
7 6 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) → 𝑥 = 𝐴 ) )
8 elrnressn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ran ( 𝑅 ↾ { 𝐴 } ) ↔ 𝐴 𝑅 𝑥 ) )
9 8 elvd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ran ( 𝑅 ↾ { 𝐴 } ) ↔ 𝐴 𝑅 𝑥 ) )
10 9 biimpd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ran ( 𝑅 ↾ { 𝐴 } ) → 𝐴 𝑅 𝑥 ) )
11 10 adantld ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ∧ 𝑥 ∈ ran ( 𝑅 ↾ { 𝐴 } ) ) → 𝐴 𝑅 𝑥 ) )
12 1 11 biimtrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) → 𝐴 𝑅 𝑥 ) )
13 4 eqcomd ⊢ ( 𝑥 ∈ dom ( 𝑅 ↾ { 𝐴 } ) → 𝐴 = 𝑥 )
14 13 breq1d ⊢ ( 𝑥 ∈ dom ( 𝑅 ↾ { 𝐴 } ) → ( 𝐴 𝑅 𝑥 ↔ 𝑥 𝑅 𝑥 ) )
15 14 adantr ⊢ ( ( 𝑥 ∈ dom ( 𝑅 ↾ { 𝐴 } ) ∧ 𝑥 ∈ ran ( 𝑅 ↾ { 𝐴 } ) ) → ( 𝐴 𝑅 𝑥 ↔ 𝑥 𝑅 𝑥 ) )
16 1 15 sylbi ⊢ ( 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) → ( 𝐴 𝑅 𝑥 ↔ 𝑥 𝑅 𝑥 ) )
17 12 16 mpbidi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) → 𝑥 𝑅 𝑥 ) )
18 7 17 jcad ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) → ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑥 ) ) )
19 brressn ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑥 ) ) )
20 19 el2v ⊢ ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑥 ) )
21 18 20 imbitrrdi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) → 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ) )
22 21 ralrimiv ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ ( dom ( 𝑅 ↾ { 𝐴 } ) ∩ ran ( 𝑅 ↾ { 𝐴 } ) ) 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑥 )