Metamath Proof Explorer

Theorem hashle2prv

Description: A nonempty subset of a powerset of a class V has size less than or equal to two iff it is an unordered pair of elements of V . (Contributed by AV, 24-Nov-2021)

Ref Expression
Assertion hashle2prv ⊢ P ∈ 𝒫 V ∖ ∅ → P ≤ 2 ↔ ∃ a ∈ V ∃ b ∈ V P = a b

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ P ∈ 𝒫 V ∖ ∅ ↔ P ∈ 𝒫 V ∧ P ≠ ∅
2 hashle2pr ⊢ P ∈ 𝒫 V ∧ P ≠ ∅ → P ≤ 2 ↔ ∃ a ∃ b P = a b
3 1 2 sylbi ⊢ P ∈ 𝒫 V ∖ ∅ → P ≤ 2 ↔ ∃ a ∃ b P = a b
4 eldifi ⊢ P ∈ 𝒫 V ∖ ∅ → P ∈ 𝒫 V
5 eleq1 ⊢ P = a b → P ∈ 𝒫 V ↔ a b ∈ 𝒫 V
6 prelpw ⊢ a ∈ V ∧ b ∈ V → a ∈ V ∧ b ∈ V ↔ a b ∈ 𝒫 V
7 6 biimprd ⊢ a ∈ V ∧ b ∈ V → a b ∈ 𝒫 V → a ∈ V ∧ b ∈ V
8 7 el2v ⊢ a b ∈ 𝒫 V → a ∈ V ∧ b ∈ V
9 5 8 biimtrdi ⊢ P = a b → P ∈ 𝒫 V → a ∈ V ∧ b ∈ V
10 4 9 syl5com ⊢ P ∈ 𝒫 V ∖ ∅ → P = a b → a ∈ V ∧ b ∈ V
11 10 pm4.71rd ⊢ P ∈ 𝒫 V ∖ ∅ → P = a b ↔ a ∈ V ∧ b ∈ V ∧ P = a b
12 11 2exbidv ⊢ P ∈ 𝒫 V ∖ ∅ → ∃ a ∃ b P = a b ↔ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ P = a b
13 r2ex ⊢ ∃ a ∈ V ∃ b ∈ V P = a b ↔ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ P = a b
14 13 bicomi ⊢ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ P = a b ↔ ∃ a ∈ V ∃ b ∈ V P = a b
15 14 a1i ⊢ P ∈ 𝒫 V ∖ ∅ → ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ P = a b ↔ ∃ a ∈ V ∃ b ∈ V P = a b
16 3 12 15 3bitrd ⊢ P ∈ 𝒫 V ∖ ∅ → P ≤ 2 ↔ ∃ a ∈ V ∃ b ∈ V P = a b