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∈VP=ab

Proof

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