Metamath Proof Explorer

Theorem hash3tpde

Description: A set of size three is an unordered triple of three different elements. (Contributed by AV, 21-Jul-2025)

Ref Expression
Assertion hash3tpde ⊢ V ∈ W ∧ V = 3 → ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c

Proof

Step Hyp Ref Expression
1 hash3tr ⊢ V ∈ W ∧ V = 3 → ∃ a ∃ b ∃ c V = a b c
2 ax-1 ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → V ∈ W ∧ V = 3 ∧ V = a b c → a ≠ b ∧ a ≠ c ∧ b ≠ c
3 3ianor ⊢ ¬ a ≠ b ∧ a ≠ c ∧ b ≠ c ↔ ¬ a ≠ b ∨ ¬ a ≠ c ∨ ¬ b ≠ c
4 nne ⊢ ¬ a ≠ b ↔ a = b
5 nne ⊢ ¬ a ≠ c ↔ a = c
6 nne ⊢ ¬ b ≠ c ↔ b = c
7 4 5 6 3orbi123i ⊢ ¬ a ≠ b ∨ ¬ a ≠ c ∨ ¬ b ≠ c ↔ a = b ∨ a = c ∨ b = c
8 3 7 bitri ⊢ ¬ a ≠ b ∧ a ≠ c ∧ b ≠ c ↔ a = b ∨ a = c ∨ b = c
9 tpeq1 ⊢ a = b → a b c = b b c
10 tpidm12 ⊢ b b c = b c
11 9 10 eqtrdi ⊢ a = b → a b c = b c
12 11 eqeq2d ⊢ a = b → V = a b c ↔ V = b c
13 fveqeq2 ⊢ V = b c → V = 3 ↔ b c = 3
14 hashprlei ⊢ b c ∈ Fin ∧ b c ≤ 2
15 breq1 ⊢ b c = 3 → b c ≤ 2 ↔ 3 ≤ 2
16 2lt3 ⊢ 2 < 3
17 2re ⊢ 2 ∈ ℝ
18 3re ⊢ 3 ∈ ℝ
19 17 18 ltnlei ⊢ 2 < 3 ↔ ¬ 3 ≤ 2
20 16 19 mpbi ⊢ ¬ 3 ≤ 2
21 20 pm2.21i ⊢ 3 ≤ 2 → a ≠ b ∧ a ≠ c ∧ b ≠ c
22 15 21 biimtrdi ⊢ b c = 3 → b c ≤ 2 → a ≠ b ∧ a ≠ c ∧ b ≠ c
23 22 com12 ⊢ b c ≤ 2 → b c = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
24 23 adantl ⊢ b c ∈ Fin ∧ b c ≤ 2 → b c = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
25 14 24 ax-mp ⊢ b c = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
26 13 25 biimtrdi ⊢ V = b c → V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
27 26 adantld ⊢ V = b c → V ∈ W ∧ V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
28 12 27 biimtrdi ⊢ a = b → V = a b c → V ∈ W ∧ V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
29 tpeq1 ⊢ a = c → a b c = c b c
30 tpidm13 ⊢ c b c = c b
31 29 30 eqtrdi ⊢ a = c → a b c = c b
32 31 eqeq2d ⊢ a = c → V = a b c ↔ V = c b
33 fveqeq2 ⊢ V = c b → V = 3 ↔ c b = 3
34 hashprlei ⊢ c b ∈ Fin ∧ c b ≤ 2
35 breq1 ⊢ c b = 3 → c b ≤ 2 ↔ 3 ≤ 2
36 35 21 biimtrdi ⊢ c b = 3 → c b ≤ 2 → a ≠ b ∧ a ≠ c ∧ b ≠ c
37 36 com12 ⊢ c b ≤ 2 → c b = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
38 37 adantl ⊢ c b ∈ Fin ∧ c b ≤ 2 → c b = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
39 34 38 ax-mp ⊢ c b = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
40 33 39 biimtrdi ⊢ V = c b → V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
41 40 adantld ⊢ V = c b → V ∈ W ∧ V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
42 32 41 biimtrdi ⊢ a = c → V = a b c → V ∈ W ∧ V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
43 tpeq2 ⊢ b = c → a b c = a c c
44 tpidm23 ⊢ a c c = a c
45 43 44 eqtrdi ⊢ b = c → a b c = a c
46 45 eqeq2d ⊢ b = c → V = a b c ↔ V = a c
47 fveqeq2 ⊢ V = a c → V = 3 ↔ a c = 3
48 hashprlei ⊢ a c ∈ Fin ∧ a c ≤ 2
49 breq1 ⊢ a c = 3 → a c ≤ 2 ↔ 3 ≤ 2
50 49 21 biimtrdi ⊢ a c = 3 → a c ≤ 2 → a ≠ b ∧ a ≠ c ∧ b ≠ c
51 50 com12 ⊢ a c ≤ 2 → a c = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
52 51 adantl ⊢ a c ∈ Fin ∧ a c ≤ 2 → a c = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
53 48 52 ax-mp ⊢ a c = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
54 47 53 biimtrdi ⊢ V = a c → V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
55 54 adantld ⊢ V = a c → V ∈ W ∧ V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
56 46 55 biimtrdi ⊢ b = c → V = a b c → V ∈ W ∧ V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
57 28 42 56 3jaoi ⊢ a = b ∨ a = c ∨ b = c → V = a b c → V ∈ W ∧ V = 3 → a ≠ b ∧ a ≠ c ∧ b ≠ c
58 57 impcomd ⊢ a = b ∨ a = c ∨ b = c → V ∈ W ∧ V = 3 ∧ V = a b c → a ≠ b ∧ a ≠ c ∧ b ≠ c
59 8 58 sylbi ⊢ ¬ a ≠ b ∧ a ≠ c ∧ b ≠ c → V ∈ W ∧ V = 3 ∧ V = a b c → a ≠ b ∧ a ≠ c ∧ b ≠ c
60 2 59 pm2.61i ⊢ V ∈ W ∧ V = 3 ∧ V = a b c → a ≠ b ∧ a ≠ c ∧ b ≠ c
61 simpr ⊢ V ∈ W ∧ V = 3 ∧ V = a b c → V = a b c
62 60 61 jca ⊢ V ∈ W ∧ V = 3 ∧ V = a b c → a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
63 62 ex ⊢ V ∈ W ∧ V = 3 → V = a b c → a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
64 63 eximdv ⊢ V ∈ W ∧ V = 3 → ∃ c V = a b c → ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
65 64 2eximdv ⊢ V ∈ W ∧ V = 3 → ∃ a ∃ b ∃ c V = a b c → ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
66 1 65 mpd ⊢ V ∈ W ∧ V = 3 → ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c