Theorem ensucne0OLD

Description: A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ensucne0OLD	$$⊢A\approx \mathrm{suc}B\to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		encv	$$⊢A\approx \mathrm{suc}B\to \left(A\in \mathrm{V}\wedge \mathrm{suc}B\in \mathrm{V}\right)$$
2	1	simprd	$$⊢A\approx \mathrm{suc}B\to \mathrm{suc}B\in \mathrm{V}$$
3		en0	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$
4	3	biimpri	$$⊢A=\varnothing \to A\approx \varnothing$$
5	4	a1i	$$⊢\mathrm{suc}B\in \mathrm{V}\to \left(A=\varnothing \to A\approx \varnothing \right)$$
6		nsuceq0	$$⊢\mathrm{suc}B\ne \varnothing$$
7		0sdomg	$$⊢\mathrm{suc}B\in \mathrm{V}\to \left(\varnothing \prec \mathrm{suc}B\leftrightarrow \mathrm{suc}B\ne \varnothing \right)$$
8	6 7	mpbiri	$$⊢\mathrm{suc}B\in \mathrm{V}\to \varnothing \prec \mathrm{suc}B$$
9	5 8	jctird	$$⊢\mathrm{suc}B\in \mathrm{V}\to \left(A=\varnothing \to \left(A\approx \varnothing \wedge \varnothing \prec \mathrm{suc}B\right)\right)$$
10		ensdomtr	$$⊢\left(A\approx \varnothing \wedge \varnothing \prec \mathrm{suc}B\right)\to A\prec \mathrm{suc}B$$
11		sdomnen	$$⊢A\prec \mathrm{suc}B\to \neg A\approx \mathrm{suc}B$$
12	10 11	syl	$$⊢\left(A\approx \varnothing \wedge \varnothing \prec \mathrm{suc}B\right)\to \neg A\approx \mathrm{suc}B$$
13	9 12	syl6	$$⊢\mathrm{suc}B\in \mathrm{V}\to \left(A=\varnothing \to \neg A\approx \mathrm{suc}B\right)$$
14	13	necon2ad	$$⊢\mathrm{suc}B\in \mathrm{V}\to \left(A\approx \mathrm{suc}B\to A\ne \varnothing \right)$$
15	2 14	mpcom	$$⊢A\approx \mathrm{suc}B\to A\ne \varnothing$$