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 ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → 2 ≤ ( ♯ ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2 elex ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
3 id ⊢ ( 𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵 )
4 hashprb ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
5 4 biimpi ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
6 1 2 3 5 syl3an ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
7 6 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 ∈ 𝑈 ) ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
8 hashss ⊢ ( ( 𝐶 ∈ 𝑈 ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) ≤ ( ♯ ‘ 𝐶 ) )
9 8 adantll ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 ∈ 𝑈 ) ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) ≤ ( ♯ ‘ 𝐶 ) )
10 7 9 eqbrtrrd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 ∈ 𝑈 ) ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → 2 ≤ ( ♯ ‘ 𝐶 ) )
11 10 ex ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 , 𝐵 } ⊆ 𝐶 → 2 ≤ ( ♯ ‘ 𝐶 ) ) )