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	⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑧 ) → 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		an3	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑦 ) ∧ ( 𝑦 = 𝐴 ∧ 𝐴 𝑅 𝑧 ) ) → ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑧 ) )
2		eqbrb	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) ↔ ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑦 ) )
3		eqbrb	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑧 ) ↔ ( 𝑦 = 𝐴 ∧ 𝐴 𝑅 𝑧 ) )
4	2 3	anbi12i	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑦 ) ∧ ( 𝑦 = 𝐴 ∧ 𝐴 𝑅 𝑧 ) ) )
5		eqbrb	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑧 ) ↔ ( 𝑥 = 𝐴 ∧ 𝐴 𝑅 𝑧 ) )
6	1 4 5	3imtr4i	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) → ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑧 ) )
7		brressn	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
8	7	el2v	⊢ ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
9		brressn	⊢ ( ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑧 ↔ ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) )
10	9	el2v	⊢ ( 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑧 ↔ ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑧 ) )
11	8 10	anbi12i	⊢ ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑧 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) ∧ ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑧 ) ) )
12		brressn	⊢ ( ( 𝑥 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑧 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) )
13	12	el2v	⊢ ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑧 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑧 ) )
14	6 11 13	3imtr4i	⊢ ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑧 ) → 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑧 )
15	14	gen2	⊢ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑧 ) → 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑧 )
16	15	ax-gen	⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑧 ) → 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑧 )