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 syl5bir ( 𝑥𝐴 → ( ( 𝑥 𝐴 𝐴𝑥 ) → 𝐴𝐴 ) )
28 23 27 mpand ( 𝑥𝐴 → ( 𝐴𝑥 𝐴𝐴 ) )
29 28 rexlimiv ( ∃ 𝑥𝐴 𝐴𝑥 𝐴𝐴 )
30 22 29 syl ( ( 𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 𝐴𝐴 )