Metamath Proof Explorer

Theorem elss2prb

Description: An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion elss2prb ( 𝑃 ∈ { 𝑧 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑧 ) = 2 } ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) )

Proof

Step Hyp Ref Expression
1 fveqeq2 ⊢ ( 𝑧 = 𝑃 → ( ( ♯ ‘ 𝑧 ) = 2 ↔ ( ♯ ‘ 𝑃 ) = 2 ) )
2 1 elrab ⊢ ( 𝑃 ∈ { 𝑧 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑧 ) = 2 } ↔ ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) )
3 hash2prb ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ( ♯ ‘ 𝑃 ) = 2 ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) )
4 elpwi ⊢ ( 𝑃 ∈ 𝒫 𝑉 → 𝑃 ⊆ 𝑉 )
5 ssrexv ⊢ ( 𝑃 ⊆ 𝑉 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) )
6 4 5 syl ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) )
7 ssrexv ⊢ ( 𝑃 ⊆ 𝑉 → ( ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) )
8 4 7 syl ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) )
9 8 reximdv ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) )
10 6 9 syld ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) )
11 3 10 sylbid ⊢ ( 𝑃 ∈ 𝒫 𝑉 → ( ( ♯ ‘ 𝑃 ) = 2 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) )
12 11 imp ⊢ ( ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) )
13 prelpwi ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → { 𝑥 , 𝑦 } ∈ 𝒫 𝑉 )
14 13 adantr ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) → { 𝑥 , 𝑦 } ∈ 𝒫 𝑉 )
15 eleq1 ⊢ ( 𝑃 = { 𝑥 , 𝑦 } → ( 𝑃 ∈ 𝒫 𝑉 ↔ { 𝑥 , 𝑦 } ∈ 𝒫 𝑉 ) )
16 15 ad2antll ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) → ( 𝑃 ∈ 𝒫 𝑉 ↔ { 𝑥 , 𝑦 } ∈ 𝒫 𝑉 ) )
17 14 16 mpbird ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) → 𝑃 ∈ 𝒫 𝑉 )
18 fveq2 ⊢ ( 𝑃 = { 𝑥 , 𝑦 } → ( ♯ ‘ 𝑃 ) = ( ♯ ‘ { 𝑥 , 𝑦 } ) )
19 18 ad2antll ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) → ( ♯ ‘ 𝑃 ) = ( ♯ ‘ { 𝑥 , 𝑦 } ) )
20 hashprg ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 ≠ 𝑦 ↔ ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 ) )
21 20 biimpcd ⊢ ( 𝑥 ≠ 𝑦 → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 ) )
22 21 adantr ⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 ) )
23 22 impcom ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) → ( ♯ ‘ { 𝑥 , 𝑦 } ) = 2 )
24 19 23 eqtrd ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) → ( ♯ ‘ 𝑃 ) = 2 )
25 17 24 jca ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) ) → ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) )
26 25 ex ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) ) )
27 26 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) → ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) )
28 12 27 impbii ⊢ ( ( 𝑃 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) )
29 2 28 bitri ⊢ ( 𝑃 ∈ { 𝑧 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑧 ) = 2 } ↔ ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ( 𝑥 ≠ 𝑦 ∧ 𝑃 = { 𝑥 , 𝑦 } ) )