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 ≺ 𝐴 ↔ 2o ≼ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		relsdom	⊢ Rel ≺
2	1	brrelex2i	⊢ ( 1o ≺ 𝐴 → 𝐴 ∈ V )
3		sdomdom	⊢ ( 1o ≺ 𝐴 → 1o ≼ 𝐴 )
4		0sdom1dom	⊢ ( ∅ ≺ 𝐴 ↔ 1o ≼ 𝐴 )
5	3 4	sylibr	⊢ ( 1o ≺ 𝐴 → ∅ ≺ 𝐴 )
6		0sdomg	⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
7	2 6	syl	⊢ ( 1o ≺ 𝐴 → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
8	5 7	mpbid	⊢ ( 1o ≺ 𝐴 → 𝐴 ≠ ∅ )
9		n0snor2el	⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃ 𝑥 𝐴 = { 𝑥 } ) )
10	8 9	syl	⊢ ( 1o ≺ 𝐴 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ∨ ∃ 𝑥 𝐴 = { 𝑥 } ) )
11		sdomnen	⊢ ( 1o ≺ 𝐴 → ¬ 1o ≈ 𝐴 )
12		df1o2	⊢ 1o = { ∅ }
13		0ex	⊢ ∅ ∈ V
14		vex	⊢ 𝑥 ∈ V
15		en2sn	⊢ ( ( ∅ ∈ V ∧ 𝑥 ∈ V ) → { ∅ } ≈ { 𝑥 } )
16	13 14 15	mp2an	⊢ { ∅ } ≈ { 𝑥 }
17	12 16	eqbrtri	⊢ 1o ≈ { 𝑥 }
18		breq2	⊢ ( 𝐴 = { 𝑥 } → ( 1o ≈ 𝐴 ↔ 1o ≈ { 𝑥 } ) )
19	17 18	mpbiri	⊢ ( 𝐴 = { 𝑥 } → 1o ≈ 𝐴 )
20	19	exlimiv	⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → 1o ≈ 𝐴 )
21	11 20	nsyl	⊢ ( 1o ≺ 𝐴 → ¬ ∃ 𝑥 𝐴 = { 𝑥 } )
22	10 21	olcnd	⊢ ( 1o ≺ 𝐴 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 )
23		rex2dom	⊢ ( ( 𝐴 ∈ V ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 ) → 2o ≼ 𝐴 )
24	2 22 23	syl2anc	⊢ ( 1o ≺ 𝐴 → 2o ≼ 𝐴 )
25		snsspr1	⊢ { ∅ } ⊆ { ∅ , 1o }
26		df2o3	⊢ 2o = { ∅ , 1o }
27	25 12 26	3sstr4i	⊢ 1o ⊆ 2o
28		domssl	⊢ ( ( 1o ⊆ 2o ∧ 2o ≼ 𝐴 ) → 1o ≼ 𝐴 )
29	27 28	mpan	⊢ ( 2o ≼ 𝐴 → 1o ≼ 𝐴 )
30		snnen2o	⊢ ¬ { 𝑦 } ≈ 2o
31	13	a1i	⊢ ( ⊤ → ∅ ∈ V )
32		1oex	⊢ 1o ∈ V
33	32	a1i	⊢ ( ⊤ → 1o ∈ V )
34		1n0	⊢ 1o ≠ ∅
35	34	nesymi	⊢ ¬ ∅ = 1o
36	35	a1i	⊢ ( ⊤ → ¬ ∅ = 1o )
37	31 33 36	enpr2d	⊢ ( ⊤ → { ∅ , 1o } ≈ 2o )
38	37	mptru	⊢ { ∅ , 1o } ≈ 2o
39	26 38	eqbrtri	⊢ 2o ≈ 2o
40		breq1	⊢ ( 2o = { 𝑦 } → ( 2o ≈ 2o ↔ { 𝑦 } ≈ 2o ) )
41	39 40	mpbii	⊢ ( 2o = { 𝑦 } → { 𝑦 } ≈ 2o )
42	30 41	mto	⊢ ¬ 2o = { 𝑦 }
43	42	nex	⊢ ¬ ∃ 𝑦 2o = { 𝑦 }
44		2on0	⊢ 2o ≠ ∅
45		f1cdmsn	⊢ ( ( 𝑓 : 2o –1-1→ { 𝑥 } ∧ 2o ≠ ∅ ) → ∃ 𝑦 2o = { 𝑦 } )
46	44 45	mpan2	⊢ ( 𝑓 : 2o –1-1→ { 𝑥 } → ∃ 𝑦 2o = { 𝑦 } )
47	43 46	mto	⊢ ¬ 𝑓 : 2o –1-1→ { 𝑥 }
48	47	nex	⊢ ¬ ∃ 𝑓 𝑓 : 2o –1-1→ { 𝑥 }
49		brdomi	⊢ ( 2o ≼ { 𝑥 } → ∃ 𝑓 𝑓 : 2o –1-1→ { 𝑥 } )
50	48 49	mto	⊢ ¬ 2o ≼ { 𝑥 }
51		breq2	⊢ ( 𝐴 = { 𝑥 } → ( 2o ≼ 𝐴 ↔ 2o ≼ { 𝑥 } ) )
52	50 51	mtbiri	⊢ ( 𝐴 = { 𝑥 } → ¬ 2o ≼ 𝐴 )
53	52	con2i	⊢ ( 2o ≼ 𝐴 → ¬ 𝐴 = { 𝑥 } )
54	53	nexdv	⊢ ( 2o ≼ 𝐴 → ¬ ∃ 𝑥 𝐴 = { 𝑥 } )
55		reldom	⊢ Rel ≼
56	55	brrelex2i	⊢ ( 2o ≼ 𝐴 → 𝐴 ∈ V )
57		breng	⊢ ( ( 1o ∈ V ∧ 𝐴 ∈ V ) → ( 1o ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 1o –1-1-onto→ 𝐴 ) )
58	32 57	mpan	⊢ ( 𝐴 ∈ V → ( 1o ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 1o –1-1-onto→ 𝐴 ) )
59	56 58	syl	⊢ ( 2o ≼ 𝐴 → ( 1o ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 1o –1-1-onto→ 𝐴 ) )
60	29 4	sylibr	⊢ ( 2o ≼ 𝐴 → ∅ ≺ 𝐴 )
61	56 6	syl	⊢ ( 2o ≼ 𝐴 → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
62	60 61	mpbid	⊢ ( 2o ≼ 𝐴 → 𝐴 ≠ ∅ )
63		f1ocnv	⊢ ( 𝑓 : 1o –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐴 –1-1-onto→ 1o )
64		f1of1	⊢ ( ◡ 𝑓 : 𝐴 –1-1-onto→ 1o → ◡ 𝑓 : 𝐴 –1-1→ 1o )
65		f1eq3	⊢ ( 1o = { ∅ } → ( ◡ 𝑓 : 𝐴 –1-1→ 1o ↔ ◡ 𝑓 : 𝐴 –1-1→ { ∅ } ) )
66	12 65	ax-mp	⊢ ( ◡ 𝑓 : 𝐴 –1-1→ 1o ↔ ◡ 𝑓 : 𝐴 –1-1→ { ∅ } )
67	64 66	sylib	⊢ ( ◡ 𝑓 : 𝐴 –1-1-onto→ 1o → ◡ 𝑓 : 𝐴 –1-1→ { ∅ } )
68	63 67	syl	⊢ ( 𝑓 : 1o –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐴 –1-1→ { ∅ } )
69		f1cdmsn	⊢ ( ( ◡ 𝑓 : 𝐴 –1-1→ { ∅ } ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )
70	68 69	sylan	⊢ ( ( 𝑓 : 1o –1-1-onto→ 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )
71	70	expcom	⊢ ( 𝐴 ≠ ∅ → ( 𝑓 : 1o –1-1-onto→ 𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
72	71	exlimdv	⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑓 𝑓 : 1o –1-1-onto→ 𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
73	62 72	syl	⊢ ( 2o ≼ 𝐴 → ( ∃ 𝑓 𝑓 : 1o –1-1-onto→ 𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
74	59 73	sylbid	⊢ ( 2o ≼ 𝐴 → ( 1o ≈ 𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
75	54 74	mtod	⊢ ( 2o ≼ 𝐴 → ¬ 1o ≈ 𝐴 )
76		brsdom	⊢ ( 1o ≺ 𝐴 ↔ ( 1o ≼ 𝐴 ∧ ¬ 1o ≈ 𝐴 ) )
77	29 75 76	sylanbrc	⊢ ( 2o ≼ 𝐴 → 1o ≺ 𝐴 )
78	24 77	impbii	⊢ ( 1o ≺ 𝐴 ↔ 2o ≼ 𝐴 )