Theorem 1sdom2dom

Description: Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024)

	Ref	Expression
Assertion	1sdom2dom	$$⊢1_{𝑜}\prec A\leftrightarrow 2_{𝑜}\preccurlyeq A$$

Proof

Step	Hyp	Ref	Expression
1		relsdom	$$⊢\mathrm{Rel}\prec$$
2	1	brrelex2i	$$⊢1_{𝑜}\prec A\to A\in \mathrm{V}$$
3		sdomdom	$$⊢1_{𝑜}\prec A\to 1_{𝑜}\preccurlyeq A$$
4		0sdom1dom	$$⊢\varnothing \prec A\leftrightarrow 1_{𝑜}\preccurlyeq A$$
5	3 4	sylibr	$$⊢1_{𝑜}\prec A\to \varnothing \prec A$$
6		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
7	2 6	syl	$$⊢1_{𝑜}\prec A\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
8	5 7	mpbid	$$⊢1_{𝑜}\prec A\to A\ne \varnothing$$
9		n0snor2el	$$⊢A\ne \varnothing \to \left(\exists x\in A\exists y\in Ax\ne y\vee \exists xA=\left\{x\right\}\right)$$
10	8 9	syl	$$⊢1_{𝑜}\prec A\to \left(\exists x\in A\exists y\in Ax\ne y\vee \exists xA=\left\{x\right\}\right)$$
11		sdomnen	$$⊢1_{𝑜}\prec A\to \neg 1_{𝑜}\approx A$$
12		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
13		0ex	$$⊢\varnothing \in \mathrm{V}$$
14		vex	$$⊢x\in \mathrm{V}$$
15		en2sn	$$⊢\left(\varnothing \in \mathrm{V}\wedge x\in \mathrm{V}\right)\to \left\{\varnothing \right\}\approx \left\{x\right\}$$
16	13 14 15	mp2an	$$⊢\left\{\varnothing \right\}\approx \left\{x\right\}$$
17	12 16	eqbrtri	$$⊢1_{𝑜}\approx \left\{x\right\}$$
18		breq2	$$⊢A=\left\{x\right\}\to \left(1_{𝑜}\approx A\leftrightarrow 1_{𝑜}\approx \left\{x\right\}\right)$$
19	17 18	mpbiri	$$⊢A=\left\{x\right\}\to 1_{𝑜}\approx A$$
20	19	exlimiv	$$⊢\exists xA=\left\{x\right\}\to 1_{𝑜}\approx A$$
21	11 20	nsyl	$$⊢1_{𝑜}\prec A\to \neg \exists xA=\left\{x\right\}$$
22	10 21	olcnd	$$⊢1_{𝑜}\prec A\to \exists x\in A\exists y\in Ax\ne y$$
23		rex2dom	$$⊢\left(A\in \mathrm{V}\wedge \exists x\in A\exists y\in Ax\ne y\right)\to 2_{𝑜}\preccurlyeq A$$
24	2 22 23	syl2anc	$$⊢1_{𝑜}\prec A\to 2_{𝑜}\preccurlyeq A$$
25		snsspr1	$$⊢\left\{\varnothing \right\}\subseteq \left\{\varnothing ,1_{𝑜}\right\}$$
26		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
27	25 12 26	3sstr4i	$$⊢1_{𝑜}\subseteq 2_{𝑜}$$
28		domssl	$$⊢\left(1_{𝑜}\subseteq 2_{𝑜}\wedge 2_{𝑜}\preccurlyeq A\right)\to 1_{𝑜}\preccurlyeq A$$
29	27 28	mpan	$$⊢2_{𝑜}\preccurlyeq A\to 1_{𝑜}\preccurlyeq A$$
30		snnen2o	$$⊢\neg \left\{y\right\}\approx 2_{𝑜}$$
31	13	a1i	$$⊢\top \to \varnothing \in \mathrm{V}$$
32		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
33	32	a1i	$$⊢\top \to 1_{𝑜}\in \mathrm{V}$$
34		1n0	$$⊢1_{𝑜}\ne \varnothing$$
35	34	nesymi	$$⊢\neg \varnothing =1_{𝑜}$$
36	35	a1i	$$⊢\top \to \neg \varnothing =1_{𝑜}$$
37	31 33 36	enpr2d	$$⊢\top \to \left\{\varnothing ,1_{𝑜}\right\}\approx 2_{𝑜}$$
38	37	mptru	$$⊢\left\{\varnothing ,1_{𝑜}\right\}\approx 2_{𝑜}$$
39	26 38	eqbrtri	$$⊢2_{𝑜}\approx 2_{𝑜}$$
40		breq1	$$⊢2_{𝑜}=\left\{y\right\}\to \left(2_{𝑜}\approx 2_{𝑜}\leftrightarrow \left\{y\right\}\approx 2_{𝑜}\right)$$
41	39 40	mpbii	$$⊢2_{𝑜}=\left\{y\right\}\to \left\{y\right\}\approx 2_{𝑜}$$
42	30 41	mto	$$⊢\neg 2_{𝑜}=\left\{y\right\}$$
43	42	nex	$$⊢\neg \exists y{2}_{𝑜}=\left\{y\right\}$$
44		2on0	$$⊢2_{𝑜}\ne \varnothing$$
45		f1cdmsn	$$⊢\left(f:2_{𝑜}\underset{1-1}{⟶}\left\{x\right\}\wedge 2_{𝑜}\ne \varnothing \right)\to \exists y{2}_{𝑜}=\left\{y\right\}$$
46	44 45	mpan2	$$⊢f:2_{𝑜}\underset{1-1}{⟶}\left\{x\right\}\to \exists y{2}_{𝑜}=\left\{y\right\}$$
47	43 46	mto	$$⊢\neg f:2_{𝑜}\underset{1-1}{⟶}\left\{x\right\}$$
48	47	nex	$$⊢\neg \exists ff:2_{𝑜}\underset{1-1}{⟶}\left\{x\right\}$$
49		brdomi	$$⊢2_{𝑜}\preccurlyeq \left\{x\right\}\to \exists ff:2_{𝑜}\underset{1-1}{⟶}\left\{x\right\}$$
50	48 49	mto	$$⊢\neg 2_{𝑜}\preccurlyeq \left\{x\right\}$$
51		breq2	$$⊢A=\left\{x\right\}\to \left(2_{𝑜}\preccurlyeq A\leftrightarrow 2_{𝑜}\preccurlyeq \left\{x\right\}\right)$$
52	50 51	mtbiri	$$⊢A=\left\{x\right\}\to \neg 2_{𝑜}\preccurlyeq A$$
53	52	con2i	$$⊢2_{𝑜}\preccurlyeq A\to \neg A=\left\{x\right\}$$
54	53	nexdv	$$⊢2_{𝑜}\preccurlyeq A\to \neg \exists xA=\left\{x\right\}$$
55		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
56	55	brrelex2i	$$⊢2_{𝑜}\preccurlyeq A\to A\in \mathrm{V}$$
57		breng	$$⊢\left(1_{𝑜}\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(1_{𝑜}\approx A\leftrightarrow \exists ff:1_{𝑜}\underset{1-1\; onto}{⟶}A\right)$$
58	32 57	mpan	$$⊢A\in \mathrm{V}\to \left(1_{𝑜}\approx A\leftrightarrow \exists ff:1_{𝑜}\underset{1-1\; onto}{⟶}A\right)$$
59	56 58	syl	$$⊢2_{𝑜}\preccurlyeq A\to \left(1_{𝑜}\approx A\leftrightarrow \exists ff:1_{𝑜}\underset{1-1\; onto}{⟶}A\right)$$
60	29 4	sylibr	$$⊢2_{𝑜}\preccurlyeq A\to \varnothing \prec A$$
61	56 6	syl	$$⊢2_{𝑜}\preccurlyeq A\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
62	60 61	mpbid	$$⊢2_{𝑜}\preccurlyeq A\to A\ne \varnothing$$
63		f1ocnv	$$⊢f:1_{𝑜}\underset{1-1\; onto}{⟶}A\to f^{-1}:A\underset{1-1\; onto}{⟶}{1}_{𝑜}$$
64		f1of1	$$⊢f^{-1}:A\underset{1-1\; onto}{⟶}{1}_{𝑜}\to f^{-1}:A\underset{1-1}{⟶}{1}_{𝑜}$$
65		f1eq3	$$⊢1_{𝑜}=\left\{\varnothing \right\}\to \left(f^{-1}:A\underset{1-1}{⟶}{1}_{𝑜}\leftrightarrow f^{-1}:A\underset{1-1}{⟶}\left\{\varnothing \right\}\right)$$
66	12 65	ax-mp	$$⊢f^{-1}:A\underset{1-1}{⟶}{1}_{𝑜}\leftrightarrow f^{-1}:A\underset{1-1}{⟶}\left\{\varnothing \right\}$$
67	64 66	sylib	$$⊢f^{-1}:A\underset{1-1\; onto}{⟶}{1}_{𝑜}\to f^{-1}:A\underset{1-1}{⟶}\left\{\varnothing \right\}$$
68	63 67	syl	$$⊢f:1_{𝑜}\underset{1-1\; onto}{⟶}A\to f^{-1}:A\underset{1-1}{⟶}\left\{\varnothing \right\}$$
69		f1cdmsn	$$⊢\left(f^{-1}:A\underset{1-1}{⟶}\left\{\varnothing \right\}\wedge A\ne \varnothing \right)\to \exists xA=\left\{x\right\}$$
70	68 69	sylan	$$⊢\left(f:1_{𝑜}\underset{1-1\; onto}{⟶}A\wedge A\ne \varnothing \right)\to \exists xA=\left\{x\right\}$$
71	70	expcom	$$⊢A\ne \varnothing \to \left(f:1_{𝑜}\underset{1-1\; onto}{⟶}A\to \exists xA=\left\{x\right\}\right)$$
72	71	exlimdv	$$⊢A\ne \varnothing \to \left(\exists ff:1_{𝑜}\underset{1-1\; onto}{⟶}A\to \exists xA=\left\{x\right\}\right)$$
73	62 72	syl	$$⊢2_{𝑜}\preccurlyeq A\to \left(\exists ff:1_{𝑜}\underset{1-1\; onto}{⟶}A\to \exists xA=\left\{x\right\}\right)$$
74	59 73	sylbid	$$⊢2_{𝑜}\preccurlyeq A\to \left(1_{𝑜}\approx A\to \exists xA=\left\{x\right\}\right)$$
75	54 74	mtod	$$⊢2_{𝑜}\preccurlyeq A\to \neg 1_{𝑜}\approx A$$
76		brsdom	$$⊢1_{𝑜}\prec A\leftrightarrow \left(1_{𝑜}\preccurlyeq A\wedge \neg 1_{𝑜}\approx A\right)$$
77	29 75 76	sylanbrc	$$⊢2_{𝑜}\preccurlyeq A\to 1_{𝑜}\prec A$$
78	24 77	impbii	$$⊢1_{𝑜}\prec A\leftrightarrow 2_{𝑜}\preccurlyeq A$$