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

Metamath Proof Explorer

Theorem hash3tpde

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

Ref Expression
Assertion hash3tpde ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) )

Proof

Step Hyp Ref Expression
1 hash3tr ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 𝑉 = { 𝑎 , 𝑏 , 𝑐 } )
2 ax-1 ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) → ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
3 3ianor ⊢ ( ¬ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ( ¬ 𝑎 ≠ 𝑏 ∨ ¬ 𝑎 ≠ 𝑐 ∨ ¬ 𝑏 ≠ 𝑐 ) )
4 nne ⊢ ( ¬ 𝑎 ≠ 𝑏 ↔ 𝑎 = 𝑏 )
5 nne ⊢ ( ¬ 𝑎 ≠ 𝑐 ↔ 𝑎 = 𝑐 )
6 nne ⊢ ( ¬ 𝑏 ≠ 𝑐 ↔ 𝑏 = 𝑐 )
7 4 5 6 3orbi123i ⊢ ( ( ¬ 𝑎 ≠ 𝑏 ∨ ¬ 𝑎 ≠ 𝑐 ∨ ¬ 𝑏 ≠ 𝑐 ) ↔ ( 𝑎 = 𝑏 ∨ 𝑎 = 𝑐 ∨ 𝑏 = 𝑐 ) )
8 3 7 bitri ⊢ ( ¬ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ( 𝑎 = 𝑏 ∨ 𝑎 = 𝑐 ∨ 𝑏 = 𝑐 ) )
9 tpeq1 ⊢ ( 𝑎 = 𝑏 → { 𝑎 , 𝑏 , 𝑐 } = { 𝑏 , 𝑏 , 𝑐 } )
10 tpidm12 ⊢ { 𝑏 , 𝑏 , 𝑐 } = { 𝑏 , 𝑐 }
11 9 10 eqtrdi ⊢ ( 𝑎 = 𝑏 → { 𝑎 , 𝑏 , 𝑐 } = { 𝑏 , 𝑐 } )
12 11 eqeq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ↔ 𝑉 = { 𝑏 , 𝑐 } ) )
13 fveqeq2 ⊢ ( 𝑉 = { 𝑏 , 𝑐 } → ( ( ♯ ‘ 𝑉 ) = 3 ↔ ( ♯ ‘ { 𝑏 , 𝑐 } ) = 3 ) )
14 hashprlei ⊢ ( { 𝑏 , 𝑐 } ∈ Fin ∧ ( ♯ ‘ { 𝑏 , 𝑐 } ) ≤ 2 )
15 breq1 ⊢ ( ( ♯ ‘ { 𝑏 , 𝑐 } ) = 3 → ( ( ♯ ‘ { 𝑏 , 𝑐 } ) ≤ 2 ↔ 3 ≤ 2 ) )
16 2lt3 ⊢ 2 < 3
17 2re ⊢ 2 ∈ ℝ
18 3re ⊢ 3 ∈ ℝ
19 17 18 ltnlei ⊢ ( 2 < 3 ↔ ¬ 3 ≤ 2 )
20 16 19 mpbi ⊢ ¬ 3 ≤ 2
21 20 pm2.21i ⊢ ( 3 ≤ 2 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
22 15 21 biimtrdi ⊢ ( ( ♯ ‘ { 𝑏 , 𝑐 } ) = 3 → ( ( ♯ ‘ { 𝑏 , 𝑐 } ) ≤ 2 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
23 22 com12 ⊢ ( ( ♯ ‘ { 𝑏 , 𝑐 } ) ≤ 2 → ( ( ♯ ‘ { 𝑏 , 𝑐 } ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
24 23 adantl ⊢ ( ( { 𝑏 , 𝑐 } ∈ Fin ∧ ( ♯ ‘ { 𝑏 , 𝑐 } ) ≤ 2 ) → ( ( ♯ ‘ { 𝑏 , 𝑐 } ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
25 14 24 ax-mp ⊢ ( ( ♯ ‘ { 𝑏 , 𝑐 } ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
26 13 25 biimtrdi ⊢ ( 𝑉 = { 𝑏 , 𝑐 } → ( ( ♯ ‘ 𝑉 ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
27 26 adantld ⊢ ( 𝑉 = { 𝑏 , 𝑐 } → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
28 12 27 biimtrdi ⊢ ( 𝑎 = 𝑏 → ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) ) )
29 tpeq1 ⊢ ( 𝑎 = 𝑐 → { 𝑎 , 𝑏 , 𝑐 } = { 𝑐 , 𝑏 , 𝑐 } )
30 tpidm13 ⊢ { 𝑐 , 𝑏 , 𝑐 } = { 𝑐 , 𝑏 }
31 29 30 eqtrdi ⊢ ( 𝑎 = 𝑐 → { 𝑎 , 𝑏 , 𝑐 } = { 𝑐 , 𝑏 } )
32 31 eqeq2d ⊢ ( 𝑎 = 𝑐 → ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ↔ 𝑉 = { 𝑐 , 𝑏 } ) )
33 fveqeq2 ⊢ ( 𝑉 = { 𝑐 , 𝑏 } → ( ( ♯ ‘ 𝑉 ) = 3 ↔ ( ♯ ‘ { 𝑐 , 𝑏 } ) = 3 ) )
34 hashprlei ⊢ ( { 𝑐 , 𝑏 } ∈ Fin ∧ ( ♯ ‘ { 𝑐 , 𝑏 } ) ≤ 2 )
35 breq1 ⊢ ( ( ♯ ‘ { 𝑐 , 𝑏 } ) = 3 → ( ( ♯ ‘ { 𝑐 , 𝑏 } ) ≤ 2 ↔ 3 ≤ 2 ) )
36 35 21 biimtrdi ⊢ ( ( ♯ ‘ { 𝑐 , 𝑏 } ) = 3 → ( ( ♯ ‘ { 𝑐 , 𝑏 } ) ≤ 2 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
37 36 com12 ⊢ ( ( ♯ ‘ { 𝑐 , 𝑏 } ) ≤ 2 → ( ( ♯ ‘ { 𝑐 , 𝑏 } ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
38 37 adantl ⊢ ( ( { 𝑐 , 𝑏 } ∈ Fin ∧ ( ♯ ‘ { 𝑐 , 𝑏 } ) ≤ 2 ) → ( ( ♯ ‘ { 𝑐 , 𝑏 } ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
39 34 38 ax-mp ⊢ ( ( ♯ ‘ { 𝑐 , 𝑏 } ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
40 33 39 biimtrdi ⊢ ( 𝑉 = { 𝑐 , 𝑏 } → ( ( ♯ ‘ 𝑉 ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
41 40 adantld ⊢ ( 𝑉 = { 𝑐 , 𝑏 } → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
42 32 41 biimtrdi ⊢ ( 𝑎 = 𝑐 → ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) ) )
43 tpeq2 ⊢ ( 𝑏 = 𝑐 → { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑐 , 𝑐 } )
44 tpidm23 ⊢ { 𝑎 , 𝑐 , 𝑐 } = { 𝑎 , 𝑐 }
45 43 44 eqtrdi ⊢ ( 𝑏 = 𝑐 → { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑐 } )
46 45 eqeq2d ⊢ ( 𝑏 = 𝑐 → ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ↔ 𝑉 = { 𝑎 , 𝑐 } ) )
47 fveqeq2 ⊢ ( 𝑉 = { 𝑎 , 𝑐 } → ( ( ♯ ‘ 𝑉 ) = 3 ↔ ( ♯ ‘ { 𝑎 , 𝑐 } ) = 3 ) )
48 hashprlei ⊢ ( { 𝑎 , 𝑐 } ∈ Fin ∧ ( ♯ ‘ { 𝑎 , 𝑐 } ) ≤ 2 )
49 breq1 ⊢ ( ( ♯ ‘ { 𝑎 , 𝑐 } ) = 3 → ( ( ♯ ‘ { 𝑎 , 𝑐 } ) ≤ 2 ↔ 3 ≤ 2 ) )
50 49 21 biimtrdi ⊢ ( ( ♯ ‘ { 𝑎 , 𝑐 } ) = 3 → ( ( ♯ ‘ { 𝑎 , 𝑐 } ) ≤ 2 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
51 50 com12 ⊢ ( ( ♯ ‘ { 𝑎 , 𝑐 } ) ≤ 2 → ( ( ♯ ‘ { 𝑎 , 𝑐 } ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
52 51 adantl ⊢ ( ( { 𝑎 , 𝑐 } ∈ Fin ∧ ( ♯ ‘ { 𝑎 , 𝑐 } ) ≤ 2 ) → ( ( ♯ ‘ { 𝑎 , 𝑐 } ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
53 48 52 ax-mp ⊢ ( ( ♯ ‘ { 𝑎 , 𝑐 } ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
54 47 53 biimtrdi ⊢ ( 𝑉 = { 𝑎 , 𝑐 } → ( ( ♯ ‘ 𝑉 ) = 3 → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
55 54 adantld ⊢ ( 𝑉 = { 𝑎 , 𝑐 } → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
56 46 55 biimtrdi ⊢ ( 𝑏 = 𝑐 → ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) ) )
57 28 42 56 3jaoi ⊢ ( ( 𝑎 = 𝑏 ∨ 𝑎 = 𝑐 ∨ 𝑏 = 𝑐 ) → ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) ) )
58 57 impcomd ⊢ ( ( 𝑎 = 𝑏 ∨ 𝑎 = 𝑐 ∨ 𝑏 = 𝑐 ) → ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
59 8 58 sylbi ⊢ ( ¬ ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) → ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
60 2 59 pm2.61i ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) → ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
61 simpr ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) → 𝑉 = { 𝑎 , 𝑏 , 𝑐 } )
62 60 61 jca ⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) )
63 62 ex ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )
64 63 eximdv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( ∃ 𝑐 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ∃ 𝑐 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )
65 64 2eximdv ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 𝑉 = { 𝑎 , 𝑏 , 𝑐 } → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) ) )
66 1 65 mpd ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 3 ) → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) )