Metamath Proof Explorer

Theorem prprelb

Description: An element of the set of all proper unordered pairs over a given set V is a subset of V of size two. (Contributed by AV, 29-Apr-2023)

Ref Expression
Assertion prprelb ( 𝑉 ∈ 𝑊 → ( 𝑃 ∈ ( Pairsproper ‘ 𝑉 ) ↔ ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) ) )

Proof

Step Hyp Ref Expression
1 prprvalpw ⊢ ( 𝑉 ∈ 𝑊 → ( Pairsproper ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } )
2 1 eleq2d ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑃 ∈ ( Pairsproper ‘ 𝑉 ) ↔ 𝑃 ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } ) )
3 eqeq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 = { 𝑎 , 𝑏 } ↔ 𝑃 = { 𝑎 , 𝑏 } ) )
4 3 anbi2d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ↔ ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
5 4 2rexbidv ⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
6 5 elrab ⊢ ( 𝑃 ∈ { 𝑝 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) } ↔ ( 𝑃 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
7 2 6 bitrdi ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑃 ∈ ( Pairsproper ‘ 𝑉 ) ↔ ( 𝑃 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) ) )
8 hash2exprb ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ( ♯ ‘ 𝑃 ) = 2 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
9 eleq1 ⊢ ( 𝑃 = { 𝑎 , 𝑏 } → ( 𝑃 ∈ 𝒫 𝑉 ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ) )
10 prelpw ⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 ) )
11 10 el2v ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ↔ { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 )
12 11 biimpri ⊢ ( { 𝑎 , 𝑏 } ∈ 𝒫 𝑉 → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
13 9 12 syl6bi ⊢ ( 𝑃 = { 𝑎 , 𝑏 } → ( 𝑃 ∈ 𝒫 𝑉 → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
14 13 com12 ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( 𝑃 = { 𝑎 , 𝑏 } → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
15 14 adantld ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
16 15 pm4.71rd ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) ) )
17 16 2exbidv ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) ) )
18 r2ex ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∃ 𝑏 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
19 17 18 bitr4di ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) )
20 8 19 bitr2d ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ↔ ( ♯ ‘ 𝑃 ) = 2 ) )
21 20 pm5.32i ⊢ ( ( 𝑃 ∈ 𝒫 𝑉 ∧ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑃 = { 𝑎 , 𝑏 } ) ) ↔ ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) )
22 7 21 bitrdi ⊢ ( 𝑉 ∈ 𝑊 → ( 𝑃 ∈ ( Pairsproper ‘ 𝑉 ) ↔ ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) ) )