# Metamath Proof Explorer

## 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}_{𝑜}↔\left\{{A},{A}\right\}\preccurlyeq {2}_{𝑜}\right)$
13 10 12 syl5ibr ${⊢}{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}_{𝑜}↔{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}_{𝑜}$