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	$⊢ \emptyset ≺ A \leftrightarrow 1_{𝑜} ≼ A$

Proof

Step	Hyp	Ref	Expression
1		relsdom	$⊢ Rel ≺$
2	1	brrelex2i	$⊢ \emptyset ≺ A \to A \in V$
3		reldom	$⊢ Rel ≼$
4	3	brrelex2i	$⊢ 1_{𝑜} ≼ A \to A \in V$
5		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
6		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
7		snssi	$⊢ x \in A \to \{x\} \subseteq A$
8		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
9		0ex	$⊢ \emptyset \in V$
10		vex	$⊢ x \in V$
11		en2sn	$⊢ (\emptyset \in V \land x \in V) \to \{\emptyset\} \approx \{x\}$
12	9 10 11	mp2an	$⊢ \{\emptyset\} \approx \{x\}$
13	8 12	eqbrtri	$⊢ 1_{𝑜} \approx \{x\}$
14		endom	$⊢ 1_{𝑜} \approx \{x\} \to 1_{𝑜} ≼ \{x\}$
15	13 14	ax-mp	$⊢ 1_{𝑜} ≼ \{x\}$
16		domssr	$⊢ (A \in V \land \{x\} \subseteq A \land 1_{𝑜} ≼ \{x\}) \to 1_{𝑜} ≼ A$
17	15 16	mp3an3	$⊢ (A \in V \land \{x\} \subseteq A) \to 1_{𝑜} ≼ A$
18	17	ex	$⊢ A \in V \to (\{x\} \subseteq A \to 1_{𝑜} ≼ A)$
19	7 18	syl5	$⊢ A \in V \to (x \in A \to 1_{𝑜} ≼ A)$
20	19	exlimdv	$⊢ A \in V \to (\exists x x \in A \to 1_{𝑜} ≼ A)$
21	6 20	biimtrid	$⊢ A \in V \to (A \neq \emptyset \to 1_{𝑜} ≼ A)$
22		1n0	$⊢ 1_{𝑜} \neq \emptyset$
23		dom0	$⊢ 1_{𝑜} ≼ \emptyset \leftrightarrow 1_{𝑜} = \emptyset$
24	22 23	nemtbir	$⊢ \neg 1_{𝑜} ≼ \emptyset$
25		breq2	$⊢ A = \emptyset \to (1_{𝑜} ≼ A \leftrightarrow 1_{𝑜} ≼ \emptyset)$
26	24 25	mtbiri	$⊢ A = \emptyset \to \neg 1_{𝑜} ≼ A$
27	26	necon2ai	$⊢ 1_{𝑜} ≼ A \to A \neq \emptyset$
28	21 27	impbid1	$⊢ A \in V \to (A \neq \emptyset \leftrightarrow 1_{𝑜} ≼ A)$
29	5 28	bitrd	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow 1_{𝑜} ≼ A)$
30	2 4 29	pm5.21nii	$⊢ \emptyset ≺ A \leftrightarrow 1_{𝑜} ≼ A$

Metamath Proof Explorer

Theorem 0sdom1dom

Proof