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

Metamath Proof Explorer

Theorem sstr2

Description: Transitivity of subclass relationship. Exercise 5 of TakeutiZaring p. 17. (Contributed by NM, 24-Jun-1993) (Proof shortened by Andrew Salmon, 14-Jun-2011) Avoid axioms. (Revised by GG, 19-May-2025)

		Ref	Expression
	Assertion	sstr2	$⊢ A \subseteq B \to (B \subseteq C \to A \subseteq C)$

Proof

Step	Hyp	Ref	Expression
1		imim1	$⊢ (x \in A \to x \in B) \to ((x \in B \to x \in C) \to (x \in A \to x \in C))$
2	1	al2imi	$⊢ \forall x (x \in A \to x \in B) \to (\forall x (x \in B \to x \in C) \to \forall x (x \in A \to x \in C))$
3		df-ss	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$
4		df-ss	$⊢ B \subseteq C \leftrightarrow \forall x (x \in B \to x \in C)$
5		df-ss	$⊢ A \subseteq C \leftrightarrow \forall x (x \in A \to x \in C)$
6	4 5	imbi12i	$⊢ (B \subseteq C \to A \subseteq C) \leftrightarrow (\forall x (x \in B \to x \in C) \to \forall x (x \in A \to x \in C))$
7	2 3 6	3imtr4i	$⊢ A \subseteq B \to (B \subseteq C \to A \subseteq C)$