Metamath Proof Explorer

Theorem hash3tpexb

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

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

Proof

Step Hyp Ref Expression
1 hash3tpde ⊢ V ∈ W ∧ V = 3 → ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
2 1 ex ⊢ V ∈ W → V = 3 → ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
3 fveq2 ⊢ V = a b c → V = a b c
4 df-tp ⊢ a b c = a b ∪ c
5 4 a1i ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → a b c = a b ∪ c
6 5 fveq2d ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → a b c = a b ∪ c
7 prfi ⊢ a b ∈ Fin
8 snfi ⊢ c ∈ Fin
9 disjprsn ⊢ a ≠ c ∧ b ≠ c → a b ∩ c = ∅
10 9 3adant1 ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → a b ∩ c = ∅
11 hashun ⊢ a b ∈ Fin ∧ c ∈ Fin ∧ a b ∩ c = ∅ → a b ∪ c = a b + c
12 7 8 10 11 mp3an12i ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → a b ∪ c = a b + c
13 hashprg ⊢ a ∈ V ∧ b ∈ V → a ≠ b ↔ a b = 2
14 13 el2v ⊢ a ≠ b ↔ a b = 2
15 14 biimpi ⊢ a ≠ b → a b = 2
16 15 3ad2ant1 ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → a b = 2
17 hashsng ⊢ c ∈ V → c = 1
18 17 elv ⊢ c = 1
19 18 a1i ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → c = 1
20 16 19 oveq12d ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → a b + c = 2 + 1
21 2p1e3 ⊢ 2 + 1 = 3
22 20 21 eqtrdi ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → a b + c = 3
23 6 12 22 3eqtrd ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c → a b c = 3
24 3 23 sylan9eqr ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c → V = 3
25 24 a1i ⊢ V ∈ W → a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c → V = 3
26 25 exlimdv ⊢ V ∈ W → ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c → V = 3
27 26 exlimdvv ⊢ V ∈ W → ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c → V = 3
28 2 27 impbid ⊢ V ∈ W → V = 3 ↔ ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c