Metamath Proof Explorer

Theorem hash3tpb

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

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

Proof

Step Hyp Ref Expression
1 hash3tpexb ⊢ V ∈ W → V = 3 ↔ ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
2 vex ⊢ a ∈ V
3 2 tpid1 ⊢ a ∈ a b c
4 vex ⊢ b ∈ V
5 4 tpid2 ⊢ b ∈ a b c
6 vex ⊢ c ∈ V
7 6 tpid3 ⊢ c ∈ a b c
8 3 5 7 3pm3.2i ⊢ a ∈ a b c ∧ b ∈ a b c ∧ c ∈ a b c
9 eleq2 ⊢ V = a b c → a ∈ V ↔ a ∈ a b c
10 eleq2 ⊢ V = a b c → b ∈ V ↔ b ∈ a b c
11 eleq2 ⊢ V = a b c → c ∈ V ↔ c ∈ a b c
12 9 10 11 3anbi123d ⊢ V = a b c → a ∈ V ∧ b ∈ V ∧ c ∈ V ↔ a ∈ a b c ∧ b ∈ a b c ∧ c ∈ a b c
13 8 12 mpbiri ⊢ V = a b c → a ∈ V ∧ b ∈ V ∧ c ∈ V
14 13 adantl ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c → a ∈ V ∧ b ∈ V ∧ c ∈ V
15 14 pm4.71ri ⊢ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c ↔ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
16 15 3exbii ⊢ ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c ↔ ∃ a ∃ b ∃ c a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
17 16 a1i ⊢ V ∈ W → ∃ a ∃ b ∃ c a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c ↔ ∃ a ∃ b ∃ c a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
18 r3ex ⊢ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c ↔ ∃ a ∃ b ∃ c a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
19 18 bicomi ⊢ ∃ a ∃ b ∃ c a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
20 19 a1i ⊢ V ∈ W → ∃ a ∃ b ∃ c a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c
21 1 17 20 3bitrd ⊢ V ∈ W → V = 3 ↔ ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ V = a b c