onsupuni

Description: The supremum of a set of ordinals is the union of that set. Lemma 2.10 of Schloeder p. 5. (Contributed by RP, 19-Jan-2025)

		Ref	Expression
	Assertion	onsupuni	$⊢ (A \subseteq On \land A \in V) \to sup (A, On, E) = ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		ssonuni	$⊢ A \in V \to (A \subseteq On \to ⋃ A \in On)$
2	1	impcom	$⊢ (A \subseteq On \land A \in V) \to ⋃ A \in On$
3		elssuni	$⊢ y \in A \to y \subseteq ⋃ A$
4	3	rgen	$⊢ \forall y \in A y \subseteq ⋃ A$
5		simpl	$⊢ (A \subseteq On \land A \in V) \to A \subseteq On$
6	5	sselda	$⊢ ((A \subseteq On \land A \in V) \land y \in A) \to y \in On$
7	2	adantr	$⊢ ((A \subseteq On \land A \in V) \land y \in A) \to ⋃ A \in On$
8		ontri1	$⊢ (y \in On \land ⋃ A \in On) \to (y \subseteq ⋃ A \leftrightarrow \neg ⋃ A \in y)$
9	6 7 8	syl2anc	$⊢ ((A \subseteq On \land A \in V) \land y \in A) \to (y \subseteq ⋃ A \leftrightarrow \neg ⋃ A \in y)$
10		epel	$⊢ ⋃ A E y \leftrightarrow ⋃ A \in y$
11	10	notbii	$⊢ \neg ⋃ A E y \leftrightarrow \neg ⋃ A \in y$
12	9 11	bitr4di	$⊢ ((A \subseteq On \land A \in V) \land y \in A) \to (y \subseteq ⋃ A \leftrightarrow \neg ⋃ A E y)$
13	12	ralbidva	$⊢ (A \subseteq On \land A \in V) \to (\forall y \in A y \subseteq ⋃ A \leftrightarrow \forall y \in A \neg ⋃ A E y)$
14	4 13	mpbii	$⊢ (A \subseteq On \land A \in V) \to \forall y \in A \neg ⋃ A E y$
15	2	adantr	$⊢ ((A \subseteq On \land A \in V) \land y \in On) \to ⋃ A \in On$
16		epelg	$⊢ ⋃ A \in On \to (y E ⋃ A \leftrightarrow y \in ⋃ A)$
17	15 16	syl	$⊢ ((A \subseteq On \land A \in V) \land y \in On) \to (y E ⋃ A \leftrightarrow y \in ⋃ A)$
18	17	biimpd	$⊢ ((A \subseteq On \land A \in V) \land y \in On) \to (y E ⋃ A \to y \in ⋃ A)$
19		eluni2	$⊢ y \in ⋃ A \leftrightarrow \exists x \in A y \in x$
20		epel	$⊢ y E x \leftrightarrow y \in x$
21	20	rexbii	$⊢ \exists x \in A y E x \leftrightarrow \exists x \in A y \in x$
22	19 21	bitr4i	$⊢ y \in ⋃ A \leftrightarrow \exists x \in A y E x$
23	18 22	imbitrdi	$⊢ ((A \subseteq On \land A \in V) \land y \in On) \to (y E ⋃ A \to \exists x \in A y E x)$
24	23	ralrimiva	$⊢ (A \subseteq On \land A \in V) \to \forall y \in On (y E ⋃ A \to \exists x \in A y E x)$
25		epweon	$⊢ E We On$
26		weso	$⊢ E We On \to E Or On$
27	25 26	mp1i	$⊢ (A \subseteq On \land A \in V) \to E Or On$
28	27	eqsup	$⊢ (A \subseteq On \land A \in V) \to ((⋃ A \in On \land \forall y \in A \neg ⋃ A E y \land \forall y \in On (y E ⋃ A \to \exists x \in A y E x)) \to sup (A, On, E) = ⋃ A)$
29	2 14 24 28	mp3and	$⊢ (A \subseteq On \land A \in V) \to sup (A, On, E) = ⋃ A$

Metamath Proof Explorer

Theorem onsupuni

Proof