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	⊢ ( ∅ ≺ 𝐴 ↔ 1o ≼ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		relsdom	⊢ Rel ≺
2	1	brrelex2i	⊢ ( ∅ ≺ 𝐴 → 𝐴 ∈ V )
3		reldom	⊢ Rel ≼
4	3	brrelex2i	⊢ ( 1o ≼ 𝐴 → 𝐴 ∈ V )
5		0sdomg	⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
6		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
7		snssi	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ⊆ 𝐴 )
8		df1o2	⊢ 1o = { ∅ }
9		0ex	⊢ ∅ ∈ V
10		vex	⊢ 𝑥 ∈ V
11		en2sn	⊢ ( ( ∅ ∈ V ∧ 𝑥 ∈ V ) → { ∅ } ≈ { 𝑥 } )
12	9 10 11	mp2an	⊢ { ∅ } ≈ { 𝑥 }
13	8 12	eqbrtri	⊢ 1o ≈ { 𝑥 }
14		endom	⊢ ( 1o ≈ { 𝑥 } → 1o ≼ { 𝑥 } )
15	13 14	ax-mp	⊢ 1o ≼ { 𝑥 }
16		domssr	⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 } ⊆ 𝐴 ∧ 1o ≼ { 𝑥 } ) → 1o ≼ 𝐴 )
17	15 16	mp3an3	⊢ ( ( 𝐴 ∈ V ∧ { 𝑥 } ⊆ 𝐴 ) → 1o ≼ 𝐴 )
18	17	ex	⊢ ( 𝐴 ∈ V → ( { 𝑥 } ⊆ 𝐴 → 1o ≼ 𝐴 ) )
19	7 18	syl5	⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ 𝐴 → 1o ≼ 𝐴 ) )
20	19	exlimdv	⊢ ( 𝐴 ∈ V → ( ∃ 𝑥 𝑥 ∈ 𝐴 → 1o ≼ 𝐴 ) )
21	6 20	biimtrid	⊢ ( 𝐴 ∈ V → ( 𝐴 ≠ ∅ → 1o ≼ 𝐴 ) )
22		1n0	⊢ 1o ≠ ∅
23		dom0	⊢ ( 1o ≼ ∅ ↔ 1o = ∅ )
24	22 23	nemtbir	⊢ ¬ 1o ≼ ∅
25		breq2	⊢ ( 𝐴 = ∅ → ( 1o ≼ 𝐴 ↔ 1o ≼ ∅ ) )
26	24 25	mtbiri	⊢ ( 𝐴 = ∅ → ¬ 1o ≼ 𝐴 )
27	26	necon2ai	⊢ ( 1o ≼ 𝐴 → 𝐴 ≠ ∅ )
28	21 27	impbid1	⊢ ( 𝐴 ∈ V → ( 𝐴 ≠ ∅ ↔ 1o ≼ 𝐴 ) )
29	5 28	bitrd	⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 1o ≼ 𝐴 ) )
30	2 4 29	pm5.21nii	⊢ ( ∅ ≺ 𝐴 ↔ 1o ≼ 𝐴 )