Metamath Proof Explorer

Theorem hash3tpb

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

Ref Expression
Assertion hash3tpb 
|- ( V e. W -> ( ( # ` V ) = 3 <-> E. a e. V E. b e. V E. c e. V ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )

Proof

Step Hyp Ref Expression
1 hash3tpexb 
 |-  ( V e. W -> ( ( # ` V ) = 3 <-> E. a E. b E. c ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )
2 vex 
 |-  a e. _V
3 2 tpid1 
 |-  a e. { a , b , c }
4 vex 
 |-  b e. _V
5 4 tpid2 
 |-  b e. { a , b , c }
6 vex 
 |-  c e. _V
7 6 tpid3 
 |-  c e. { a , b , c }
8 3 5 7 3pm3.2i 
 |-  ( a e. { a , b , c } /\ b e. { a , b , c } /\ c e. { a , b , c } )
9 eleq2 
 |-  ( V = { a , b , c } -> ( a e. V <-> a e. { a , b , c } ) )
10 eleq2 
 |-  ( V = { a , b , c } -> ( b e. V <-> b e. { a , b , c } ) )
11 eleq2 
 |-  ( V = { a , b , c } -> ( c e. V <-> c e. { a , b , c } ) )
12 9 10 11 3anbi123d 
 |-  ( V = { a , b , c } -> ( ( a e. V /\ b e. V /\ c e. V ) <-> ( a e. { a , b , c } /\ b e. { a , b , c } /\ c e. { a , b , c } ) ) )
13 8 12 mpbiri 
 |-  ( V = { a , b , c } -> ( a e. V /\ b e. V /\ c e. V ) )
14 13 adantl 
 |-  ( ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) -> ( a e. V /\ b e. V /\ c e. V ) )
15 14 pm4.71ri 
 |-  ( ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) <-> ( ( a e. V /\ b e. V /\ c e. V ) /\ ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )
16 15 3exbii 
 |-  ( E. a E. b E. c ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) <-> E. a E. b E. c ( ( a e. V /\ b e. V /\ c e. V ) /\ ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )
17 16 a1i 
 |-  ( V e. W -> ( E. a E. b E. c ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) <-> E. a E. b E. c ( ( a e. V /\ b e. V /\ c e. V ) /\ ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) ) )
18 r3ex 
 |-  ( E. a e. V E. b e. V E. c e. V ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) <-> E. a E. b E. c ( ( a e. V /\ b e. V /\ c e. V ) /\ ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )
19 18 bicomi 
 |-  ( E. a E. b E. c ( ( a e. V /\ b e. V /\ c e. V ) /\ ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) <-> E. a e. V E. b e. V E. c e. V ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) )
20 19 a1i 
 |-  ( V e. W -> ( E. a E. b E. c ( ( a e. V /\ b e. V /\ c e. V ) /\ ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) <-> E. a e. V E. b e. V E. c e. V ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )
21 1 17 20 3bitrd 
 |-  ( V e. W -> ( ( # ` V ) = 3 <-> E. a e. V E. b e. V E. c e. V ( ( a =/= b /\ a =/= c /\ b =/= c ) /\ V = { a , b , c } ) ) )