This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 3 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )

Proof

Step Hyp Ref Expression
1 hash3tpexb ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 3 ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )
2 vex ⊢ 𝑎 ∈ V
3 2 tpid1 ⊢ 𝑎 ∈ { 𝑎 , 𝑏 , 𝑐 }
4 vex ⊢ 𝑏 ∈ V
5 4 tpid2 ⊢ 𝑏 ∈ { 𝑎 , 𝑏 , 𝑐 }
6 vex ⊢ 𝑐 ∈ V
7 6 tpid3 ⊢ 𝑐 ∈ { 𝑎 , 𝑏 , 𝑐 }
8 3 5 7 3pm3.2i ⊢ ( 𝑎 ∈ { 𝑎 , 𝑏 , 𝑐 } ∧ 𝑏 ∈ { 𝑎 , 𝑏 , 𝑐 } ∧ 𝑐 ∈ { 𝑎 , 𝑏 , 𝑐 } )
9 eleq2 ⊢ ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( 𝑎 ∈ 𝑉 ↔ 𝑎 ∈ { 𝑎 , 𝑏 , 𝑐 } ) )
10 eleq2 ⊢ ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( 𝑏 ∈ 𝑉 ↔ 𝑏 ∈ { 𝑎 , 𝑏 , 𝑐 } ) )
11 eleq2 ⊢ ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( 𝑐 ∈ 𝑉 ↔ 𝑐 ∈ { 𝑎 , 𝑏 , 𝑐 } ) )
12 9 10 11 3anbi123d ⊢ ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ↔ ( 𝑎 ∈ { 𝑎 , 𝑏 , 𝑐 } ∧ 𝑏 ∈ { 𝑎 , 𝑏 , 𝑐 } ∧ 𝑐 ∈ { 𝑎 , 𝑏 , 𝑐 } ) ) )
13 8 12 mpbiri ⊢ ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) )
14 13 adantl ⊢ ( ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) → ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) )
15 14 pm4.71ri ⊢ ( ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ↔ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )
16 15 3exbii ⊢ ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )
17 16 a1i ⊢ ( 𝑉 ∈ 𝑊 → ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) ) )
18 r3ex ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )
19 18 bicomi ⊢ ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) )
20 19 a1i ⊢ ( 𝑉 ∈ 𝑊 → ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )
21 1 17 20 3bitrd ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 3 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )