orduninsuc

Description: An ordinal class is equal to its union if and only if it is not the successor of an ordinal. Closed-form generalization of onuninsuci . (Contributed by NM, 18-Feb-2004)

		Ref	Expression
	Assertion	orduninsuc	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x)$

Proof

Step	Hyp	Ref	Expression
1		ordeleqon	$⊢ Ord A \leftrightarrow (A \in On \lor A = On)$
2		id	$⊢ A = if (A \in On, A, \emptyset) \to A = if (A \in On, A, \emptyset)$
3		unieq	$⊢ A = if (A \in On, A, \emptyset) \to ⋃ A = ⋃ if (A \in On, A, \emptyset)$
4	2 3	eqeq12d	$⊢ A = if (A \in On, A, \emptyset) \to (A = ⋃ A \leftrightarrow if (A \in On, A, \emptyset) = ⋃ if (A \in On, A, \emptyset))$
5		eqeq1	$⊢ A = if (A \in On, A, \emptyset) \to (A = suc x \leftrightarrow if (A \in On, A, \emptyset) = suc x)$
6	5	rexbidv	$⊢ A = if (A \in On, A, \emptyset) \to (\exists x \in On A = suc x \leftrightarrow \exists x \in On if (A \in On, A, \emptyset) = suc x)$
7	6	notbid	$⊢ A = if (A \in On, A, \emptyset) \to (\neg \exists x \in On A = suc x \leftrightarrow \neg \exists x \in On if (A \in On, A, \emptyset) = suc x)$
8	4 7	bibi12d	$⊢ A = if (A \in On, A, \emptyset) \to ((A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x) \leftrightarrow (if (A \in On, A, \emptyset) = ⋃ if (A \in On, A, \emptyset) \leftrightarrow \neg \exists x \in On if (A \in On, A, \emptyset) = suc x))$
9		0elon	$⊢ \emptyset \in On$
10	9	elimel	$⊢ if (A \in On, A, \emptyset) \in On$
11	10	onuninsuci	$⊢ if (A \in On, A, \emptyset) = ⋃ if (A \in On, A, \emptyset) \leftrightarrow \neg \exists x \in On if (A \in On, A, \emptyset) = suc x$
12	8 11	dedth	$⊢ A \in On \to (A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x)$
13		unon	$⊢ ⋃ On = On$
14	13	eqcomi	$⊢ On = ⋃ On$
15		onprc	$⊢ \neg On \in V$
16		vex	$⊢ x \in V$
17	16	sucex	$⊢ suc x \in V$
18		eleq1	$⊢ On = suc x \to (On \in V \leftrightarrow suc x \in V)$
19	17 18	mpbiri	$⊢ On = suc x \to On \in V$
20	15 19	mto	$⊢ \neg On = suc x$
21	20	a1i	$⊢ x \in On \to \neg On = suc x$
22	21	nrex	$⊢ \neg \exists x \in On On = suc x$
23	14 22	2th	$⊢ On = ⋃ On \leftrightarrow \neg \exists x \in On On = suc x$
24		id	$⊢ A = On \to A = On$
25		unieq	$⊢ A = On \to ⋃ A = ⋃ On$
26	24 25	eqeq12d	$⊢ A = On \to (A = ⋃ A \leftrightarrow On = ⋃ On)$
27		eqeq1	$⊢ A = On \to (A = suc x \leftrightarrow On = suc x)$
28	27	rexbidv	$⊢ A = On \to (\exists x \in On A = suc x \leftrightarrow \exists x \in On On = suc x)$
29	28	notbid	$⊢ A = On \to (\neg \exists x \in On A = suc x \leftrightarrow \neg \exists x \in On On = suc x)$
30	26 29	bibi12d	$⊢ A = On \to ((A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x) \leftrightarrow (On = ⋃ On \leftrightarrow \neg \exists x \in On On = suc x))$
31	23 30	mpbiri	$⊢ A = On \to (A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x)$
32	12 31	jaoi	$⊢ (A \in On \lor A = On) \to (A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x)$
33	1 32	sylbi	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x)$

Metamath Proof Explorer

Theorem orduninsuc

Proof