Theorem nehash2

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

	Ref	Expression
Hypotheses	nehash2.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
	nehash2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	nehash2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	nehash2.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	nehash2	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		nehash2.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
2		nehash2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
3		nehash2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
4		nehash2.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
5		hashprg	⊢ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ) → ( 𝐴 ≠ 𝐵 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
6	2 3 5	syl2anc	⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
7	4 6	mpbid	⊢ ( 𝜑 → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
8	2 3	prssd	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ 𝑃 )
9		hashss	⊢ ( ( 𝑃 ∈ 𝑉 ∧ { 𝐴 , 𝐵 } ⊆ 𝑃 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) ≤ ( ♯ ‘ 𝑃 ) )
10	1 8 9	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ { 𝐴 , 𝐵 } ) ≤ ( ♯ ‘ 𝑃 ) )
11	7 10	eqbrtrrd	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )