Theorem prct

Description: An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016)

	Ref	Expression
Assertion	prct	|- ( ( A e. V /\ B e. W ) -> { A , B } ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { A , B } = ( { A } u. { B } )
2		snct	|- ( A e. V -> { A } ~<_ _om )
3		snct	|- ( B e. W -> { B } ~<_ _om )
4		unctb	|- ( ( { A } ~<_ _om /\ { B } ~<_ _om ) -> ( { A } u. { B } ) ~<_ _om )
5	2 3 4	syl2an	|- ( ( A e. V /\ B e. W ) -> ( { A } u. { B } ) ~<_ _om )
6	1 5	eqbrtrid	|- ( ( A e. V /\ B e. W ) -> { A , B } ~<_ _om )