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

Proof

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