Metamath Proof Explorer

Theorem hashle2pr

Description: A nonempty set of size less than or equal to two is an unordered pair of sets. (Contributed by AV, 24-Nov-2021)

Ref Expression
Assertion hashle2pr ⊢P∈V∧P≠∅→P≤2↔∃a∃bP=ab

Proof

Step Hyp Ref Expression
1 hashxnn0 ⊢P∈V→P∈ℕ0*
2 xnn0le2is012 ⊢P∈ℕ0*∧P≤2→P=0∨P=1∨P=2
3 1 2 sylan ⊢P∈V∧P≤2→P=0∨P=1∨P=2
4 3 ex ⊢P∈V→P≤2→P=0∨P=1∨P=2
5 hasheq0 ⊢P∈V→P=0↔P=∅
6 eqneqall ⊢P=∅→P≠∅→∃a∃bP=ab
7 5 6 syl6bi ⊢P∈V→P=0→P≠∅→∃a∃bP=ab
8 7 com12 ⊢P=0→P∈V→P≠∅→∃a∃bP=ab
9 hash1snb ⊢P∈V→P=1↔∃cP=c
10 vex ⊢c∈V
11 preq12 ⊢a=c∧b=c→ab=cc
12 dfsn2 ⊢c=cc
13 11 12 eqtr4di ⊢a=c∧b=c→ab=c
14 13 eqeq2d ⊢a=c∧b=c→P=ab↔P=c
15 10 10 14 spc2ev ⊢P=c→∃a∃bP=ab
16 15 exlimiv ⊢∃cP=c→∃a∃bP=ab
17 9 16 syl6bi ⊢P∈V→P=1→∃a∃bP=ab
18 17 imp ⊢P∈V∧P=1→∃a∃bP=ab
19 18 a1d ⊢P∈V∧P=1→P≠∅→∃a∃bP=ab
20 19 expcom ⊢P=1→P∈V→P≠∅→∃a∃bP=ab
21 hash2pr ⊢P∈V∧P=2→∃a∃bP=ab
22 21 a1d ⊢P∈V∧P=2→P≠∅→∃a∃bP=ab
23 22 expcom ⊢P=2→P∈V→P≠∅→∃a∃bP=ab
24 8 20 23 3jaoi ⊢P=0∨P=1∨P=2→P∈V→P≠∅→∃a∃bP=ab
25 24 com12 ⊢P∈V→P=0∨P=1∨P=2→P≠∅→∃a∃bP=ab
26 4 25 syld ⊢P∈V→P≤2→P≠∅→∃a∃bP=ab
27 26 com23 ⊢P∈V→P≠∅→P≤2→∃a∃bP=ab
28 27 imp ⊢P∈V∧P≠∅→P≤2→∃a∃bP=ab
29 fveq2 ⊢P=ab→P=ab
30 hashprlei ⊢ab∈Fin∧ab≤2
31 30 simpri ⊢ab≤2
32 29 31 eqbrtrdi ⊢P=ab→P≤2
33 32 exlimivv ⊢∃a∃bP=ab→P≤2
34 28 33 impbid1 ⊢P∈V∧P≠∅→P≤2↔∃a∃bP=ab