ondif2

Description: Two ways to say that A is an ordinal greater than one. (Contributed by Mario Carneiro, 21-May-2015)

		Ref	Expression
	Assertion	ondif2	$⊢ A \in (On ∖ 2_{𝑜}) \leftrightarrow (A \in On \land 1_{𝑜} \in A)$

Step	Hyp	Ref	Expression
1		eldif	$⊢ A \in (On ∖ 2_{𝑜}) \leftrightarrow (A \in On \land \neg A \in 2_{𝑜})$
2		1on	$⊢ 1_{𝑜} \in On$
3		ontri1	$⊢ (A \in On \land 1_{𝑜} \in On) \to (A \subseteq 1_{𝑜} \leftrightarrow \neg 1_{𝑜} \in A)$
4		onsssuc	$⊢ (A \in On \land 1_{𝑜} \in On) \to (A \subseteq 1_{𝑜} \leftrightarrow A \in suc 1_{𝑜})$
5		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
6	5	eleq2i	$⊢ A \in 2_{𝑜} \leftrightarrow A \in suc 1_{𝑜}$
7	4 6	bitr4di	$⊢ (A \in On \land 1_{𝑜} \in On) \to (A \subseteq 1_{𝑜} \leftrightarrow A \in 2_{𝑜})$
8	3 7	bitr3d	$⊢ (A \in On \land 1_{𝑜} \in On) \to (\neg 1_{𝑜} \in A \leftrightarrow A \in 2_{𝑜})$
9	2 8	mpan2	$⊢ A \in On \to (\neg 1_{𝑜} \in A \leftrightarrow A \in 2_{𝑜})$
10	9	con1bid	$⊢ A \in On \to (\neg A \in 2_{𝑜} \leftrightarrow 1_{𝑜} \in A)$
11	10	pm5.32i	$⊢ (A \in On \land \neg A \in 2_{𝑜}) \leftrightarrow (A \in On \land 1_{𝑜} \in A)$
12	1 11	bitri	$⊢ A \in (On ∖ 2_{𝑜}) \leftrightarrow (A \in On \land 1_{𝑜} \in A)$

Metamath Proof Explorer