Theorem 0sdom1dom

Description: Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un , see 0sdom1domALT . (Contributed by NM, 28-Sep-2004) Avoid ax-un . (Revised by BTernaryTau, 7-Dec-2024)

	Ref	Expression
Assertion	0sdom1dom	$$⊢\varnothing \prec A\leftrightarrow 1_{𝑜}\preccurlyeq A$$

Proof

Step	Hyp	Ref	Expression
1		relsdom	$$⊢\mathrm{Rel}\prec$$
2	1	brrelex2i	$$⊢\varnothing \prec A\to A\in \mathrm{V}$$
3		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
4	3	brrelex2i	$$⊢1_{𝑜}\preccurlyeq A\to A\in \mathrm{V}$$
5		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
6		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
7		snssi	$$⊢x\in A\to \left\{x\right\}\subseteq A$$
8		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
9		0ex	$$⊢\varnothing \in \mathrm{V}$$
10		vex	$$⊢x\in \mathrm{V}$$
11		en2sn	$$⊢\left(\varnothing \in \mathrm{V}\wedge x\in \mathrm{V}\right)\to \left\{\varnothing \right\}\approx \left\{x\right\}$$
12	9 10 11	mp2an	$$⊢\left\{\varnothing \right\}\approx \left\{x\right\}$$
13	8 12	eqbrtri	$$⊢1_{𝑜}\approx \left\{x\right\}$$
14		endom	$$⊢1_{𝑜}\approx \left\{x\right\}\to 1_{𝑜}\preccurlyeq \left\{x\right\}$$
15	13 14	ax-mp	$$⊢1_{𝑜}\preccurlyeq \left\{x\right\}$$
16		domssr	$$⊢\left(A\in \mathrm{V}\wedge \left\{x\right\}\subseteq A\wedge 1_{𝑜}\preccurlyeq \left\{x\right\}\right)\to 1_{𝑜}\preccurlyeq A$$
17	15 16	mp3an3	$$⊢\left(A\in \mathrm{V}\wedge \left\{x\right\}\subseteq A\right)\to 1_{𝑜}\preccurlyeq A$$
18	17	ex	$$⊢A\in \mathrm{V}\to \left(\left\{x\right\}\subseteq A\to 1_{𝑜}\preccurlyeq A\right)$$
19	7 18	syl5	$$⊢A\in \mathrm{V}\to \left(x\in A\to 1_{𝑜}\preccurlyeq A\right)$$
20	19	exlimdv	$$⊢A\in \mathrm{V}\to \left(\exists xx\in A\to 1_{𝑜}\preccurlyeq A\right)$$
21	6 20	biimtrid	$$⊢A\in \mathrm{V}\to \left(A\ne \varnothing \to 1_{𝑜}\preccurlyeq A\right)$$
22		1n0	$$⊢1_{𝑜}\ne \varnothing$$
23		dom0	$$⊢1_{𝑜}\preccurlyeq \varnothing \leftrightarrow 1_{𝑜}=\varnothing$$
24	22 23	nemtbir	$$⊢\neg 1_{𝑜}\preccurlyeq \varnothing$$
25		breq2	$$⊢A=\varnothing \to \left(1_{𝑜}\preccurlyeq A\leftrightarrow 1_{𝑜}\preccurlyeq \varnothing \right)$$
26	24 25	mtbiri	$$⊢A=\varnothing \to \neg 1_{𝑜}\preccurlyeq A$$
27	26	necon2ai	$$⊢1_{𝑜}\preccurlyeq A\to A\ne \varnothing$$
28	21 27	impbid1	$$⊢A\in \mathrm{V}\to \left(A\ne \varnothing \leftrightarrow 1_{𝑜}\preccurlyeq A\right)$$
29	5 28	bitrd	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow 1_{𝑜}\preccurlyeq A\right)$$
30	2 4 29	pm5.21nii	$$⊢\varnothing \prec A\leftrightarrow 1_{𝑜}\preccurlyeq A$$