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 
|- ( A e. V -> A. x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) x ( R |` { A } ) x )

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) <-> ( x e. dom ( R |` { A } ) /\ x e. ran ( R |` { A } ) ) )
2 eldmressnALTV 
 |-  ( x e. _V -> ( x e. dom ( R |` { A } ) <-> ( x = A /\ A e. dom R ) ) )
3 2 elv 
 |-  ( x e. dom ( R |` { A } ) <-> ( x = A /\ A e. dom R ) )
4 3 simplbi 
 |-  ( x e. dom ( R |` { A } ) -> x = A )
5 4 adantr 
 |-  ( ( x e. dom ( R |` { A } ) /\ x e. ran ( R |` { A } ) ) -> x = A )
6 1 5 sylbi 
 |-  ( x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) -> x = A )
7 6 a1i 
 |-  ( A e. V -> ( x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) -> x = A ) )
8 elrnressn 
 |-  ( ( A e. V /\ x e. _V ) -> ( x e. ran ( R |` { A } ) <-> A R x ) )
9 8 elvd 
 |-  ( A e. V -> ( x e. ran ( R |` { A } ) <-> A R x ) )
10 9 biimpd 
 |-  ( A e. V -> ( x e. ran ( R |` { A } ) -> A R x ) )
11 10 adantld 
 |-  ( A e. V -> ( ( x e. dom ( R |` { A } ) /\ x e. ran ( R |` { A } ) ) -> A R x ) )
12 1 11 biimtrid 
 |-  ( A e. V -> ( x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) -> A R x ) )
13 4 eqcomd 
 |-  ( x e. dom ( R |` { A } ) -> A = x )
14 13 breq1d 
 |-  ( x e. dom ( R |` { A } ) -> ( A R x <-> x R x ) )
15 14 adantr 
 |-  ( ( x e. dom ( R |` { A } ) /\ x e. ran ( R |` { A } ) ) -> ( A R x <-> x R x ) )
16 1 15 sylbi 
 |-  ( x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) -> ( A R x <-> x R x ) )
17 12 16 mpbidi 
 |-  ( A e. V -> ( x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) -> x R x ) )
18 7 17 jcad 
 |-  ( A e. V -> ( x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) -> ( x = A /\ x R x ) ) )
19 brressn 
 |-  ( ( x e. _V /\ x e. _V ) -> ( x ( R |` { A } ) x <-> ( x = A /\ x R x ) ) )
20 19 el2v 
 |-  ( x ( R |` { A } ) x <-> ( x = A /\ x R x ) )
21 18 20 imbitrrdi 
 |-  ( A e. V -> ( x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) -> x ( R |` { A } ) x ) )
22 21 ralrimiv 
 |-  ( A e. V -> A. x e. ( dom ( R |` { A } ) i^i ran ( R |` { A } ) ) x ( R |` { A } ) x )