cotrgOLD

Description: Obsolete version of cotrg as of 29-Dec-2024. (Contributed by NM, 27-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011) Generalized from its special instance cotr . (Revised by Richard Penner, 24-Dec-2019) (Proof shortened by SN, 19-Dec-2024) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	cotrgOLD	$⊢ A \circ B \subseteq C \leftrightarrow \forall x \forall y \forall z ((x B y \land y A z) \to x C z)$

Proof

Step	Hyp	Ref	Expression
1		relco	$⊢ Rel (A \circ B)$
2		ssrel3	$⊢ Rel (A \circ B) \to (A \circ B \subseteq C \leftrightarrow \forall x \forall z (x (A \circ B) z \to x C z))$
3	1 2	ax-mp	$⊢ A \circ B \subseteq C \leftrightarrow \forall x \forall z (x (A \circ B) z \to x C z)$
4		vex	$⊢ x \in V$
5		vex	$⊢ z \in V$
6	4 5	brco	$⊢ x (A \circ B) z \leftrightarrow \exists y (x B y \land y A z)$
7	6	imbi1i	$⊢ (x (A \circ B) z \to x C z) \leftrightarrow (\exists y (x B y \land y A z) \to x C z)$
8		19.23v	$⊢ \forall y ((x B y \land y A z) \to x C z) \leftrightarrow (\exists y (x B y \land y A z) \to x C z)$
9	7 8	bitr4i	$⊢ (x (A \circ B) z \to x C z) \leftrightarrow \forall y ((x B y \land y A z) \to x C z)$
10	9	albii	$⊢ \forall z (x (A \circ B) z \to x C z) \leftrightarrow \forall z \forall y ((x B y \land y A z) \to x C z)$
11		alcom	$⊢ \forall z \forall y ((x B y \land y A z) \to x C z) \leftrightarrow \forall y \forall z ((x B y \land y A z) \to x C z)$
12	10 11	bitri	$⊢ \forall z (x (A \circ B) z \to x C z) \leftrightarrow \forall y \forall z ((x B y \land y A z) \to x C z)$
13	12	albii	$⊢ \forall x \forall z (x (A \circ B) z \to x C z) \leftrightarrow \forall x \forall y \forall z ((x B y \land y A z) \to x C z)$
14	3 13	bitri	$⊢ A \circ B \subseteq C \leftrightarrow \forall x \forall y \forall z ((x B y \land y A z) \to x C z)$

Metamath Proof Explorer

Theorem cotrgOLD

Proof