ordunifi

Description: The maximum of a finite collection of ordinals is in the set. (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 29-Jan-2014)

		Ref	Expression
	Assertion	ordunifi	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to ⋃ A \in A$

Proof

Step	Hyp	Ref	Expression
1		epweon	$⊢ E We On$
2		weso	$⊢ E We On \to E Or On$
3	1 2	ax-mp	$⊢ E Or On$
4		soss	$⊢ A \subseteq On \to (E Or On \to E Or A)$
5	3 4	mpi	$⊢ A \subseteq On \to E Or A$
6		fimax2g	$⊢ (E Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg x E y$
7	5 6	syl3an1	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg x E y$
8		ssel2	$⊢ (A \subseteq On \land y \in A) \to y \in On$
9	8	adantlr	$⊢ ((A \subseteq On \land x \in A) \land y \in A) \to y \in On$
10		ssel2	$⊢ (A \subseteq On \land x \in A) \to x \in On$
11	10	adantr	$⊢ ((A \subseteq On \land x \in A) \land y \in A) \to x \in On$
12		epel	$⊢ x E y \leftrightarrow x \in y$
13	12	notbii	$⊢ \neg x E y \leftrightarrow \neg x \in y$
14		ontri1	$⊢ (y \in On \land x \in On) \to (y \subseteq x \leftrightarrow \neg x \in y)$
15	13 14	bitr4id	$⊢ (y \in On \land x \in On) \to (\neg x E y \leftrightarrow y \subseteq x)$
16	9 11 15	syl2anc	$⊢ ((A \subseteq On \land x \in A) \land y \in A) \to (\neg x E y \leftrightarrow y \subseteq x)$
17	16	ralbidva	$⊢ (A \subseteq On \land x \in A) \to (\forall y \in A \neg x E y \leftrightarrow \forall y \in A y \subseteq x)$
18		unissb	$⊢ ⋃ A \subseteq x \leftrightarrow \forall y \in A y \subseteq x$
19	17 18	bitr4di	$⊢ (A \subseteq On \land x \in A) \to (\forall y \in A \neg x E y \leftrightarrow ⋃ A \subseteq x)$
20	19	rexbidva	$⊢ A \subseteq On \to (\exists x \in A \forall y \in A \neg x E y \leftrightarrow \exists x \in A ⋃ A \subseteq x)$
21	20	3ad2ant1	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to (\exists x \in A \forall y \in A \neg x E y \leftrightarrow \exists x \in A ⋃ A \subseteq x)$
22	7 21	mpbid	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to \exists x \in A ⋃ A \subseteq x$
23		elssuni	$⊢ x \in A \to x \subseteq ⋃ A$
24		eqss	$⊢ x = ⋃ A \leftrightarrow (x \subseteq ⋃ A \land ⋃ A \subseteq x)$
25		eleq1	$⊢ x = ⋃ A \to (x \in A \leftrightarrow ⋃ A \in A)$
26	25	biimpcd	$⊢ x \in A \to (x = ⋃ A \to ⋃ A \in A)$
27	24 26	syl5bir	$⊢ x \in A \to ((x \subseteq ⋃ A \land ⋃ A \subseteq x) \to ⋃ A \in A)$
28	23 27	mpand	$⊢ x \in A \to (⋃ A \subseteq x \to ⋃ A \in A)$
29	28	rexlimiv	$⊢ \exists x \in A ⋃ A \subseteq x \to ⋃ A \in A$
30	22 29	syl	$⊢ (A \subseteq On \land A \in Fin \land A \neq \emptyset) \to ⋃ A \in A$

Metamath Proof Explorer

Theorem ordunifi

Proof