This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝐴 ≠ ∅ ) → ∪ 𝐴 ∈ 𝐴 )