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 ⊢V∈W∧V=2→∃a∃ba≠b∧V=ab

Proof

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