Metamath Proof Explorer

Theorem hash2prde

Description: A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017)

Ref Expression
Assertion hash2prde ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) )

Proof

Step Hyp Ref Expression
1 hash2pr ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ∃ 𝑎 ∃ 𝑏 𝑉 = { 𝑎 , 𝑏 } )
2 equid ⊢ 𝑏 = 𝑏
3 vex ⊢ 𝑎 ∈ V
4 vex ⊢ 𝑏 ∈ V
5 3 4 preqsn ⊢ ( { 𝑎 , 𝑏 } = { 𝑏 } ↔ ( 𝑎 = 𝑏 ∧ 𝑏 = 𝑏 ) )
6 eqeq2 ⊢ ( { 𝑎 , 𝑏 } = { 𝑏 } → ( 𝑉 = { 𝑎 , 𝑏 } ↔ 𝑉 = { 𝑏 } ) )
7 fveq2 ⊢ ( 𝑉 = { 𝑏 } → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝑏 } ) )
8 hashsng ⊢ ( 𝑏 ∈ V → ( ♯ ‘ { 𝑏 } ) = 1 )
9 8 elv ⊢ ( ♯ ‘ { 𝑏 } ) = 1
10 7 9 eqtrdi ⊢ ( 𝑉 = { 𝑏 } → ( ♯ ‘ 𝑉 ) = 1 )
11 eqeq1 ⊢ ( ( ♯ ‘ 𝑉 ) = 2 → ( ( ♯ ‘ 𝑉 ) = 1 ↔ 2 = 1 ) )
12 1ne2 ⊢ 1 ≠ 2
13 df-ne ⊢ ( 1 ≠ 2 ↔ ¬ 1 = 2 )
14 pm2.21 ⊢ ( ¬ 1 = 2 → ( 1 = 2 → 𝑎 ≠ 𝑏 ) )
15 13 14 sylbi ⊢ ( 1 ≠ 2 → ( 1 = 2 → 𝑎 ≠ 𝑏 ) )
16 12 15 ax-mp ⊢ ( 1 = 2 → 𝑎 ≠ 𝑏 )
17 16 eqcoms ⊢ ( 2 = 1 → 𝑎 ≠ 𝑏 )
18 11 17 syl6bi ⊢ ( ( ♯ ‘ 𝑉 ) = 2 → ( ( ♯ ‘ 𝑉 ) = 1 → 𝑎 ≠ 𝑏 ) )
19 18 adantl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ( ( ♯ ‘ 𝑉 ) = 1 → 𝑎 ≠ 𝑏 ) )
20 10 19 syl5com ⊢ ( 𝑉 = { 𝑏 } → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) → 𝑎 ≠ 𝑏 ) )
21 6 20 syl6bi ⊢ ( { 𝑎 , 𝑏 } = { 𝑏 } → ( 𝑉 = { 𝑎 , 𝑏 } → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) → 𝑎 ≠ 𝑏 ) ) )
22 21 impcomd ⊢ ( { 𝑎 , 𝑏 } = { 𝑏 } → ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → 𝑎 ≠ 𝑏 ) )
23 5 22 sylbir ⊢ ( ( 𝑎 = 𝑏 ∧ 𝑏 = 𝑏 ) → ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → 𝑎 ≠ 𝑏 ) )
24 2 23 mpan2 ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → 𝑎 ≠ 𝑏 ) )
25 ax-1 ⊢ ( 𝑎 ≠ 𝑏 → ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → 𝑎 ≠ 𝑏 ) )
26 24 25 pm2.61ine ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → 𝑎 ≠ 𝑏 )
27 simpr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → 𝑉 = { 𝑎 , 𝑏 } )
28 26 27 jca ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) )
29 28 ex ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )
30 29 2eximdv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ( ∃ 𝑎 ∃ 𝑏 𝑉 = { 𝑎 , 𝑏 } → ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )
31 1 30 mpd ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) )