Metamath Proof Explorer

Theorem ellimits

Description: Membership in the class of all limit ordinals. (Contributed by Scott Fenton, 11-Apr-2012)

		Ref	Expression
	Hypothesis	ellimits.1	$⊢ A \in V$
	Assertion	ellimits	$⊢ A \in 𝖫𝗂𝗆𝗂𝗍𝗌 \leftrightarrow Lim A$

Proof

Step	Hyp	Ref	Expression
1		ellimits.1	$⊢ A \in V$
2		df-limits	$⊢ 𝖫𝗂𝗆𝗂𝗍𝗌 = (On \cap 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉) ∖ \{\emptyset\}$
3	2	eleq2i	$⊢ A \in 𝖫𝗂𝗆𝗂𝗍𝗌 \leftrightarrow A \in ((On \cap 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉) ∖ \{\emptyset\})$
4		eldif	$⊢ A \in ((On \cap 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉) ∖ \{\emptyset\}) \leftrightarrow (A \in (On \cap 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉) \land \neg A \in \{\emptyset\})$
5		3anan32	$⊢ (Ord A \land A \neq \emptyset \land A = ⋃ A) \leftrightarrow ((Ord A \land A = ⋃ A) \land A \neq \emptyset)$
6		df-lim	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land A = ⋃ A)$
7		elin	$⊢ A \in (On \cap 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉) \leftrightarrow (A \in On \land A \in 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉)$
8	1	elon	$⊢ A \in On \leftrightarrow Ord A$
9	1	elfix	$⊢ A \in 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 \leftrightarrow A 𝖡𝗂𝗀𝖼𝗎𝗉 A$
10	1	brbigcup	$⊢ A 𝖡𝗂𝗀𝖼𝗎𝗉 A \leftrightarrow ⋃ A = A$
11		eqcom	$⊢ ⋃ A = A \leftrightarrow A = ⋃ A$
12	9 10 11	3bitri	$⊢ A \in 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉 \leftrightarrow A = ⋃ A$
13	8 12	anbi12i	$⊢ (A \in On \land A \in 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉) \leftrightarrow (Ord A \land A = ⋃ A)$
14	7 13	bitri	$⊢ A \in (On \cap 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉) \leftrightarrow (Ord A \land A = ⋃ A)$
15	1	elsn	$⊢ A \in \{\emptyset\} \leftrightarrow A = \emptyset$
16	15	necon3bbii	$⊢ \neg A \in \{\emptyset\} \leftrightarrow A \neq \emptyset$
17	14 16	anbi12i	$⊢ (A \in (On \cap 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉) \land \neg A \in \{\emptyset\}) \leftrightarrow ((Ord A \land A = ⋃ A) \land A \neq \emptyset)$
18	5 6 17	3bitr4ri	$⊢ (A \in (On \cap 𝖥𝗂𝗑 𝖡𝗂𝗀𝖼𝗎𝗉) \land \neg A \in \{\emptyset\}) \leftrightarrow Lim A$
19	3 4 18	3bitri	$⊢ A \in 𝖫𝗂𝗆𝗂𝗍𝗌 \leftrightarrow Lim A$