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 ∃ b P = a b

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 ∃ b P = a b
7 5 6 syl6bi ⊢ P ∈ V → P = 0 → P ≠ ∅ → ∃ a ∃ b P = a b
8 7 com12 ⊢ P = 0 → P ∈ V → P ≠ ∅ → ∃ a ∃ b P = a b
9 hash1snb ⊢ P ∈ V → P = 1 ↔ ∃ c P = c
10 vex ⊢ c ∈ V
11 preq12 ⊢ a = c ∧ b = c → a b = c c
12 dfsn2 ⊢ c = c c
13 11 12 eqtr4di ⊢ a = c ∧ b = c → a b = c
14 13 eqeq2d ⊢ a = c ∧ b = c → P = a b ↔ P = c
15 10 10 14 spc2ev ⊢ P = c → ∃ a ∃ b P = a b
16 15 exlimiv ⊢ ∃ c P = c → ∃ a ∃ b P = a b
17 9 16 syl6bi ⊢ P ∈ V → P = 1 → ∃ a ∃ b P = a b
18 17 imp ⊢ P ∈ V ∧ P = 1 → ∃ a ∃ b P = a b
19 18 a1d ⊢ P ∈ V ∧ P = 1 → P ≠ ∅ → ∃ a ∃ b P = a b
20 19 expcom ⊢ P = 1 → P ∈ V → P ≠ ∅ → ∃ a ∃ b P = a b
21 hash2pr ⊢ P ∈ V ∧ P = 2 → ∃ a ∃ b P = a b
22 21 a1d ⊢ P ∈ V ∧ P = 2 → P ≠ ∅ → ∃ a ∃ b P = a b
23 22 expcom ⊢ P = 2 → P ∈ V → P ≠ ∅ → ∃ a ∃ b P = a b
24 8 20 23 3jaoi ⊢ P = 0 ∨ P = 1 ∨ P = 2 → P ∈ V → P ≠ ∅ → ∃ a ∃ b P = a b
25 24 com12 ⊢ P ∈ V → P = 0 ∨ P = 1 ∨ P = 2 → P ≠ ∅ → ∃ a ∃ b P = a b
26 4 25 syld ⊢ P ∈ V → P ≤ 2 → P ≠ ∅ → ∃ a ∃ b P = a b
27 26 com23 ⊢ P ∈ V → P ≠ ∅ → P ≤ 2 → ∃ a ∃ b P = a b
28 27 imp ⊢ P ∈ V ∧ P ≠ ∅ → P ≤ 2 → ∃ a ∃ b P = a b
29 fveq2 ⊢ P = a b → P = a b
30 hashprlei ⊢ a b ∈ Fin ∧ a b ≤ 2
31 30 simpri ⊢ a b ≤ 2
32 29 31 eqbrtrdi ⊢ P = a b → P ≤ 2
33 32 exlimivv ⊢ ∃ a ∃ b P = a b → P ≤ 2
34 28 33 impbid1 ⊢ P ∈ V ∧ P ≠ ∅ → P ≤ 2 ↔ ∃ a ∃ b P = a b