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

Metamath Proof Explorer

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