Metamath Proof Explorer

Theorem nninfnub

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

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

Proof

Step Hyp Ref Expression
1 eq0 
 |-  ( { x e. A | B < x } = (/) <-> A. y -. y e. { x e. A | B < x } )
2 breq2 
 |-  ( x = y -> ( B < x <-> B < y ) )
3 2 elrab 
 |-  ( y e. { x e. A | B < x } <-> ( y e. A /\ B < y ) )
4 3 notbii 
 |-  ( -. y e. { x e. A | B < x } <-> -. ( y e. A /\ B < y ) )
5 imnan 
 |-  ( ( y e. A -> -. B < y ) <-> -. ( y e. A /\ B < y ) )
6 4 5 sylbb2 
 |-  ( -. y e. { x e. A | B < x } -> ( y e. A -> -. B < y ) )
7 6 alimi 
 |-  ( A. y -. y e. { x e. A | B < x } -> A. y ( y e. A -> -. B < y ) )
8 7 ralrid 
 |-  ( A. y -. y e. { x e. A | B < x } -> A. y e. A -. B < y )
9 ssel2 
 |-  ( ( A C_ NN /\ y e. A ) -> y e. NN )
10 9 nnred 
 |-  ( ( A C_ NN /\ y e. A ) -> y e. RR )
11 10 adantlr 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) -> y e. RR )
12 nnre 
 |-  ( B e. NN -> B e. RR )
13 12 ad2antlr 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) -> B e. RR )
14 lenlt 
 |-  ( ( y e. RR /\ B e. RR ) -> ( y <_ B <-> -. B < y ) )
15 14 biimprd 
 |-  ( ( y e. RR /\ B e. RR ) -> ( -. B < y -> y <_ B ) )
16 11 13 15 syl2anc 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) -> ( -. B < y -> y <_ B ) )
17 16 ralimdva 
 |-  ( ( A C_ NN /\ B e. NN ) -> ( A. y e. A -. B < y -> A. y e. A y <_ B ) )
18 fzfi 
 |-  ( 0 ... B ) e. Fin
19 9 nnnn0d 
 |-  ( ( A C_ NN /\ y e. A ) -> y e. NN0 )
20 19 adantlr 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) -> y e. NN0 )
21 20 adantr 
 |-  ( ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) /\ y <_ B ) -> y e. NN0 )
22 nnnn0 
 |-  ( B e. NN -> B e. NN0 )
23 22 ad3antlr 
 |-  ( ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) /\ y <_ B ) -> B e. NN0 )
24 simpr 
 |-  ( ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) /\ y <_ B ) -> y <_ B )
25 21 23 24 3jca 
 |-  ( ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) /\ y <_ B ) -> ( y e. NN0 /\ B e. NN0 /\ y <_ B ) )
26 25 ex 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) -> ( y <_ B -> ( y e. NN0 /\ B e. NN0 /\ y <_ B ) ) )
27 elfz2nn0 
 |-  ( y e. ( 0 ... B ) <-> ( y e. NN0 /\ B e. NN0 /\ y <_ B ) )
28 26 27 imbitrrdi 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ y e. A ) -> ( y <_ B -> y e. ( 0 ... B ) ) )
29 28 ralimdva 
 |-  ( ( A C_ NN /\ B e. NN ) -> ( A. y e. A y <_ B -> A. y e. A y e. ( 0 ... B ) ) )
30 29 imp 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ A. y e. A y <_ B ) -> A. y e. A y e. ( 0 ... B ) )
31 dfss3 
 |-  ( A C_ ( 0 ... B ) <-> A. y e. A y e. ( 0 ... B ) )
32 30 31 sylibr 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ A. y e. A y <_ B ) -> A C_ ( 0 ... B ) )
33 ssfi 
 |-  ( ( ( 0 ... B ) e. Fin /\ A C_ ( 0 ... B ) ) -> A e. Fin )
34 18 32 33 sylancr 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ A. y e. A y <_ B ) -> A e. Fin )
35 34 ex 
 |-  ( ( A C_ NN /\ B e. NN ) -> ( A. y e. A y <_ B -> A e. Fin ) )
36 17 35 syld 
 |-  ( ( A C_ NN /\ B e. NN ) -> ( A. y e. A -. B < y -> A e. Fin ) )
37 8 36 syl5 
 |-  ( ( A C_ NN /\ B e. NN ) -> ( A. y -. y e. { x e. A | B < x } -> A e. Fin ) )
38 1 37 biimtrid 
 |-  ( ( A C_ NN /\ B e. NN ) -> ( { x e. A | B < x } = (/) -> A e. Fin ) )
39 38 necon3bd 
 |-  ( ( A C_ NN /\ B e. NN ) -> ( -. A e. Fin -> { x e. A | B < x } =/= (/) ) )
40 39 imp 
 |-  ( ( ( A C_ NN /\ B e. NN ) /\ -. A e. Fin ) -> { x e. A | B < x } =/= (/) )
41 40 an32s 
 |-  ( ( ( A C_ NN /\ -. A e. Fin ) /\ B e. NN ) -> { x e. A | B < x } =/= (/) )
42 41 3impa 
 |-  ( ( A C_ NN /\ -. A e. Fin /\ B e. NN ) -> { x e. A | B < x } =/= (/) )