Theorem 0sdom1dom

Description: Strict dominance over 0 is the same as dominance over 1. For a shorter proof requiring ax-un , see 0sdom1domALT . (Contributed by NM, 28-Sep-2004) Avoid ax-un . (Revised by BTernaryTau, 7-Dec-2024)

	Ref	Expression
Assertion	0sdom1dom	|- ( (/) ~< A <-> 1o ~<_ A )

Proof

Step	Hyp	Ref	Expression
1		relsdom	|- Rel ~<
2	1	brrelex2i	|- ( (/) ~< A -> A e. _V )
3		reldom	|- Rel ~<_
4	3	brrelex2i	|- ( 1o ~<_ A -> A e. _V )
5		0sdomg	|- ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
6		n0	|- ( A =/= (/) <-> E. x x e. A )
7		snssi	|- ( x e. A -> { x } C_ A )
8		df1o2	|- 1o = { (/) }
9		0ex	|- (/) e. _V
10		vex	|- x e. _V
11		en2sn	|- ( ( (/) e. _V /\ x e. _V ) -> { (/) } ~~ { x } )
12	9 10 11	mp2an	|- { (/) } ~~ { x }
13	8 12	eqbrtri	|- 1o ~~ { x }
14		endom	|- ( 1o ~~ { x } -> 1o ~<_ { x } )
15	13 14	ax-mp	|- 1o ~<_ { x }
16		domssr	|- ( ( A e. _V /\ { x } C_ A /\ 1o ~<_ { x } ) -> 1o ~<_ A )
17	15 16	mp3an3	|- ( ( A e. _V /\ { x } C_ A ) -> 1o ~<_ A )
18	17	ex	|- ( A e. _V -> ( { x } C_ A -> 1o ~<_ A ) )
19	7 18	syl5	|- ( A e. _V -> ( x e. A -> 1o ~<_ A ) )
20	19	exlimdv	|- ( A e. _V -> ( E. x x e. A -> 1o ~<_ A ) )
21	6 20	biimtrid	|- ( A e. _V -> ( A =/= (/) -> 1o ~<_ A ) )
22		1n0	|- 1o =/= (/)
23		dom0	|- ( 1o ~<_ (/) <-> 1o = (/) )
24	22 23	nemtbir	|- -. 1o ~<_ (/)
25		breq2	|- ( A = (/) -> ( 1o ~<_ A <-> 1o ~<_ (/) ) )
26	24 25	mtbiri	|- ( A = (/) -> -. 1o ~<_ A )
27	26	necon2ai	|- ( 1o ~<_ A -> A =/= (/) )
28	21 27	impbid1	|- ( A e. _V -> ( A =/= (/) <-> 1o ~<_ A ) )
29	5 28	bitrd	|- ( A e. _V -> ( (/) ~< A <-> 1o ~<_ A ) )
30	2 4 29	pm5.21nii	|- ( (/) ~< A <-> 1o ~<_ A )