Theorem en4

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

	Ref	Expression
Assertion	en4	|- ( A ~~ 4o -> E. x E. y E. z E. w A = ( { x , y } u. { z , w } ) )

Proof

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