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