Metamath Proof Explorer

Theorem nnubfi

Description: A bounded above set of positive integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 28-Feb-2014)

Ref Expression
Assertion nnubfi 
|- ( ( A C_ NN /\ B e. NN ) -> { x e. A | x < B } e. Fin )

Proof

Step Hyp Ref Expression
1 fzfi 
 |-  ( 0 ... B ) e. Fin
2 ssel2 
 |-  ( ( A C_ NN /\ x e. A ) -> x e. NN )
3 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
4 2 3 syl 
 |-  ( ( A C_ NN /\ x e. A ) -> x e. NN0 )
5 4 adantlr 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ x e. A ) -> x e. NN0 )
6 5 adantr 
 |-  ( ( ( ( A C_ NN /\ B e. NN ) /\ x e. A ) /\ x < B ) -> x e. NN0 )
7 nnnn0 
 |-  ( B e. NN -> B e. NN0 )
8 7 ad3antlr 
 |-  ( ( ( ( A C_ NN /\ B e. NN ) /\ x e. A ) /\ x < B ) -> B e. NN0 )
9 nnre 
 |-  ( x e. NN -> x e. RR )
10 2 9 syl 
 |-  ( ( A C_ NN /\ x e. A ) -> x e. RR )
11 10 adantlr 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ x e. A ) -> x e. RR )
12 nnre 
 |-  ( B e. NN -> B e. RR )
13 12 ad2antlr 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ x e. A ) -> B e. RR )
14 ltle 
 |-  ( ( x e. RR /\ B e. RR ) -> ( x < B -> x <_ B ) )
15 11 13 14 syl2anc 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ x e. A ) -> ( x < B -> x <_ B ) )
16 15 imp 
 |-  ( ( ( ( A C_ NN /\ B e. NN ) /\ x e. A ) /\ x < B ) -> x <_ B )
17 elfz2nn0 
 |-  ( x e. ( 0 ... B ) <-> ( x e. NN0 /\ B e. NN0 /\ x <_ B ) )
18 6 8 16 17 syl3anbrc 
 |-  ( ( ( ( A C_ NN /\ B e. NN ) /\ x e. A ) /\ x < B ) -> x e. ( 0 ... B ) )
19 18 ex 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ x e. A ) -> ( x < B -> x e. ( 0 ... B ) ) )
20 19 ralrimiva 
 |-  ( ( A C_ NN /\ B e. NN ) -> A. x e. A ( x < B -> x e. ( 0 ... B ) ) )
21 rabss 
 |-  ( { x e. A | x < B } C_ ( 0 ... B ) <-> A. x e. A ( x < B -> x e. ( 0 ... B ) ) )
22 20 21 sylibr 
 |-  ( ( A C_ NN /\ B e. NN ) -> { x e. A | x < B } C_ ( 0 ... B ) )
23 ssfi 
 |-  ( ( ( 0 ... B ) e. Fin /\ { x e. A | x < B } C_ ( 0 ... B ) ) -> { x e. A | x < B } e. Fin )
24 1 22 23 sylancr 
 |-  ( ( A C_ NN /\ B e. NN ) -> { x e. A | x < B } e. Fin )