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

Metamath Proof Explorer

Theorem prsshashgt1

Description: The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021)

Ref Expression
Assertion prsshashgt1 
|- ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ C e. U ) -> ( { A , B } C_ C -> 2 <_ ( # ` C ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 elex 
 |-  ( B e. W -> B e. _V )
3 id 
 |-  ( A =/= B -> A =/= B )
4 hashprb 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) <-> ( # ` { A , B } ) = 2 )
5 4 biimpi 
 |-  ( ( A e. _V /\ B e. _V /\ A =/= B ) -> ( # ` { A , B } ) = 2 )
6 1 2 3 5 syl3an 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( # ` { A , B } ) = 2 )
7 6 ad2antrr 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ C e. U ) /\ { A , B } C_ C ) -> ( # ` { A , B } ) = 2 )
8 hashss 
 |-  ( ( C e. U /\ { A , B } C_ C ) -> ( # ` { A , B } ) <_ ( # ` C ) )
9 8 adantll 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ C e. U ) /\ { A , B } C_ C ) -> ( # ` { A , B } ) <_ ( # ` C ) )
10 7 9 eqbrtrrd 
 |-  ( ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ C e. U ) /\ { A , B } C_ C ) -> 2 <_ ( # ` C ) )
11 10 ex 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ C e. U ) -> ( { A , B } C_ C -> 2 <_ ( # ` C ) ) )