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

Theorem supxrun 10899
 Description: The supremum of the union of two sets of extended reals equals the largest of their suprema. (Contributed by NM, 19-Jan-2006.)
Assertion
Ref Expression
supxrun

Proof of Theorem supxrun
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 unss 3523 . . . 4
21biimpi 188 . . 3
4 supxrcl 10898 . . 3
6 elun 3490 . . . 4
7 xrltso 10739 . . . . . . . . 9
87a1i 11 . . . . . . . 8
9 xrsupss 10892 . . . . . . . 8
108, 9supub 7467 . . . . . . 7
11103ad2ant1 979 . . . . . 6
12 supxrcl 10898 . . . . . . . . . . . . 13
1312ad2antrr 708 . . . . . . . . . . . 12
144ad2antlr 709 . . . . . . . . . . . 12
15 ssel2 3345 . . . . . . . . . . . . 13
1615adantlr 697 . . . . . . . . . . . 12
17 xrlelttr 10751 . . . . . . . . . . . 12
1813, 14, 16, 17syl3anc 1185 . . . . . . . . . . 11
1918expdimp 428 . . . . . . . . . 10
2019con3d 128 . . . . . . . . 9
2120exp41 595 . . . . . . . 8
2221com34 80 . . . . . . 7
23223imp 1148 . . . . . 6
2411, 23mpdd 39 . . . . 5
257a1i 11 . . . . . . 7
26 xrsupss 10892 . . . . . . 7
2725, 26supub 7467 . . . . . 6
28273ad2ant2 980 . . . . 5
2924, 28jaod 371 . . . 4
306, 29syl5bi 210 . . 3
3130ralrimiv 2790 . 2
32 rexr 9135 . . . . . . 7
33 xrsupss 10892 . . . . . . . 8
3425, 33suplub 7468 . . . . . . 7
3532, 34sylani 637 . . . . . 6
36 elun2 3517 . . . . . . . 8
3736anim1i 553 . . . . . . 7
3837reximi2 2814 . . . . . 6
3935, 38syl6 32 . . . . 5
4039exp3a 427 . . . 4
4140ralrimiv 2790 . . 3