Metamath Proof Explorer

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 ⊢ A ⊆ B ∧ B ⊆ C → A ⊆ C

Proof

Step Hyp Ref Expression
1 df-ss ⊢ A ⊆ C ↔ ∀ x x ∈ A → x ∈ C
2 id ⊢ A ⊆ B ∧ B ⊆ C → A ⊆ B ∧ B ⊆ C
3 simpr ⊢ A ⊆ B ∧ B ⊆ C → B ⊆ C
4 2 3 syl ⊢ A ⊆ B ∧ B ⊆ C → B ⊆ C
5 simpl ⊢ A ⊆ B ∧ B ⊆ C → A ⊆ B
6 2 5 syl ⊢ A ⊆ B ∧ B ⊆ C → A ⊆ B
7 idd ⊢ A ⊆ B ∧ B ⊆ C → x ∈ A → x ∈ A
8 ssel2 ⊢ A ⊆ B ∧ x ∈ A → x ∈ B
9 6 7 8 syl6an ⊢ A ⊆ B ∧ B ⊆ C → x ∈ A → x ∈ B
10 ssel2 ⊢ B ⊆ C ∧ x ∈ B → x ∈ C
11 4 9 10 syl6an ⊢ A ⊆ B ∧ B ⊆ C → x ∈ A → x ∈ C
12 11 idiALT ⊢ A ⊆ B ∧ B ⊆ C → x ∈ A → x ∈ C
13 12 alrimiv ⊢ A ⊆ B ∧ B ⊆ C → ∀ x x ∈ A → x ∈ C
14 biimpr ⊢ A ⊆ C ↔ ∀ x x ∈ A → x ∈ C → ∀ x x ∈ A → x ∈ C → A ⊆ C
15 1 13 14 mpsyl ⊢ A ⊆ B ∧ B ⊆ C → A ⊆ C