orddif

Description: Ordinal derived from its successor. (Contributed by NM, 20-May-1998)

		Ref	Expression
	Assertion	orddif	$⊢ Ord A \to A = suc A ∖ \{A\}$

Step	Hyp	Ref	Expression
1		orddisj	$⊢ Ord A \to A \cap \{A\} = \emptyset$
2		disj3	$⊢ A \cap \{A\} = \emptyset \leftrightarrow A = A ∖ \{A\}$
3		df-suc	$⊢ suc A = A \cup \{A\}$
4	3	difeq1i	$⊢ suc A ∖ \{A\} = (A \cup \{A\}) ∖ \{A\}$
5		difun2	$⊢ (A \cup \{A\}) ∖ \{A\} = A ∖ \{A\}$
6	4 5	eqtri	$⊢ suc A ∖ \{A\} = A ∖ \{A\}$
7	6	eqeq2i	$⊢ A = suc A ∖ \{A\} \leftrightarrow A = A ∖ \{A\}$
8	2 7	bitr4i	$⊢ A \cap \{A\} = \emptyset \leftrightarrow A = suc A ∖ \{A\}$
9	1 8	sylib	$⊢ Ord A \to A = suc A ∖ \{A\}$

Metamath Proof Explorer