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

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