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 0 | φ Fin s 0 x 0 s < x ¬ φ

Proof

Step Hyp Ref Expression
1 ssrab2 x 0 | φ 0
2 ssnn0fi x 0 | φ 0 x 0 | φ Fin s 0 y 0 s < y y x 0 | φ
3 nnel ¬ y x 0 | φ y x 0 | φ
4 nfcv _ x y
5 nfcv _ x 0
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 y x 0 | φ y 0 ¬ [˙y / x]˙ ¬ φ
12 11 baib y 0 y x 0 | φ ¬ [˙y / x]˙ ¬ φ
13 3 12 syl5bb y 0 ¬ y x 0 | φ ¬ [˙y / x]˙ ¬ φ
14 13 con4bid y 0 y x 0 | φ [˙y / x]˙ ¬ φ
15 14 imbi2d y 0 s < y y x 0 | φ s < y [˙y / x]˙ ¬ φ
16 15 ralbiia y 0 s < y y x 0 | φ y 0 s < y [˙y / x]˙ ¬ φ
17 nfv x s < y
18 17 6 nfim x s < y [˙y / x]˙ ¬ φ
19 nfv y s < x ¬ φ
20 breq2 y = x s < y s < x
21 20 8 imbi12d y = x s < y [˙y / x]˙ ¬ φ s < x ¬ φ
22 18 19 21 cbvralw y 0 s < y [˙y / x]˙ ¬ φ x 0 s < x ¬ φ
23 16 22 bitri y 0 s < y y x 0 | φ x 0 s < x ¬ φ
24 23 a1i x 0 | φ 0 s 0 y 0 s < y y x 0 | φ x 0 s < x ¬ φ
25 24 rexbidva x 0 | φ 0 s 0 y 0 s < y y x 0 | φ s 0 x 0 s < x ¬ φ
26 2 25 bitrd x 0 | φ 0 x 0 | φ Fin s 0 x 0 s < x ¬ φ
27 1 26 ax-mp x 0 | φ Fin s 0 x 0 s < x ¬ φ