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