Description: An unordered triple has at most three elements. (Contributed by Mario Carneiro, 11-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | hashtplei | |- ( { A , B , C } e. Fin /\ ( # ` { A , B , C } ) <_ 3 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-tp | |- { A , B , C } = ( { A , B } u. { C } ) |
|
2 | hashprlei | |- ( { A , B } e. Fin /\ ( # ` { A , B } ) <_ 2 ) |
|
3 | hashsnlei | |- ( { C } e. Fin /\ ( # ` { C } ) <_ 1 ) |
|
4 | 2nn0 | |- 2 e. NN0 |
|
5 | 1nn0 | |- 1 e. NN0 |
|
6 | 2p1e3 | |- ( 2 + 1 ) = 3 |
|
7 | 1 2 3 4 5 6 | hashunlei | |- ( { A , B , C } e. Fin /\ ( # ` { A , B , C } ) <_ 3 ) |