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

Theorem fisupg 7105
 Description: Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
fisupg
Distinct variable groups:   ,,,   ,,,

Proof of Theorem fisupg
StepHypRef Expression
1 fimaxg 7104 . 2
2 sotrieq2 4342 . . . . . . . . . . 11
32simprbda 606 . . . . . . . . . 10
43ex 423 . . . . . . . . 9
54anassrs 629 . . . . . . . 8
65a1dd 42 . . . . . . 7
7 pm2.27 35 . . . . . . . 8
8 so2nr 4338 . . . . . . . . . 10
9 pm3.21 435 . . . . . . . . . . 11
109con3d 125 . . . . . . . . . 10
118, 10syl5com 26 . . . . . . . . 9
1211anassrs 629 . . . . . . . 8
137, 12syl9r 67 . . . . . . 7
146, 13pm2.61dne 2523 . . . . . 6
1514ralimdva 2621 . . . . 5
16 breq2 4027 . . . . . . . . 9
1716rspcev 2884 . . . . . . . 8
1817ex 423 . . . . . . 7
1918ralrimivw 2627 . . . . . 6
2019adantl 452 . . . . 5
2115, 20jctird 528 . . . 4
2221reximdva 2655 . . 3