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 ( ( 𝑃𝑉𝑃 ≠ ∅ ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 ↔ ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) )

Proof

Step Hyp Ref Expression
1 hashxnn0 ( 𝑃𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0* )
2 xnn0le2is012 ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0* ∧ ( ♯ ‘ 𝑃 ) ≤ 2 ) → ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) )
3 1 2 sylan ( ( 𝑃𝑉 ∧ ( ♯ ‘ 𝑃 ) ≤ 2 ) → ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) )
4 3 ex ( 𝑃𝑉 → ( ( ♯ ‘ 𝑃 ) ≤ 2 → ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) ) )
5 hasheq0 ( 𝑃𝑉 → ( ( ♯ ‘ 𝑃 ) = 0 ↔ 𝑃 = ∅ ) )
6 eqneqall ( 𝑃 = ∅ → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) )
7 5 6 syl6bi ( 𝑃𝑉 → ( ( ♯ ‘ 𝑃 ) = 0 → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) )
8 7 com12 ( ( ♯ ‘ 𝑃 ) = 0 → ( 𝑃𝑉 → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) )
9 hash1snb ( 𝑃𝑉 → ( ( ♯ ‘ 𝑃 ) = 1 ↔ ∃ 𝑐 𝑃 = { 𝑐 } ) )
10 vex 𝑐 ∈ V
11 preq12 ( ( 𝑎 = 𝑐𝑏 = 𝑐 ) → { 𝑎 , 𝑏 } = { 𝑐 , 𝑐 } )
12 dfsn2 { 𝑐 } = { 𝑐 , 𝑐 }
13 11 12 eqtr4di ( ( 𝑎 = 𝑐𝑏 = 𝑐 ) → { 𝑎 , 𝑏 } = { 𝑐 } )
14 13 eqeq2d ( ( 𝑎 = 𝑐𝑏 = 𝑐 ) → ( 𝑃 = { 𝑎 , 𝑏 } ↔ 𝑃 = { 𝑐 } ) )
15 10 10 14 spc2ev ( 𝑃 = { 𝑐 } → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } )
16 15 exlimiv ( ∃ 𝑐 𝑃 = { 𝑐 } → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } )
17 9 16 syl6bi ( 𝑃𝑉 → ( ( ♯ ‘ 𝑃 ) = 1 → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) )
18 17 imp ( ( 𝑃𝑉 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } )
19 18 a1d ( ( 𝑃𝑉 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) )
20 19 expcom ( ( ♯ ‘ 𝑃 ) = 1 → ( 𝑃𝑉 → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) )
21 hash2pr ( ( 𝑃𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } )
22 21 a1d ( ( 𝑃𝑉 ∧ ( ♯ ‘ 𝑃 ) = 2 ) → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) )
23 22 expcom ( ( ♯ ‘ 𝑃 ) = 2 → ( 𝑃𝑉 → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) )
24 8 20 23 3jaoi ( ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) → ( 𝑃𝑉 → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) )
25 24 com12 ( 𝑃𝑉 → ( ( ( ♯ ‘ 𝑃 ) = 0 ∨ ( ♯ ‘ 𝑃 ) = 1 ∨ ( ♯ ‘ 𝑃 ) = 2 ) → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) )
26 4 25 syld ( 𝑃𝑉 → ( ( ♯ ‘ 𝑃 ) ≤ 2 → ( 𝑃 ≠ ∅ → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) )
27 26 com23 ( 𝑃𝑉 → ( 𝑃 ≠ ∅ → ( ( ♯ ‘ 𝑃 ) ≤ 2 → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) ) )
28 27 imp ( ( 𝑃𝑉𝑃 ≠ ∅ ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 → ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) )
29 fveq2 ( 𝑃 = { 𝑎 , 𝑏 } → ( ♯ ‘ 𝑃 ) = ( ♯ ‘ { 𝑎 , 𝑏 } ) )
30 hashprlei ( { 𝑎 , 𝑏 } ∈ Fin ∧ ( ♯ ‘ { 𝑎 , 𝑏 } ) ≤ 2 )
31 30 simpri ( ♯ ‘ { 𝑎 , 𝑏 } ) ≤ 2
32 29 31 eqbrtrdi ( 𝑃 = { 𝑎 , 𝑏 } → ( ♯ ‘ 𝑃 ) ≤ 2 )
33 32 exlimivv ( ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } → ( ♯ ‘ 𝑃 ) ≤ 2 )
34 28 33 impbid1 ( ( 𝑃𝑉𝑃 ≠ ∅ ) → ( ( ♯ ‘ 𝑃 ) ≤ 2 ↔ ∃ 𝑎𝑏 𝑃 = { 𝑎 , 𝑏 } ) )