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 ~< A -> A =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		relsdom	|- Rel ~<
2	1	brrelex1i	|- ( B ~< A -> B e. _V )
3		breq1	|- ( B = (/) -> ( B ~< A <-> (/) ~< A ) )
4	3	biimpd	|- ( B = (/) -> ( B ~< A -> (/) ~< A ) )
5	4	a1i	|- ( B e. _V -> ( B = (/) -> ( B ~< A -> (/) ~< A ) ) )
6		0sdomg	|- ( B e. _V -> ( (/) ~< B <-> B =/= (/) ) )
7		sdomtr	|- ( ( (/) ~< B /\ B ~< A ) -> (/) ~< A )
8	7	ex	|- ( (/) ~< B -> ( B ~< A -> (/) ~< A ) )
9	6 8	biimtrrdi	|- ( B e. _V -> ( B =/= (/) -> ( B ~< A -> (/) ~< A ) ) )
10	5 9	pm2.61dne	|- ( B e. _V -> ( B ~< A -> (/) ~< A ) )
11	2 10	syl	|- ( B ~< A -> ( B ~< A -> (/) ~< A ) )
12	1	brrelex2i	|- ( (/) ~< A -> A e. _V )
13		0sdomg	|- ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
14	12 13	syl	|- ( (/) ~< A -> ( (/) ~< A <-> A =/= (/) ) )
15	14	ibi	|- ( (/) ~< A -> A =/= (/) )
16	11 15	syl6	|- ( B ~< A -> ( B ~< A -> A =/= (/) ) )
17	16	pm2.43i	|- ( B ~< A -> A =/= (/) )