This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } ⊊ { 1 , 2 , 3 }

Proof

Step Hyp Ref Expression
1 ex-ss ⊢ { 1 , 2 } ⊆ { 1 , 2 , 3 }
2 3ex ⊢ 3 ∈ V
3 2 tpid3 ⊢ 3 ∈ { 1 , 2 , 3 }
4 1re ⊢ 1 ∈ ℝ
5 1lt3 ⊢ 1 < 3
6 4 5 gtneii ⊢ 3 ≠ 1
7 2re ⊢ 2 ∈ ℝ
8 2lt3 ⊢ 2 < 3
9 7 8 gtneii ⊢ 3 ≠ 2
10 6 9 nelpri ⊢ ¬ 3 ∈ { 1 , 2 }
11 nelne1 ⊢ ( ( 3 ∈ { 1 , 2 , 3 } ∧ ¬ 3 ∈ { 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 } ⊊ { 1 , 2 , 3 } ↔ ( { 1 , 2 } ⊆ { 1 , 2 , 3 } ∧ { 1 , 2 } ≠ { 1 , 2 , 3 } ) )
15 1 13 14 mpbir2an ⊢ { 1 , 2 } ⊊ { 1 , 2 , 3 }