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		onsuc	$⊢ 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		ax1w	$⊢ (Ord A \land x \in On) \to (suc x \in A \to (x \in A \to suc x \in A))$
17	15 16	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))$
18		eloni	$⊢ x \in On \to Ord x$
19		ordtri2or	$⊢ (Ord x \land Ord A) \to (x \in A \lor A \subseteq x)$
20	18 19	sylan	$⊢ (x \in On \land Ord A) \to (x \in A \lor A \subseteq x)$
21	20	ancoms	$⊢ (Ord A \land x \in On) \to (x \in A \lor A \subseteq x)$
22	21	orcomd	$⊢ (Ord A \land x \in On) \to (A \subseteq x \lor x \in A)$
23	22	adantr	$⊢ ((Ord A \land x \in On) \land (x \in A \to suc x \in A)) \to (A \subseteq x \lor x \in A)$
24		ordsssuc2	$⊢ (Ord A \land x \in On) \to (A \subseteq x \leftrightarrow A \in suc x)$
25	24	biimpd	$⊢ (Ord A \land x \in On) \to (A \subseteq x \to A \in suc x)$
26	25	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)$
27		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)$
28	26 27	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))$
29	23 28	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)$
30	29	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))$
31	17 30	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))$
32	8 31	bitr3d	$⊢ (Ord A \land x \in On) \to (\neg A = suc x \leftrightarrow (x \in A \to suc x \in A))$
33	32	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)))$
34		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))$
35		simpr	$⊢ (x \in On \land x \in A) \to x \in A$
36		ordelon	$⊢ (Ord A \land x \in A) \to x \in On$
37	36	ex	$⊢ Ord A \to (x \in A \to x \in On)$
38	37	ancrd	$⊢ Ord A \to (x \in A \to (x \in On \land x \in A))$
39	35 38	impbid2	$⊢ Ord A \to ((x \in On \land x \in A) \leftrightarrow x \in A)$
40	39	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))$
41	34 40	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))$
42	33 41	bitrd	$⊢ Ord A \to ((x \in On \to \neg A = suc x) \leftrightarrow (x \in A \to suc x \in A))$
43	42	ralbidv2	$⊢ Ord A \to (\forall x \in On \neg A = suc x \leftrightarrow \forall x \in A suc x \in A)$
44	2 43	bitr3id	$⊢ Ord A \to (\neg \exists x \in On A = suc x \leftrightarrow \forall x \in A suc x \in A)$
45	1 44	bitrd	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \forall x \in A suc x \in A)$

Metamath Proof Explorer

Theorem ordunisuc2

Proof