Metamath Proof Explorer

Theorem suprfinzcl

Description: The supremum of a nonempty finite set of integers is a member of the set. (Contributed by AV, 1-Oct-2019)

Ref Expression
Assertion suprfinzcl 
|- ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> sup ( A , RR , < ) e. A )

Proof

Step Hyp Ref Expression
1 zssre 
 |-  ZZ C_ RR
2 ltso 
 |-  < Or RR
3 soss 
 |-  ( ZZ C_ RR -> ( < Or RR -> < Or ZZ ) )
4 1 2 3 mp2 
 |-  < Or ZZ
5 4 a1i 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> < Or ZZ )
6 simp3 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> A e. Fin )
7 simp2 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> A =/= (/) )
8 simp1 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> A C_ ZZ )
9 fisup2g 
 |-  ( ( < Or ZZ /\ ( A e. Fin /\ A =/= (/) /\ A C_ ZZ ) ) -> E. r e. A ( A. a e. A -. r < a /\ A. a e. ZZ ( a < r -> E. b e. A a < b ) ) )
10 5 6 7 8 9 syl13anc 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> E. r e. A ( A. a e. A -. r < a /\ A. a e. ZZ ( a < r -> E. b e. A a < b ) ) )
11 id 
 |-  ( A C_ ZZ -> A C_ ZZ )
12 11 1 sstrdi 
 |-  ( A C_ ZZ -> A C_ RR )
13 12 3ad2ant1 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> A C_ RR )
14 ssrexv 
 |-  ( A C_ RR -> ( E. r e. A ( A. a e. A -. r < a /\ A. a e. ZZ ( a < r -> E. b e. A a < b ) ) -> E. r e. RR ( A. a e. A -. r < a /\ A. a e. ZZ ( a < r -> E. b e. A a < b ) ) ) )
15 13 14 syl 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> ( E. r e. A ( A. a e. A -. r < a /\ A. a e. ZZ ( a < r -> E. b e. A a < b ) ) -> E. r e. RR ( A. a e. A -. r < a /\ A. a e. ZZ ( a < r -> E. b e. A a < b ) ) ) )
16 ssel2 
 |-  ( ( A C_ ZZ /\ a e. A ) -> a e. ZZ )
17 16 zred 
 |-  ( ( A C_ ZZ /\ a e. A ) -> a e. RR )
18 17 ex 
 |-  ( A C_ ZZ -> ( a e. A -> a e. RR ) )
19 18 3ad2ant1 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> ( a e. A -> a e. RR ) )
20 19 adantr 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) /\ r e. RR ) -> ( a e. A -> a e. RR ) )
21 20 imp 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) /\ r e. RR ) /\ a e. A ) -> a e. RR )
22 simplr 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) /\ r e. RR ) /\ a e. A ) -> r e. RR )
23 21 22 lenltd 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) /\ r e. RR ) /\ a e. A ) -> ( a <_ r <-> -. r < a ) )
24 23 bicomd 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) /\ r e. RR ) /\ a e. A ) -> ( -. r < a <-> a <_ r ) )
25 24 ralbidva 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) /\ r e. RR ) -> ( A. a e. A -. r < a <-> A. a e. A a <_ r ) )
26 25 biimpd 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) /\ r e. RR ) -> ( A. a e. A -. r < a -> A. a e. A a <_ r ) )
27 26 adantrd 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) /\ r e. RR ) -> ( ( A. a e. A -. r < a /\ A. a e. ZZ ( a < r -> E. b e. A a < b ) ) -> A. a e. A a <_ r ) )
28 27 reximdva 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> ( E. r e. RR ( A. a e. A -. r < a /\ A. a e. ZZ ( a < r -> E. b e. A a < b ) ) -> E. r e. RR A. a e. A a <_ r ) )
29 15 28 syld 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> ( E. r e. A ( A. a e. A -. r < a /\ A. a e. ZZ ( a < r -> E. b e. A a < b ) ) -> E. r e. RR A. a e. A a <_ r ) )
30 10 29 mpd 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> E. r e. RR A. a e. A a <_ r )
31 suprzcl 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. r e. RR A. a e. A a <_ r ) -> sup ( A , RR , < ) e. A )
32 30 31 syld3an3 
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ A e. Fin ) -> sup ( A , RR , < ) e. A )