Theorem 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	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → sup ( 𝐴 , On , E ) = ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssonuni	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) )
2	1	impcom	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ∪ 𝐴 ∈ On )
3		elssuni	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ⊆ ∪ 𝐴 )
4	3	rgen	⊢ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ ∪ 𝐴
5		simpl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ⊆ On )
6	5	sselda	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
7	2	adantr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐴 ) → ∪ 𝐴 ∈ On )
8		ontri1	⊢ ( ( 𝑦 ∈ On ∧ ∪ 𝐴 ∈ On ) → ( 𝑦 ⊆ ∪ 𝐴 ↔ ¬ ∪ 𝐴 ∈ 𝑦 ) )
9	6 7 8	syl2anc	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ⊆ ∪ 𝐴 ↔ ¬ ∪ 𝐴 ∈ 𝑦 ) )
10		epel	⊢ ( ∪ 𝐴 E 𝑦 ↔ ∪ 𝐴 ∈ 𝑦 )
11	10	notbii	⊢ ( ¬ ∪ 𝐴 E 𝑦 ↔ ¬ ∪ 𝐴 ∈ 𝑦 )
12	9 11	bitr4di	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ⊆ ∪ 𝐴 ↔ ¬ ∪ 𝐴 E 𝑦 ) )
13	12	ralbidva	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ ∪ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ∪ 𝐴 E 𝑦 ) )
14	4 13	mpbii	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑦 ∈ 𝐴 ¬ ∪ 𝐴 E 𝑦 )
15	2	adantr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑦 ∈ On ) → ∪ 𝐴 ∈ On )
16		epelg	⊢ ( ∪ 𝐴 ∈ On → ( 𝑦 E ∪ 𝐴 ↔ 𝑦 ∈ ∪ 𝐴 ) )
17	15 16	syl	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑦 ∈ On ) → ( 𝑦 E ∪ 𝐴 ↔ 𝑦 ∈ ∪ 𝐴 ) )
18	17	biimpd	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑦 ∈ On ) → ( 𝑦 E ∪ 𝐴 → 𝑦 ∈ ∪ 𝐴 ) )
19		eluni2	⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 )
20		epel	⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 )
21	20	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 E 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 )
22	19 21	bitr4i	⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 E 𝑥 )
23	18 22	imbitrdi	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑦 ∈ On ) → ( 𝑦 E ∪ 𝐴 → ∃ 𝑥 ∈ 𝐴 𝑦 E 𝑥 ) )
24	23	ralrimiva	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑦 ∈ On ( 𝑦 E ∪ 𝐴 → ∃ 𝑥 ∈ 𝐴 𝑦 E 𝑥 ) )
25		epweon	⊢ E We On
26		weso	⊢ ( E We On → E Or On )
27	25 26	mp1i	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → E Or On )
28	27	eqsup	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → ( ( ∪ 𝐴 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ¬ ∪ 𝐴 E 𝑦 ∧ ∀ 𝑦 ∈ On ( 𝑦 E ∪ 𝐴 → ∃ 𝑥 ∈ 𝐴 𝑦 E 𝑥 ) ) → sup ( 𝐴 , On , E ) = ∪ 𝐴 ) )
29	2 14 24 28	mp3and	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉 ) → sup ( 𝐴 , On , E ) = ∪ 𝐴 )