ordunisuc2

Description: An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005)

		Ref	Expression
	Assertion	ordunisuc2	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \forall x \in A suc x \in A)$

Proof

Step	Hyp	Ref	Expression
1		orduninsuc	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \neg \exists x \in On A = suc x)$
2		ralnex	$⊢ \forall x \in On \neg A = suc x \leftrightarrow \neg \exists x \in On A = suc x$
3		suceloni	$⊢ x \in On \to suc x \in On$
4		eloni	$⊢ suc x \in On \to Ord suc x$
5	3 4	syl	$⊢ x \in On \to Ord suc x$
6		ordtri3	$⊢ (Ord A \land Ord suc x) \to (A = suc x \leftrightarrow \neg (A \in suc x \lor suc x \in A))$
7	5 6	sylan2	$⊢ (Ord A \land x \in On) \to (A = suc x \leftrightarrow \neg (A \in suc x \lor suc x \in A))$
8	7	con2bid	$⊢ (Ord A \land x \in On) \to ((A \in suc x \lor suc x \in A) \leftrightarrow \neg A = suc x)$
9		onnbtwn	$⊢ x \in On \to \neg (x \in A \land A \in suc x)$
10		imnan	$⊢ (x \in A \to \neg A \in suc x) \leftrightarrow \neg (x \in A \land A \in suc x)$
11	9 10	sylibr	$⊢ x \in On \to (x \in A \to \neg A \in suc x)$
12	11	con2d	$⊢ x \in On \to (A \in suc x \to \neg x \in A)$
13		pm2.21	$⊢ \neg x \in A \to (x \in A \to suc x \in A)$
14	12 13	syl6	$⊢ x \in On \to (A \in suc x \to (x \in A \to suc x \in A))$
15	14	adantl	$⊢ (Ord A \land x \in On) \to (A \in suc x \to (x \in A \to suc x \in A))$
16		ax-1	$⊢ suc x \in A \to (x \in A \to suc x \in A)$
17	16	a1i	$⊢ (Ord A \land x \in On) \to (suc x \in A \to (x \in A \to suc x \in A))$
18	15 17	jaod	$⊢ (Ord A \land x \in On) \to ((A \in suc x \lor suc x \in A) \to (x \in A \to suc x \in A))$
19		eloni	$⊢ x \in On \to Ord x$
20		ordtri2or	$⊢ (Ord x \land Ord A) \to (x \in A \lor A \subseteq x)$
21	19 20	sylan	$⊢ (x \in On \land Ord A) \to (x \in A \lor A \subseteq x)$
22	21	ancoms	$⊢ (Ord A \land x \in On) \to (x \in A \lor A \subseteq x)$
23	22	orcomd	$⊢ (Ord A \land x \in On) \to (A \subseteq x \lor x \in A)$
24	23	adantr	$⊢ ((Ord A \land x \in On) \land (x \in A \to suc x \in A)) \to (A \subseteq x \lor x \in A)$
25		ordsssuc2	$⊢ (Ord A \land x \in On) \to (A \subseteq x \leftrightarrow A \in suc x)$
26	25	biimpd	$⊢ (Ord A \land x \in On) \to (A \subseteq x \to A \in suc x)$
27	26	adantr	$⊢ ((Ord A \land x \in On) \land (x \in A \to suc x \in A)) \to (A \subseteq x \to A \in suc x)$
28		simpr	$⊢ ((Ord A \land x \in On) \land (x \in A \to suc x \in A)) \to (x \in A \to suc x \in A)$
29	27 28	orim12d	$⊢ ((Ord A \land x \in On) \land (x \in A \to suc x \in A)) \to ((A \subseteq x \lor x \in A) \to (A \in suc x \lor suc x \in A))$
30	24 29	mpd	$⊢ ((Ord A \land x \in On) \land (x \in A \to suc x \in A)) \to (A \in suc x \lor suc x \in A)$
31	30	ex	$⊢ (Ord A \land x \in On) \to ((x \in A \to suc x \in A) \to (A \in suc x \lor suc x \in A))$
32	18 31	impbid	$⊢ (Ord A \land x \in On) \to ((A \in suc x \lor suc x \in A) \leftrightarrow (x \in A \to suc x \in A))$
33	8 32	bitr3d	$⊢ (Ord A \land x \in On) \to (\neg A = suc x \leftrightarrow (x \in A \to suc x \in A))$
34	33	pm5.74da	$⊢ Ord A \to ((x \in On \to \neg A = suc x) \leftrightarrow (x \in On \to (x \in A \to suc x \in A)))$
35		impexp	$⊢ ((x \in On \land x \in A) \to suc x \in A) \leftrightarrow (x \in On \to (x \in A \to suc x \in A))$
36		simpr	$⊢ (x \in On \land x \in A) \to x \in A$
37		ordelon	$⊢ (Ord A \land x \in A) \to x \in On$
38	37	ex	$⊢ Ord A \to (x \in A \to x \in On)$
39	38	ancrd	$⊢ Ord A \to (x \in A \to (x \in On \land x \in A))$
40	36 39	impbid2	$⊢ Ord A \to ((x \in On \land x \in A) \leftrightarrow x \in A)$
41	40	imbi1d	$⊢ Ord A \to (((x \in On \land x \in A) \to suc x \in A) \leftrightarrow (x \in A \to suc x \in A))$
42	35 41	bitr3id	$⊢ Ord A \to ((x \in On \to (x \in A \to suc x \in A)) \leftrightarrow (x \in A \to suc x \in A))$
43	34 42	bitrd	$⊢ Ord A \to ((x \in On \to \neg A = suc x) \leftrightarrow (x \in A \to suc x \in A))$
44	43	ralbidv2	$⊢ Ord A \to (\forall x \in On \neg A = suc x \leftrightarrow \forall x \in A suc x \in A)$
45	2 44	bitr3id	$⊢ Ord A \to (\neg \exists x \in On A = suc x \leftrightarrow \forall x \in A suc x \in A)$
46	1 45	bitrd	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \forall x \in A suc x \in A)$

Metamath Proof Explorer

Theorem ordunisuc2

Proof