Theorem sdomne0d

Description: A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024)

	Ref	Expression
Hypotheses	sdomne0d.a	$$⊢\phi \to B\prec A$$
	sdomne0d.b	$$⊢\phi \to B\in V$$
Assertion	sdomne0d	$$⊢\phi \to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		sdomne0d.a	$$⊢\phi \to B\prec A$$
2		sdomne0d.b	$$⊢\phi \to B\in 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 V\to \left(B=\varnothing \to \left(B\prec A\to \varnothing \prec A\right)\right)$$
6		0sdomg	$$⊢B\in 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	syl6bir	$$⊢B\in V\to \left(B\ne \varnothing \to \left(B\prec A\to \varnothing \prec A\right)\right)$$
10	5 9	pm2.61dne	$$⊢B\in V\to \left(B\prec A\to \varnothing \prec A\right)$$
11	2 10	syl	$$⊢\phi \to \left(B\prec A\to \varnothing \prec A\right)$$
12		relsdom	$$⊢\mathrm{Rel}\prec$$
13	12	brrelex2i	$$⊢\varnothing \prec A\to A\in \mathrm{V}$$
14		0sdomg	$$⊢A\in \mathrm{V}\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
15	13 14	syl	$$⊢\varnothing \prec A\to \left(\varnothing \prec A\leftrightarrow A\ne \varnothing \right)$$
16	15	ibi	$$⊢\varnothing \prec A\to A\ne \varnothing$$
17	11 16	syl6	$$⊢\phi \to \left(B\prec A\to A\ne \varnothing \right)$$
18	1 17	mpd	$$⊢\phi \to A\ne \varnothing$$