Metamath Proof Explorer

Theorem sstrALT2VD

Description: Virtual deduction proof of sstrALT2 . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-ss	$⊢ A \subseteq C \leftrightarrow \forall x (x \in A \to x \in C)$
2		idn1	$⊢ ((A \subseteq B \land B \subseteq C) \to (A \subseteq B \land B \subseteq C))$
3		simpr	$⊢ (A \subseteq B \land B \subseteq C) \to B \subseteq C$
4	2 3	e1a	$⊢ ((A \subseteq B \land B \subseteq C) \to B \subseteq C)$
5		simpl	$⊢ (A \subseteq B \land B \subseteq C) \to A \subseteq B$
6	2 5	e1a	$⊢ ((A \subseteq B \land B \subseteq C) \to A \subseteq B)$
7		idn2	$⊢ ((A \subseteq B \land B \subseteq C), x \in A \to x \in A)$
8		ssel2	$⊢ (A \subseteq B \land x \in A) \to x \in B$
9	6 7 8	e12an	$⊢ ((A \subseteq B \land B \subseteq C), x \in A \to x \in B)$
10		ssel2	$⊢ (B \subseteq C \land x \in B) \to x \in C$
11	4 9 10	e12an	$⊢ ((A \subseteq B \land B \subseteq C), x \in A \to x \in C)$
12	11	in2	$⊢ ((A \subseteq B \land B \subseteq C) \to (x \in A \to x \in C))$
13	12	gen11	$⊢ ((A \subseteq B \land B \subseteq C) \to \forall x (x \in A \to x \in C))$
14		biimpr	$⊢ (A \subseteq C \leftrightarrow \forall x (x \in A \to x \in C)) \to (\forall x (x \in A \to x \in C) \to A \subseteq C)$
15	1 13 14	e01	$⊢ ((A \subseteq B \land B \subseteq C) \to A \subseteq C)$
16	15	in1	$⊢ (A \subseteq B \land B \subseteq C) \to A \subseteq C$