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

Theorem ordunifi 7357
 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 4764 . . . . . 6
2 weso 4573 . . . . . 6
31, 2ax-mp 8 . . . . 5
4 soss 4521 . . . . 5
53, 4mpi 17 . . . 4
6 fimax2g 7353 . . . 4
75, 6syl3an1 1217 . . 3
8 ssel2 3343 . . . . . . . . 9
98adantlr 696 . . . . . . . 8
10 ssel2 3343 . . . . . . . . 9
1110adantr 452 . . . . . . . 8
12 ontri1 4615 . . . . . . . . 9
13 epel 4497 . . . . . . . . . 10
1413notbii 288 . . . . . . . . 9
1512, 14syl6rbbr 256 . . . . . . . 8
169, 11, 15syl2anc 643 . . . . . . 7
1716ralbidva 2721 . . . . . 6
18 unissb 4045 . . . . . 6
1917, 18syl6bbr 255 . . . . 5
2019rexbidva 2722 . . . 4