Metamath Proof Explorer


Theorem ressiocsup

Description: If the supremum belongs to a set of reals, the set is a subset of the unbounded below, right-closed interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses ressiocsup.a φ A
ressiocsup.s S = sup A * <
ressiocsup.e φ S A
ressiocsup.5 I = −∞ S
Assertion ressiocsup φ A I

Proof

Step Hyp Ref Expression
1 ressiocsup.a φ A
2 ressiocsup.s S = sup A * <
3 ressiocsup.e φ S A
4 ressiocsup.5 I = −∞ S
5 mnfxr −∞ *
6 5 a1i φ x A −∞ *
7 ressxr *
8 7 a1i φ *
9 1 8 sstrd φ A *
10 9 adantr φ x A A *
11 10 supxrcld φ x A sup A * < *
12 2 11 eqeltrid φ x A S *
13 9 sselda φ x A x *
14 1 adantr φ x A A
15 simpr φ x A x A
16 14 15 sseldd φ x A x
17 16 mnfltd φ x A −∞ < x
18 supxrub A * x A x sup A * <
19 10 15 18 syl2anc φ x A x sup A * <
20 2 a1i φ x A S = sup A * <
21 20 eqcomd φ x A sup A * < = S
22 19 21 breqtrd φ x A x S
23 6 12 13 17 22 eliocd φ x A x −∞ S
24 23 4 eleqtrrdi φ x A x I
25 24 ralrimiva φ x A x I
26 dfss3 A I x A x I
27 25 26 sylibr φ A I