Metamath Proof Explorer

Theorem rabssnn0fi

Description: A subset of the nonnegative integers defined by a restricted class abstraction is finite if there is a nonnegative integer so that for all integers greater than this integer the condition of the class abstraction is not fulfilled. (Contributed by AV, 3-Oct-2019)

Ref Expression
Assertion rabssnn0fi 
|- ( { x e. NN0 | ph } e. Fin <-> E. s e. NN0 A. x e. NN0 ( s < x -> -. ph ) )

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { x e. NN0 | ph } C_ NN0
2 ssnn0fi 
 |-  ( { x e. NN0 | ph } C_ NN0 -> ( { x e. NN0 | ph } e. Fin <-> E. s e. NN0 A. y e. NN0 ( s < y -> y e/ { x e. NN0 | ph } ) ) )
3 nnel 
 |-  ( -. y e/ { x e. NN0 | ph } <-> y e. { x e. NN0 | ph } )
4 nfcv 
 |-  F/_ x y
5 nfcv 
 |-  F/_ x NN0
6 nfsbc1v 
 |-  F/ x [. y / x ]. -. ph
7 6 nfn 
 |-  F/ x -. [. y / x ]. -. ph
8 sbceq2a 
 |-  ( y = x -> ( [. y / x ]. -. ph <-> -. ph ) )
9 8 equcoms 
 |-  ( x = y -> ( [. y / x ]. -. ph <-> -. ph ) )
10 9 con2bid 
 |-  ( x = y -> ( ph <-> -. [. y / x ]. -. ph ) )
11 4 5 7 10 elrabf 
 |-  ( y e. { x e. NN0 | ph } <-> ( y e. NN0 /\ -. [. y / x ]. -. ph ) )
12 11 baib 
 |-  ( y e. NN0 -> ( y e. { x e. NN0 | ph } <-> -. [. y / x ]. -. ph ) )
13 3 12 syl5bb 
 |-  ( y e. NN0 -> ( -. y e/ { x e. NN0 | ph } <-> -. [. y / x ]. -. ph ) )
14 13 con4bid 
 |-  ( y e. NN0 -> ( y e/ { x e. NN0 | ph } <-> [. y / x ]. -. ph ) )
15 14 imbi2d 
 |-  ( y e. NN0 -> ( ( s < y -> y e/ { x e. NN0 | ph } ) <-> ( s < y -> [. y / x ]. -. ph ) ) )
16 15 ralbiia 
 |-  ( A. y e. NN0 ( s < y -> y e/ { x e. NN0 | ph } ) <-> A. y e. NN0 ( s < y -> [. y / x ]. -. ph ) )
17 nfv 
 |-  F/ x s < y
18 17 6 nfim 
 |-  F/ x ( s < y -> [. y / x ]. -. ph )
19 nfv 
 |-  F/ y ( s < x -> -. ph )
20 breq2 
 |-  ( y = x -> ( s < y <-> s < x ) )
21 20 8 imbi12d 
 |-  ( y = x -> ( ( s < y -> [. y / x ]. -. ph ) <-> ( s < x -> -. ph ) ) )
22 18 19 21 cbvralw 
 |-  ( A. y e. NN0 ( s < y -> [. y / x ]. -. ph ) <-> A. x e. NN0 ( s < x -> -. ph ) )
23 16 22 bitri 
 |-  ( A. y e. NN0 ( s < y -> y e/ { x e. NN0 | ph } ) <-> A. x e. NN0 ( s < x -> -. ph ) )
24 23 a1i 
 |-  ( ( { x e. NN0 | ph } C_ NN0 /\ s e. NN0 ) -> ( A. y e. NN0 ( s < y -> y e/ { x e. NN0 | ph } ) <-> A. x e. NN0 ( s < x -> -. ph ) ) )
25 24 rexbidva 
 |-  ( { x e. NN0 | ph } C_ NN0 -> ( E. s e. NN0 A. y e. NN0 ( s < y -> y e/ { x e. NN0 | ph } ) <-> E. s e. NN0 A. x e. NN0 ( s < x -> -. ph ) ) )
26 2 25 bitrd 
 |-  ( { x e. NN0 | ph } C_ NN0 -> ( { x e. NN0 | ph } e. Fin <-> E. s e. NN0 A. x e. NN0 ( s < x -> -. ph ) ) )
27 1 26 ax-mp 
 |-  ( { x e. NN0 | ph } e. Fin <-> E. s e. NN0 A. x e. NN0 ( s < x -> -. ph ) )