Theorem domunsn

Description: Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Assertion	domunsn	$$⊢A\prec B\to \left(A\cup \left\{C\right\}\right)\preccurlyeq B$$

Proof

Step	Hyp	Ref	Expression
1		sdom0	$$⊢\neg A\prec \varnothing$$
2		breq2	$$⊢B=\varnothing \to \left(A\prec B\leftrightarrow A\prec \varnothing \right)$$
3	1 2	mtbiri	$$⊢B=\varnothing \to \neg A\prec B$$
4	3	con2i	$$⊢A\prec B\to \neg B=\varnothing$$
5		neq0	$$⊢\neg B=\varnothing \leftrightarrow \exists zz\in B$$
6	4 5	sylib	$$⊢A\prec B\to \exists zz\in B$$
7		domdifsn	$$⊢A\prec B\to A\preccurlyeq \left(B\setminus \left\{z\right\}\right)$$
8	7	adantr	$$⊢\left(A\prec B\wedge z\in B\right)\to A\preccurlyeq \left(B\setminus \left\{z\right\}\right)$$
9		en2sn	$$⊢\left(C\in \mathrm{V}\wedge z\in \mathrm{V}\right)\to \left\{C\right\}\approx \left\{z\right\}$$
10	9	elvd	$$⊢C\in \mathrm{V}\to \left\{C\right\}\approx \left\{z\right\}$$
11		endom	$$⊢\left\{C\right\}\approx \left\{z\right\}\to \left\{C\right\}\preccurlyeq \left\{z\right\}$$
12	10 11	syl	$$⊢C\in \mathrm{V}\to \left\{C\right\}\preccurlyeq \left\{z\right\}$$
13		snprc	$$⊢\neg C\in \mathrm{V}\leftrightarrow \left\{C\right\}=\varnothing$$
14	13	biimpi	$$⊢\neg C\in \mathrm{V}\to \left\{C\right\}=\varnothing$$
15		vsnex	$$⊢\left\{z\right\}\in \mathrm{V}$$
16	15	0dom	$$⊢\varnothing \preccurlyeq \left\{z\right\}$$
17	14 16	eqbrtrdi	$$⊢\neg C\in \mathrm{V}\to \left\{C\right\}\preccurlyeq \left\{z\right\}$$
18	12 17	pm2.61i	$$⊢\left\{C\right\}\preccurlyeq \left\{z\right\}$$
19		disjdifr	$$⊢\left(B\setminus \left\{z\right\}\right)\cap \left\{z\right\}=\varnothing$$
20		undom	$$⊢\left(\left(A\preccurlyeq \left(B\setminus \left\{z\right\}\right)\wedge \left\{C\right\}\preccurlyeq \left\{z\right\}\right)\wedge \left(B\setminus \left\{z\right\}\right)\cap \left\{z\right\}=\varnothing \right)\to \left(A\cup \left\{C\right\}\right)\preccurlyeq \left(\left(B\setminus \left\{z\right\}\right)\cup \left\{z\right\}\right)$$
21	19 20	mpan2	$$⊢\left(A\preccurlyeq \left(B\setminus \left\{z\right\}\right)\wedge \left\{C\right\}\preccurlyeq \left\{z\right\}\right)\to \left(A\cup \left\{C\right\}\right)\preccurlyeq \left(\left(B\setminus \left\{z\right\}\right)\cup \left\{z\right\}\right)$$
22	8 18 21	sylancl	$$⊢\left(A\prec B\wedge z\in B\right)\to \left(A\cup \left\{C\right\}\right)\preccurlyeq \left(\left(B\setminus \left\{z\right\}\right)\cup \left\{z\right\}\right)$$
23		uncom	$$⊢\left(B\setminus \left\{z\right\}\right)\cup \left\{z\right\}=\left\{z\right\}\cup \left(B\setminus \left\{z\right\}\right)$$
24		simpr	$$⊢\left(A\prec B\wedge z\in B\right)\to z\in B$$
25	24	snssd	$$⊢\left(A\prec B\wedge z\in B\right)\to \left\{z\right\}\subseteq B$$
26		undif	$$⊢\left\{z\right\}\subseteq B\leftrightarrow \left\{z\right\}\cup \left(B\setminus \left\{z\right\}\right)=B$$
27	25 26	sylib	$$⊢\left(A\prec B\wedge z\in B\right)\to \left\{z\right\}\cup \left(B\setminus \left\{z\right\}\right)=B$$
28	23 27	eqtrid	$$⊢\left(A\prec B\wedge z\in B\right)\to \left(B\setminus \left\{z\right\}\right)\cup \left\{z\right\}=B$$
29	22 28	breqtrd	$$⊢\left(A\prec B\wedge z\in B\right)\to \left(A\cup \left\{C\right\}\right)\preccurlyeq B$$
30	6 29	exlimddv	$$⊢A\prec B\to \left(A\cup \left\{C\right\}\right)\preccurlyeq B$$