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 ) → ∃ 𝑎𝑏 ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) )