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 ⊢ ( 𝜑 → 𝑃 ∈ 𝑉 )
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 ≤ ( ♯ ‘ 𝑃 ) )