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 
|- ( ( V e. W /\ ( # ` V ) = 3 ) -> E. a E. b E. c ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) )

Proof

Step Hyp Ref Expression
1 hash3tr 
 |-  ( ( V e. W /\ ( # ` V ) = 3 ) -> E. a E. b E. c V = { a , b , c } )
2 ax-1 
 |-  ( ( a =/= b /\ a =/= c /\ b =/= c ) -> ( ( ( V e. W /\ ( # ` V ) = 3 ) /\ V = { a , b , c } ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
3 3ianor 
 |-  ( -. ( a =/= b /\ a =/= c /\ b =/= c ) <-> ( -. a =/= b \/ -. a =/= c \/ -. b =/= c ) )
4 nne 
 |-  ( -. a =/= b <-> a = b )
5 nne 
 |-  ( -. a =/= c <-> a = c )
6 nne 
 |-  ( -. b =/= c <-> b = c )
7 4 5 6 3orbi123i 
 |-  ( ( -. a =/= b \/ -. a =/= c \/ -. b =/= c ) <-> ( a = b \/ a = c \/ b = c ) )
8 3 7 bitri 
 |-  ( -. ( a =/= b /\ a =/= c /\ b =/= c ) <-> ( a = b \/ a = c \/ b = c ) )
9 tpeq1 
 |-  ( a = b -> { a , b , c } = { b , b , c } )
10 tpidm12 
 |-  { b , b , c } = { b , c }
11 9 10 eqtrdi 
 |-  ( a = b -> { a , b , c } = { b , c } )
12 11 eqeq2d 
 |-  ( a = b -> ( V = { a , b , c } <-> V = { b , c } ) )
13 fveqeq2 
 |-  ( V = { b , c } -> ( ( # ` V ) = 3 <-> ( # ` { b , c } ) = 3 ) )
14 hashprlei 
 |-  ( { b , c } e. Fin /\ ( # ` { b , c } ) <_ 2 )
15 breq1 
 |-  ( ( # ` { b , c } ) = 3 -> ( ( # ` { b , c } ) <_ 2 <-> 3 <_ 2 ) )
16 2lt3 
 |-  2 < 3
17 2re 
 |-  2 e. RR
18 3re 
 |-  3 e. RR
19 17 18 ltnlei 
 |-  ( 2 < 3 <-> -. 3 <_ 2 )
20 16 19 mpbi 
 |-  -. 3 <_ 2
21 20 pm2.21i 
 |-  ( 3 <_ 2 -> ( a =/= b /\ a =/= c /\ b =/= c ) )
22 15 21 biimtrdi 
 |-  ( ( # ` { b , c } ) = 3 -> ( ( # ` { b , c } ) <_ 2 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
23 22 com12 
 |-  ( ( # ` { b , c } ) <_ 2 -> ( ( # ` { b , c } ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
24 23 adantl 
 |-  ( ( { b , c } e. Fin /\ ( # ` { b , c } ) <_ 2 ) -> ( ( # ` { b , c } ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
25 14 24 ax-mp 
 |-  ( ( # ` { b , c } ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) )
26 13 25 biimtrdi 
 |-  ( V = { b , c } -> ( ( # ` V ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
27 26 adantld 
 |-  ( V = { b , c } -> ( ( V e. W /\ ( # ` V ) = 3 ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
28 12 27 biimtrdi 
 |-  ( a = b -> ( V = { a , b , c } -> ( ( V e. W /\ ( # ` V ) = 3 ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) ) )
29 tpeq1 
 |-  ( a = c -> { a , b , c } = { c , b , c } )
30 tpidm13 
 |-  { c , b , c } = { c , b }
31 29 30 eqtrdi 
 |-  ( a = c -> { a , b , c } = { c , b } )
32 31 eqeq2d 
 |-  ( a = c -> ( V = { a , b , c } <-> V = { c , b } ) )
33 fveqeq2 
 |-  ( V = { c , b } -> ( ( # ` V ) = 3 <-> ( # ` { c , b } ) = 3 ) )
34 hashprlei 
 |-  ( { c , b } e. Fin /\ ( # ` { c , b } ) <_ 2 )
35 breq1 
 |-  ( ( # ` { c , b } ) = 3 -> ( ( # ` { c , b } ) <_ 2 <-> 3 <_ 2 ) )
36 35 21 biimtrdi 
 |-  ( ( # ` { c , b } ) = 3 -> ( ( # ` { c , b } ) <_ 2 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
37 36 com12 
 |-  ( ( # ` { c , b } ) <_ 2 -> ( ( # ` { c , b } ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
38 37 adantl 
 |-  ( ( { c , b } e. Fin /\ ( # ` { c , b } ) <_ 2 ) -> ( ( # ` { c , b } ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
39 34 38 ax-mp 
 |-  ( ( # ` { c , b } ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) )
40 33 39 biimtrdi 
 |-  ( V = { c , b } -> ( ( # ` V ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
41 40 adantld 
 |-  ( V = { c , b } -> ( ( V e. W /\ ( # ` V ) = 3 ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
42 32 41 biimtrdi 
 |-  ( a = c -> ( V = { a , b , c } -> ( ( V e. W /\ ( # ` V ) = 3 ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) ) )
43 tpeq2 
 |-  ( b = c -> { a , b , c } = { a , c , c } )
44 tpidm23 
 |-  { a , c , c } = { a , c }
45 43 44 eqtrdi 
 |-  ( b = c -> { a , b , c } = { a , c } )
46 45 eqeq2d 
 |-  ( b = c -> ( V = { a , b , c } <-> V = { a , c } ) )
47 fveqeq2 
 |-  ( V = { a , c } -> ( ( # ` V ) = 3 <-> ( # ` { a , c } ) = 3 ) )
48 hashprlei 
 |-  ( { a , c } e. Fin /\ ( # ` { a , c } ) <_ 2 )
49 breq1 
 |-  ( ( # ` { a , c } ) = 3 -> ( ( # ` { a , c } ) <_ 2 <-> 3 <_ 2 ) )
50 49 21 biimtrdi 
 |-  ( ( # ` { a , c } ) = 3 -> ( ( # ` { a , c } ) <_ 2 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
51 50 com12 
 |-  ( ( # ` { a , c } ) <_ 2 -> ( ( # ` { a , c } ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
52 51 adantl 
 |-  ( ( { a , c } e. Fin /\ ( # ` { a , c } ) <_ 2 ) -> ( ( # ` { a , c } ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
53 48 52 ax-mp 
 |-  ( ( # ` { a , c } ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) )
54 47 53 biimtrdi 
 |-  ( V = { a , c } -> ( ( # ` V ) = 3 -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
55 54 adantld 
 |-  ( V = { a , c } -> ( ( V e. W /\ ( # ` V ) = 3 ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
56 46 55 biimtrdi 
 |-  ( b = c -> ( V = { a , b , c } -> ( ( V e. W /\ ( # ` V ) = 3 ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) ) )
57 28 42 56 3jaoi 
 |-  ( ( a = b \/ a = c \/ b = c ) -> ( V = { a , b , c } -> ( ( V e. W /\ ( # ` V ) = 3 ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) ) )
58 57 impcomd 
 |-  ( ( a = b \/ a = c \/ b = c ) -> ( ( ( V e. W /\ ( # ` V ) = 3 ) /\ V = { a , b , c } ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
59 8 58 sylbi 
 |-  ( -. ( a =/= b /\ a =/= c /\ b =/= c ) -> ( ( ( V e. W /\ ( # ` V ) = 3 ) /\ V = { a , b , c } ) -> ( a =/= b /\ a =/= c /\ b =/= c ) ) )
60 2 59 pm2.61i 
 |-  ( ( ( V e. W /\ ( # ` V ) = 3 ) /\ V = { a , b , c } ) -> ( a =/= b /\ a =/= c /\ b =/= c ) )
61 simpr 
 |-  ( ( ( V e. W /\ ( # ` V ) = 3 ) /\ V = { a , b , c } ) -> V = { a , b , c } )
62 60 61 jca 
 |-  ( ( ( V e. W /\ ( # ` V ) = 3 ) /\ V = { a , b , c } ) -> ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) )
63 62 ex 
 |-  ( ( V e. W /\ ( # ` V ) = 3 ) -> ( V = { a , b , c } -> ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )
64 63 eximdv 
 |-  ( ( V e. W /\ ( # ` V ) = 3 ) -> ( E. c V = { a , b , c } -> E. c ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )
65 64 2eximdv 
 |-  ( ( V e. W /\ ( # ` V ) = 3 ) -> ( E. a E. b E. c V = { a , b , c } -> E. a E. b E. c ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )
66 1 65 mpd 
 |-  ( ( V e. W /\ ( # ` V ) = 3 ) -> E. a E. b E. c ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) )