Metamath Proof Explorer

Theorem ordeldif1o

Description: Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025)

		Ref	Expression
	Assertion	ordeldif1o	$⊢ Ord A \to (B \in (A ∖ 1_{𝑜}) \leftrightarrow (B \in A \land B \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
2	1	difeq2i	$⊢ A ∖ 1_{𝑜} = A ∖ suc \emptyset$
3	2	eleq2i	$⊢ B \in (A ∖ 1_{𝑜}) \leftrightarrow B \in (A ∖ suc \emptyset)$
4		eldif	$⊢ B \in (A ∖ suc \emptyset) \leftrightarrow (B \in A \land \neg B \in suc \emptyset)$
5	3 4	bitri	$⊢ B \in (A ∖ 1_{𝑜}) \leftrightarrow (B \in A \land \neg B \in suc \emptyset)$
6		0elon	$⊢ \emptyset \in On$
7		ordelord	$⊢ (Ord A \land B \in A) \to Ord B$
8		ordelsuc	$⊢ (\emptyset \in On \land Ord B) \to (\emptyset \in B \leftrightarrow suc \emptyset \subseteq B)$
9	6 7 8	sylancr	$⊢ (Ord A \land B \in A) \to (\emptyset \in B \leftrightarrow suc \emptyset \subseteq B)$
10		ord0eln0	$⊢ Ord B \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
11	7 10	syl	$⊢ (Ord A \land B \in A) \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
12		eloni	$⊢ \emptyset \in On \to Ord \emptyset$
13		ordsuci	$⊢ Ord \emptyset \to Ord suc \emptyset$
14	6 12 13	mp2b	$⊢ Ord suc \emptyset$
15		ordtri1	$⊢ (Ord suc \emptyset \land Ord B) \to (suc \emptyset \subseteq B \leftrightarrow \neg B \in suc \emptyset)$
16	14 7 15	sylancr	$⊢ (Ord A \land B \in A) \to (suc \emptyset \subseteq B \leftrightarrow \neg B \in suc \emptyset)$
17	9 11 16	3bitr3rd	$⊢ (Ord A \land B \in A) \to (\neg B \in suc \emptyset \leftrightarrow B \neq \emptyset)$
18	17	pm5.32da	$⊢ Ord A \to ((B \in A \land \neg B \in suc \emptyset) \leftrightarrow (B \in A \land B \neq \emptyset))$
19	5 18	bitrid	$⊢ Ord A \to (B \in (A ∖ 1_{𝑜}) \leftrightarrow (B \in A \land B \neq \emptyset))$