Theorem hash2sspr

Description: A subset of size two is an unordered pair of elements of its superset. (Contributed by Alexander van der Vekens, 12-Jul-2017) (Proof shortened by AV, 4-Nov-2020)

	Ref	Expression
Assertion	hash2sspr	⊢ ( ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝑝 = 𝑃 → ( ( ♯ ‘ 𝑝 ) = 2 ↔ ( ♯ ‘ 𝑃 ) = 2 ) )
2	1	elrab	⊢ ( 𝑃 ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } ↔ ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) )
3		elss2prb	⊢ ( 𝑃 ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) )
4		simpr	⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) → 𝑃 = { 𝑎 , 𝑏 } )
5	4	reximi	⊢ ( ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) → ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } )
6	5	reximi	⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } )
7	3 6	sylbi	⊢ ( 𝑃 ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 } → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } )
8	2 7	sylbir	⊢ ( ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } )