This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 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 biimtrdi ⊢ ( 𝑃 ∈ 𝑉 → ( ( ♯ ‘ 𝑃 ) = 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 ↔ ∃ 𝑎 ∃ 𝑏 𝑃 = { 𝑎 , 𝑏 } ) )