Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordunifi Structured version   Visualization version   Unicode version

Theorem ordunifi 7821
 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.)
Assertion
Ref Expression
ordunifi

Proof of Theorem ordunifi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 epweon 6610 . . . . . 6
2 weso 4825 . . . . . 6
31, 2ax-mp 5 . . . . 5
4 soss 4773 . . . . 5
53, 4mpi 20 . . . 4
6 fimax2g 7817 . . . 4
75, 6syl3an1 1301 . . 3
8 ssel2 3427 . . . . . . . . 9
98adantlr 721 . . . . . . . 8
10 ssel2 3427 . . . . . . . . 9
1110adantr 467 . . . . . . . 8
12 ontri1 5457 . . . . . . . . 9
13 epel 4748 . . . . . . . . . 10
1413notbii 298 . . . . . . . . 9
1512, 14syl6rbbr 268 . . . . . . . 8
169, 11, 15syl2anc 667 . . . . . . 7
1716ralbidva 2824 . . . . . 6
18 unissb 4229 . . . . . 6
1917, 18syl6bbr 267 . . . . 5
2019rexbidva 2898 . . . 4