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 ≤ ( ♯ ‘ 𝐶 ) ) )