Theorem sdomne0

Description: A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025)

	Ref	Expression
Assertion	sdomne0	$$⊢B\prec A\to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		relsdom	$$⊢\mathrm{Rel}\prec$$
2	1	brrelex1i	$$⊢B\prec A\to B\in \mathrm{V}$$
3		breq1	$$⊢B=\varnothing \to \left(B\prec A\leftrightarrow \varnothing \prec A\right)$$
4	3	biimpd	$$⊢B=\varnothing \to \left(B\prec A\to \varnothing \prec A\right)$$
5	4	a1i	$$⊢B\in \mathrm{V}\to \left(B=\varnothing \to \left(B\prec A\to \varnothing \prec A\right)\right)$$
6		0sdomg	$$⊢B\in \mathrm{V}\to \left(\varnothing \prec B\leftrightarrow B\ne \varnothing \right)$$
7		sdomtr	$$⊢\left(\varnothing \prec B\wedge B\prec A\right)\to \varnothing \prec A$$
8	7	ex	$$⊢\varnothing \prec B\to \left(B\prec A\to \varnothing \prec A\right)$$
9	6 8	biimtrrdi	$$⊢B\in \mathrm{V}\to \left(B\ne \varnothing \to \left(B\prec A\to \varnothing \prec A\right)\right)$$
10	5 9	pm2.61dne	$$⊢B\in \mathrm{V}\to \left(B\prec A\to \varnothing \prec A\right)$$
11	2 10	syl	$$⊢B\prec A\to \left(B\prec A\to \varnothing \prec A\right)$$
12	1	brrelex2i	$$⊢\varnothing \prec A\to A\in \mathrm{V}$$
13		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
14	12 13	syl	$$⊢\varnothing \prec A\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
15	14	ibi	$$⊢\varnothing \prec A\to A\ne \varnothing$$
16	11 15	syl6	$$⊢B\prec A\to \left(B\prec A\to A\ne \varnothing \right)$$
17	16	pm2.43i	$$⊢B\prec A\to A\ne \varnothing$$