This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑃 = { 𝑎 , 𝑏 } )