Theorem trressn

Description: Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 ) is transitive, see also trrelressn . (Contributed by Peter Mazsa, 16-Jun-2024)

	Ref	Expression
Assertion	trressn	|- A. x A. y A. z ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) z ) -> x ( R |` { A } ) z )

Proof

Step	Hyp	Ref	Expression
1		an3	|- ( ( ( x = A /\ A R y ) /\ ( y = A /\ A R z ) ) -> ( x = A /\ A R z ) )
2		eqbrb	|- ( ( x = A /\ x R y ) <-> ( x = A /\ A R y ) )
3		eqbrb	|- ( ( y = A /\ y R z ) <-> ( y = A /\ A R z ) )
4	2 3	anbi12i	|- ( ( ( x = A /\ x R y ) /\ ( y = A /\ y R z ) ) <-> ( ( x = A /\ A R y ) /\ ( y = A /\ A R z ) ) )
5		eqbrb	|- ( ( x = A /\ x R z ) <-> ( x = A /\ A R z ) )
6	1 4 5	3imtr4i	|- ( ( ( x = A /\ x R y ) /\ ( y = A /\ y R z ) ) -> ( x = A /\ x R z ) )
7		brressn	|- ( ( x e. _V /\ y e. _V ) -> ( x ( R |` { A } ) y <-> ( x = A /\ x R y ) ) )
8	7	el2v	|- ( x ( R |` { A } ) y <-> ( x = A /\ x R y ) )
9		brressn	|- ( ( y e. _V /\ z e. _V ) -> ( y ( R |` { A } ) z <-> ( y = A /\ y R z ) ) )
10	9	el2v	|- ( y ( R |` { A } ) z <-> ( y = A /\ y R z ) )
11	8 10	anbi12i	|- ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) z ) <-> ( ( x = A /\ x R y ) /\ ( y = A /\ y R z ) ) )
12		brressn	|- ( ( x e. _V /\ z e. _V ) -> ( x ( R |` { A } ) z <-> ( x = A /\ x R z ) ) )
13	12	el2v	|- ( x ( R |` { A } ) z <-> ( x = A /\ x R z ) )
14	6 11 13	3imtr4i	|- ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) z ) -> x ( R |` { A } ) z )
15	14	gen2	|- A. y A. z ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) z ) -> x ( R |` { A } ) z )
16	15	ax-gen	|- A. x A. y A. z ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) z ) -> x ( R |` { A } ) z )