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 dfss2 ⊢A⊆C↔∀xx∈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→∀xx∈A→x∈C
14 biimpr ⊢A⊆C↔∀xx∈A→x∈C→∀xx∈A→x∈C→A⊆C
15 1 13 14 mpsyl ⊢A⊆B∧B⊆C→A⊆C