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 C_ B /\ B C_ C ) -> A C_ C )

Proof

Step Hyp Ref Expression
1 df-ss 
 |-  ( A C_ C <-> A. x ( x e. A -> x e. C ) )
2 idn1 
 |-  (. ( A C_ B /\ B C_ C ) ->. ( A C_ B /\ B C_ C ) ).
3 simpr 
 |-  ( ( A C_ B /\ B C_ C ) -> B C_ C )
4 2 3 e1a 
 |-  (. ( A C_ B /\ B C_ C ) ->. B C_ C ).
5 simpl 
 |-  ( ( A C_ B /\ B C_ C ) -> A C_ B )
6 2 5 e1a 
 |-  (. ( A C_ B /\ B C_ C ) ->. A C_ B ).
7 idn2 
 |-  (. ( A C_ B /\ B C_ C ) ,. x e. A ->. x e. A ).
8 ssel2 
 |-  ( ( A C_ B /\ x e. A ) -> x e. B )
9 6 7 8 e12an 
 |-  (. ( A C_ B /\ B C_ C ) ,. x e. A ->. x e. B ).
10 ssel2 
 |-  ( ( B C_ C /\ x e. B ) -> x e. C )
11 4 9 10 e12an 
 |-  (. ( A C_ B /\ B C_ C ) ,. x e. A ->. x e. C ).
12 11 in2 
 |-  (. ( A C_ B /\ B C_ C ) ->. ( x e. A -> x e. C ) ).
13 12 gen11 
 |-  (. ( A C_ B /\ B C_ C ) ->. A. x ( x e. A -> x e. C ) ).
14 biimpr 
 |-  ( ( A C_ C <-> A. x ( x e. A -> x e. C ) ) -> ( A. x ( x e. A -> x e. C ) -> A C_ C ) )
15 1 13 14 e01 
 |-  (. ( A C_ B /\ B C_ C ) ->. A C_ C ).
16 15 in1 
 |-  ( ( A C_ B /\ B C_ C ) -> A C_ C )