Theorem en3

Description: A set equinumerous to ordinal 3 is a triple. (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Assertion	en3	|- ( A ~~ 3o -> E. x E. y E. z A = { x , y , z } )

Proof

Step	Hyp	Ref	Expression
1		2on	|- 2o e. On
2	1	onordi	|- Ord 2o
3		df-3o	|- 3o = suc 2o
4		en2	|- ( ( A \ { x } ) ~~ 2o -> E. y E. z ( A \ { x } ) = { y , z } )
5		tpass	|- { x , y , z } = ( { x } u. { y , z } )
6	5	enp1ilem	|- ( x e. A -> ( ( A \ { x } ) = { y , z } -> A = { x , y , z } ) )
7	6	2eximdv	|- ( x e. A -> ( E. y E. z ( A \ { x } ) = { y , z } -> E. y E. z A = { x , y , z } ) )
8	2 3 4 7	enp1i	|- ( A ~~ 3o -> E. x E. y E. z A = { x , y , z } )