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	$⊢ \forall x \forall y \forall z ((x ({R ↾}_{\{A\}}) y \land y ({R ↾}_{\{A\}}) z) \to x ({R ↾}_{\{A\}}) z)$

Proof

Step	Hyp	Ref	Expression
1		an3	$⊢ ((x = A \land A R y) \land (y = A \land A R z)) \to (x = A \land A R z)$
2		eqbrb	$⊢ (x = A \land x R y) \leftrightarrow (x = A \land A R y)$
3		eqbrb	$⊢ (y = A \land y R z) \leftrightarrow (y = A \land A R z)$
4	2 3	anbi12i	$⊢ ((x = A \land x R y) \land (y = A \land y R z)) \leftrightarrow ((x = A \land A R y) \land (y = A \land A R z))$
5		eqbrb	$⊢ (x = A \land x R z) \leftrightarrow (x = A \land A R z)$
6	1 4 5	3imtr4i	$⊢ ((x = A \land x R y) \land (y = A \land y R z)) \to (x = A \land x R z)$
7		brressn	$⊢ (x \in V \land y \in V) \to (x ({R ↾}_{\{A\}}) y \leftrightarrow (x = A \land x R y))$
8	7	el2v	$⊢ x ({R ↾}_{\{A\}}) y \leftrightarrow (x = A \land x R y)$
9		brressn	$⊢ (y \in V \land z \in V) \to (y ({R ↾}_{\{A\}}) z \leftrightarrow (y = A \land y R z))$
10	9	el2v	$⊢ y ({R ↾}_{\{A\}}) z \leftrightarrow (y = A \land y R z)$
11	8 10	anbi12i	$⊢ (x ({R ↾}_{\{A\}}) y \land y ({R ↾}_{\{A\}}) z) \leftrightarrow ((x = A \land x R y) \land (y = A \land y R z))$
12		brressn	$⊢ (x \in V \land z \in V) \to (x ({R ↾}_{\{A\}}) z \leftrightarrow (x = A \land x R z))$
13	12	el2v	$⊢ x ({R ↾}_{\{A\}}) z \leftrightarrow (x = A \land x R z)$
14	6 11 13	3imtr4i	$⊢ (x ({R ↾}_{\{A\}}) y \land y ({R ↾}_{\{A\}}) z) \to x ({R ↾}_{\{A\}}) z$
15	14	gen2	$⊢ \forall y \forall z ((x ({R ↾}_{\{A\}}) y \land y ({R ↾}_{\{A\}}) z) \to x ({R ↾}_{\{A\}}) z)$
16	15	ax-gen	$⊢ \forall x \forall y \forall z ((x ({R ↾}_{\{A\}}) y \land y ({R ↾}_{\{A\}}) z) \to x ({R ↾}_{\{A\}}) z)$