Theorem 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	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∪ 𝐴 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		epweon	⊢ E We On
2		weso	⊢ ( E We On → E Or On )
3	1 2	ax-mp	⊢ E Or On
4		soss	⊢ ( 𝐴 ⊆ On → ( E Or On → E Or 𝐴 ) )
5	3 4	mpi	⊢ ( 𝐴 ⊆ On → E Or 𝐴 )
6		fimax2g	⊢ ( ( E Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 E 𝑦 )
7	5 6	syl3an1	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 E 𝑦 )
8		ssel2	⊢ ( ( 𝐴 ⊆ On ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
9	8	adantlr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
10		ssel2	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
11	10	adantr	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ On )
12		epel	⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
13	12	notbii	⊢ ( ¬ 𝑥 E 𝑦 ↔ ¬ 𝑥 ∈ 𝑦 )
14		ontri1	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝑦 ) )
15	13 14	bitr4id	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( ¬ 𝑥 E 𝑦 ↔ 𝑦 ⊆ 𝑥 ) )
16	9 11 15	syl2anc	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑥 E 𝑦 ↔ 𝑦 ⊆ 𝑥 ) )
17	16	ralbidva	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 E 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ) )
18		unissb	⊢ ( ∪ 𝐴 ⊆ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 )
19	17 18	bitr4di	⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 E 𝑦 ↔ ∪ 𝐴 ⊆ 𝑥 ) )
20	19	rexbidva	⊢ ( 𝐴 ⊆ On → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 E 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 ∪ 𝐴 ⊆ 𝑥 ) )
21	20	3ad2ant1	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 E 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 ∪ 𝐴 ⊆ 𝑥 ) )
22	7 21	mpbid	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∪ 𝐴 ⊆ 𝑥 )
23		elssuni	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴 )
24		eqss	⊢ ( 𝑥 = ∪ 𝐴 ↔ ( 𝑥 ⊆ ∪ 𝐴 ∧ ∪ 𝐴 ⊆ 𝑥 ) )
25		eleq1	⊢ ( 𝑥 = ∪ 𝐴 → ( 𝑥 ∈ 𝐴 ↔ ∪ 𝐴 ∈ 𝐴 ) )
26	25	biimpcd	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 = ∪ 𝐴 → ∪ 𝐴 ∈ 𝐴 ) )
27	24 26	biimtrrid	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑥 ⊆ ∪ 𝐴 ∧ ∪ 𝐴 ⊆ 𝑥 ) → ∪ 𝐴 ∈ 𝐴 ) )
28	23 27	mpand	⊢ ( 𝑥 ∈ 𝐴 → ( ∪ 𝐴 ⊆ 𝑥 → ∪ 𝐴 ∈ 𝐴 ) )
29	28	rexlimiv	⊢ ( ∃ 𝑥 ∈ 𝐴 ∪ 𝐴 ⊆ 𝑥 → ∪ 𝐴 ∈ 𝐴 )
30	22 29	syl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∪ 𝐴 ∈ 𝐴 )