Theorem sstrALT2

Description: Virtual deduction proof of sstr , transitivity of subclasses, Theorem 6 of Suppes p. 23. This theorem was automatically generated from sstrALT2VD using the command file translate__without__overwriting.cmd . It was not minimized because the automated minimization excluding duplicates generates a minimized proof which, although not directly containing any duplicates, indirectly contains a duplicate. That is, the trace back of the minimized proof contains a duplicate. This is undesirable because some step(s) of the minimized proof use the proven theorem. (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sstrALT2	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐴 ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		dfss2	⊢ ( 𝐴 ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
2		id	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) )
3		simpr	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐵 ⊆ 𝐶 )
4	2 3	syl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐵 ⊆ 𝐶 )
5		simpl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐴 ⊆ 𝐵 )
6	2 5	syl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐴 ⊆ 𝐵 )
7		idd	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴 ) )
8		ssel2	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
9	6 7 8	syl6an	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
10		ssel2	⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐶 )
11	4 9 10	syl6an	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
12	11	idiALT	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
13	12	alrimiv	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) )
14		biimpr	⊢ ( ( 𝐴 ⊆ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶 ) → 𝐴 ⊆ 𝐶 ) )
15	1 13 14	mpsyl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝐴 ⊆ 𝐶 )