Metamath Proof Explorer

Theorem ex-pss

Description: Example for df-pss . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion ex-pss 
|- { 1 , 2 } C. { 1 , 2 , 3 }

Proof

Step Hyp Ref Expression
1 ex-ss 
 |-  { 1 , 2 } C_ { 1 , 2 , 3 }
2 3ex 
 |-  3 e. _V
3 2 tpid3 
 |-  3 e. { 1 , 2 , 3 }
4 1re 
 |-  1 e. RR
5 1lt3 
 |-  1 < 3
6 4 5 gtneii 
 |-  3 =/= 1
7 2re 
 |-  2 e. RR
8 2lt3 
 |-  2 < 3
9 7 8 gtneii 
 |-  3 =/= 2
10 6 9 nelpri 
 |-  -. 3 e. { 1 , 2 }
11 nelne1 
 |-  ( ( 3 e. { 1 , 2 , 3 } /\ -. 3 e. { 1 , 2 } ) -> { 1 , 2 , 3 } =/= { 1 , 2 } )
12 3 10 11 mp2an 
 |-  { 1 , 2 , 3 } =/= { 1 , 2 }
13 12 necomi 
 |-  { 1 , 2 } =/= { 1 , 2 , 3 }
14 df-pss 
 |-  ( { 1 , 2 } C. { 1 , 2 , 3 } <-> ( { 1 , 2 } C_ { 1 , 2 , 3 } /\ { 1 , 2 } =/= { 1 , 2 , 3 } ) )
15 1 13 14 mpbir2an 
 |-  { 1 , 2 } C. { 1 , 2 , 3 }