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 ) )