Theorem djudoml

Description: A set is dominated by its disjoint union with another. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	djudoml	$$⊢\left(A\in V\wedge B\in W\right)\to A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		unexg	$$⊢\left(A\in V\wedge B\in W\right)\to A\cup B\in \mathrm{V}$$
2		ssun1	$$⊢A\subseteq A\cup B$$
3		ssdomg	$$⊢A\cup B\in \mathrm{V}\to \left(A\subseteq A\cup B\to A\preccurlyeq \left(A\cup B\right)\right)$$
4	1 2 3	mpisyl	$$⊢\left(A\in V\wedge B\in W\right)\to A\preccurlyeq \left(A\cup B\right)$$
5		undjudom	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\cup B\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)$$
6		domtr	$$⊢\left(A\preccurlyeq \left(A\cup B\right)\wedge \left(A\cup B\right)\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)\right)\to A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)$$
7	4 5 6	syl2anc	$$⊢\left(A\in V\wedge B\in W\right)\to A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}B\right)$$