Theorem 1sdom2dom

Description: Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024)

	Ref	Expression
Assertion	1sdom2dom	|- ( 1o ~< A <-> 2o ~<_ A )

Proof

Step	Hyp	Ref	Expression
1		relsdom	|- Rel ~<
2	1	brrelex2i	|- ( 1o ~< A -> A e. _V )
3		sdomdom	|- ( 1o ~< A -> 1o ~<_ A )
4		0sdom1dom	|- ( (/) ~< A <-> 1o ~<_ A )
5	3 4	sylibr	|- ( 1o ~< A -> (/) ~< A )
6		0sdomg	|- ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
7	2 6	syl	|- ( 1o ~< A -> ( (/) ~< A <-> A =/= (/) ) )
8	5 7	mpbid	|- ( 1o ~< A -> A =/= (/) )
9		n0snor2el	|- ( A =/= (/) -> ( E. x e. A E. y e. A x =/= y \/ E. x A = { x } ) )
10	8 9	syl	|- ( 1o ~< A -> ( E. x e. A E. y e. A x =/= y \/ E. x A = { x } ) )
11		sdomnen	|- ( 1o ~< A -> -. 1o ~~ A )
12		df1o2	|- 1o = { (/) }
13		0ex	|- (/) e. _V
14		vex	|- x e. _V
15		en2sn	|- ( ( (/) e. _V /\ x e. _V ) -> { (/) } ~~ { x } )
16	13 14 15	mp2an	|- { (/) } ~~ { x }
17	12 16	eqbrtri	|- 1o ~~ { x }
18		breq2	|- ( A = { x } -> ( 1o ~~ A <-> 1o ~~ { x } ) )
19	17 18	mpbiri	|- ( A = { x } -> 1o ~~ A )
20	19	exlimiv	|- ( E. x A = { x } -> 1o ~~ A )
21	11 20	nsyl	|- ( 1o ~< A -> -. E. x A = { x } )
22	10 21	olcnd	|- ( 1o ~< A -> E. x e. A E. y e. A x =/= y )
23		rex2dom	|- ( ( A e. _V /\ E. x e. A E. y e. A x =/= y ) -> 2o ~<_ A )
24	2 22 23	syl2anc	|- ( 1o ~< A -> 2o ~<_ A )
25		snsspr1	|- { (/) } C_ { (/) , 1o }
26		df2o3	|- 2o = { (/) , 1o }
27	25 12 26	3sstr4i	|- 1o C_ 2o
28		domssl	|- ( ( 1o C_ 2o /\ 2o ~<_ A ) -> 1o ~<_ A )
29	27 28	mpan	|- ( 2o ~<_ A -> 1o ~<_ A )
30		snnen2o	|- -. { y } ~~ 2o
31	13	a1i	|- ( T. -> (/) e. _V )
32		1oex	|- 1o e. _V
33	32	a1i	|- ( T. -> 1o e. _V )
34		1n0	|- 1o =/= (/)
35	34	nesymi	|- -. (/) = 1o
36	35	a1i	|- ( T. -> -. (/) = 1o )
37	31 33 36	enpr2d	|- ( T. -> { (/) , 1o } ~~ 2o )
38	37	mptru	|- { (/) , 1o } ~~ 2o
39	26 38	eqbrtri	|- 2o ~~ 2o
40		breq1	|- ( 2o = { y } -> ( 2o ~~ 2o <-> { y } ~~ 2o ) )
41	39 40	mpbii	|- ( 2o = { y } -> { y } ~~ 2o )
42	30 41	mto	|- -. 2o = { y }
43	42	nex	|- -. E. y 2o = { y }
44		2on0	|- 2o =/= (/)
45		f1cdmsn	|- ( ( f : 2o -1-1-> { x } /\ 2o =/= (/) ) -> E. y 2o = { y } )
46	44 45	mpan2	|- ( f : 2o -1-1-> { x } -> E. y 2o = { y } )
47	43 46	mto	|- -. f : 2o -1-1-> { x }
48	47	nex	|- -. E. f f : 2o -1-1-> { x }
49		brdomi	|- ( 2o ~<_ { x } -> E. f f : 2o -1-1-> { x } )
50	48 49	mto	|- -. 2o ~<_ { x }
51		breq2	|- ( A = { x } -> ( 2o ~<_ A <-> 2o ~<_ { x } ) )
52	50 51	mtbiri	|- ( A = { x } -> -. 2o ~<_ A )
53	52	con2i	|- ( 2o ~<_ A -> -. A = { x } )
54	53	nexdv	|- ( 2o ~<_ A -> -. E. x A = { x } )
55		reldom	|- Rel ~<_
56	55	brrelex2i	|- ( 2o ~<_ A -> A e. _V )
57		breng	|- ( ( 1o e. _V /\ A e. _V ) -> ( 1o ~~ A <-> E. f f : 1o -1-1-onto-> A ) )
58	32 57	mpan	|- ( A e. _V -> ( 1o ~~ A <-> E. f f : 1o -1-1-onto-> A ) )
59	56 58	syl	|- ( 2o ~<_ A -> ( 1o ~~ A <-> E. f f : 1o -1-1-onto-> A ) )
60	29 4	sylibr	|- ( 2o ~<_ A -> (/) ~< A )
61	56 6	syl	|- ( 2o ~<_ A -> ( (/) ~< A <-> A =/= (/) ) )
62	60 61	mpbid	|- ( 2o ~<_ A -> A =/= (/) )
63		f1ocnv	|- ( f : 1o -1-1-onto-> A -> `' f : A -1-1-onto-> 1o )
64		f1of1	|- ( `' f : A -1-1-onto-> 1o -> `' f : A -1-1-> 1o )
65		f1eq3	|- ( 1o = { (/) } -> ( `' f : A -1-1-> 1o <-> `' f : A -1-1-> { (/) } ) )
66	12 65	ax-mp	|- ( `' f : A -1-1-> 1o <-> `' f : A -1-1-> { (/) } )
67	64 66	sylib	|- ( `' f : A -1-1-onto-> 1o -> `' f : A -1-1-> { (/) } )
68	63 67	syl	|- ( f : 1o -1-1-onto-> A -> `' f : A -1-1-> { (/) } )
69		f1cdmsn	|- ( ( `' f : A -1-1-> { (/) } /\ A =/= (/) ) -> E. x A = { x } )
70	68 69	sylan	|- ( ( f : 1o -1-1-onto-> A /\ A =/= (/) ) -> E. x A = { x } )
71	70	expcom	|- ( A =/= (/) -> ( f : 1o -1-1-onto-> A -> E. x A = { x } ) )
72	71	exlimdv	|- ( A =/= (/) -> ( E. f f : 1o -1-1-onto-> A -> E. x A = { x } ) )
73	62 72	syl	|- ( 2o ~<_ A -> ( E. f f : 1o -1-1-onto-> A -> E. x A = { x } ) )
74	59 73	sylbid	|- ( 2o ~<_ A -> ( 1o ~~ A -> E. x A = { x } ) )
75	54 74	mtod	|- ( 2o ~<_ A -> -. 1o ~~ A )
76		brsdom	|- ( 1o ~< A <-> ( 1o ~<_ A /\ -. 1o ~~ A ) )
77	29 75 76	sylanbrc	|- ( 2o ~<_ A -> 1o ~< A )
78	24 77	impbii	|- ( 1o ~< A <-> 2o ~<_ A )