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

Metamath Proof Explorer

Theorem nehash2

Description: The cardinality of a set with two distinct elements. (Contributed by Thierry Arnoux, 27-Aug-2019)

Ref Expression
Hypotheses nehash2.p 
|- ( ph -> P e. V )
nehash2.a 
|- ( ph -> A e. P )
nehash2.b 
|- ( ph -> B e. P )
nehash2.1 
|- ( ph -> A =/= B )
Assertion nehash2 
|- ( ph -> 2 <_ ( # ` P ) )

Proof

Step Hyp Ref Expression
1 nehash2.p 
 |-  ( ph -> P e. V )
2 nehash2.a 
 |-  ( ph -> A e. P )
3 nehash2.b 
 |-  ( ph -> B e. P )
4 nehash2.1 
 |-  ( ph -> A =/= B )
5 hashprg 
 |-  ( ( A e. P /\ B e. P ) -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )
6 2 3 5 syl2anc 
 |-  ( ph -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )
7 4 6 mpbid 
 |-  ( ph -> ( # ` { A , B } ) = 2 )
8 2 3 prssd 
 |-  ( ph -> { A , B } C_ P )
9 hashss 
 |-  ( ( P e. V /\ { A , B } C_ P ) -> ( # ` { A , B } ) <_ ( # ` P ) )
10 1 8 9 syl2anc 
 |-  ( ph -> ( # ` { A , B } ) <_ ( # ` P ) )
11 7 10 eqbrtrrd 
 |-  ( ph -> 2 <_ ( # ` P ) )