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 x0|φFins0x0s<x¬φ

Proof

Step Hyp Ref Expression
1 ssrab2 x0|φ0
2 ssnn0fi x0|φ0x0|φFins0y0s<yyx0|φ
3 nnel ¬yx0|φyx0|φ
4 nfcv _xy
5 nfcv _x0
6 nfsbc1v x[˙y/x]˙¬φ
7 6 nfn x¬[˙y/x]˙¬φ
8 sbceq2a y=x[˙y/x]˙¬φ¬φ
9 8 equcoms x=y[˙y/x]˙¬φ¬φ
10 9 con2bid x=yφ¬[˙y/x]˙¬φ
11 4 5 7 10 elrabf yx0|φy0¬[˙y/x]˙¬φ
12 11 baib y0yx0|φ¬[˙y/x]˙¬φ
13 3 12 syl5bb y0¬yx0|φ¬[˙y/x]˙¬φ
14 13 con4bid y0yx0|φ[˙y/x]˙¬φ
15 14 imbi2d y0s<yyx0|φs<y[˙y/x]˙¬φ
16 15 ralbiia y0s<yyx0|φy0s<y[˙y/x]˙¬φ
17 nfv xs<y
18 17 6 nfim xs<y[˙y/x]˙¬φ
19 nfv ys<x¬φ
20 breq2 y=xs<ys<x
21 20 8 imbi12d y=xs<y[˙y/x]˙¬φs<x¬φ
22 18 19 21 cbvralw y0s<y[˙y/x]˙¬φx0s<x¬φ
23 16 22 bitri y0s<yyx0|φx0s<x¬φ
24 23 a1i x0|φ0s0y0s<yyx0|φx0s<x¬φ
25 24 rexbidva x0|φ0s0y0s<yyx0|φs0x0s<x¬φ
26 2 25 bitrd x0|φ0x0|φFins0x0s<x¬φ
27 1 26 ax-mp x0|φFins0x0s<x¬φ