Theorem prdom2

Description: An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011)

	Ref	Expression
Assertion	prdom2	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{A,B\right\}\preccurlyeq 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		dfsn2	$$⊢\left\{A\right\}=\left\{A,A\right\}$$
2		ensn1g	$$⊢A\in C\to \left\{A\right\}\approx 1_{𝑜}$$
3		endom	$$⊢\left\{A\right\}\approx 1_{𝑜}\to \left\{A\right\}\preccurlyeq 1_{𝑜}$$
4		1sdom2	$$⊢1_{𝑜}\prec 2_{𝑜}$$
5		domsdomtr	$$⊢\left(\left\{A\right\}\preccurlyeq 1_{𝑜}\wedge 1_{𝑜}\prec 2_{𝑜}\right)\to \left\{A\right\}\prec 2_{𝑜}$$
6		sdomdom	$$⊢\left\{A\right\}\prec 2_{𝑜}\to \left\{A\right\}\preccurlyeq 2_{𝑜}$$
7	5 6	syl	$$⊢\left(\left\{A\right\}\preccurlyeq 1_{𝑜}\wedge 1_{𝑜}\prec 2_{𝑜}\right)\to \left\{A\right\}\preccurlyeq 2_{𝑜}$$
8	3 4 7	sylancl	$$⊢\left\{A\right\}\approx 1_{𝑜}\to \left\{A\right\}\preccurlyeq 2_{𝑜}$$
9	2 8	syl	$$⊢A\in C\to \left\{A\right\}\preccurlyeq 2_{𝑜}$$
10	1 9	eqbrtrrid	$$⊢A\in C\to \left\{A,A\right\}\preccurlyeq 2_{𝑜}$$
11		preq2	$$⊢B=A\to \left\{A,B\right\}=\left\{A,A\right\}$$
12	11	breq1d	$$⊢B=A\to \left(\left\{A,B\right\}\preccurlyeq 2_{𝑜}\leftrightarrow \left\{A,A\right\}\preccurlyeq 2_{𝑜}\right)$$
13	10 12	imbitrrid	$$⊢B=A\to \left(A\in C\to \left\{A,B\right\}\preccurlyeq 2_{𝑜}\right)$$
14	13	eqcoms	$$⊢A=B\to \left(A\in C\to \left\{A,B\right\}\preccurlyeq 2_{𝑜}\right)$$
15	14	adantrd	$$⊢A=B\to \left(\left(A\in C\wedge B\in D\right)\to \left\{A,B\right\}\preccurlyeq 2_{𝑜}\right)$$
16		pr2ne	$$⊢\left(A\in C\wedge B\in D\right)\to \left(\left\{A,B\right\}\approx 2_{𝑜}\leftrightarrow A\ne B\right)$$
17	16	biimprd	$$⊢\left(A\in C\wedge B\in D\right)\to \left(A\ne B\to \left\{A,B\right\}\approx 2_{𝑜}\right)$$
18		endom	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\to \left\{A,B\right\}\preccurlyeq 2_{𝑜}$$
19	17 18	syl6com	$$⊢A\ne B\to \left(\left(A\in C\wedge B\in D\right)\to \left\{A,B\right\}\preccurlyeq 2_{𝑜}\right)$$
20	15 19	pm2.61ine	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{A,B\right\}\preccurlyeq 2_{𝑜}$$