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 ( 𝑅 ↾ { 𝐴 } ) ) 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑥 )