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 12123

Proof

Step Hyp Ref Expression
1 ex-ss 12123
2 3ex 3V
3 2 tpid3 3123
4 1re 1
5 1lt3 1<3
6 4 5 gtneii 31
7 2re 2
8 2lt3 2<3
9 7 8 gtneii 32
10 6 9 nelpri ¬312
11 nelne1 3123¬31212312
12 3 10 11 mp2an 12312
13 12 necomi 12123
14 df-pss 121231212312123
15 1 13 14 mpbir2an 12123