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	$$⊢\left\{x\in {\mathbb{N}}_0|\phi \right\}\in \mathrm{Fin}\leftrightarrow \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to \neg \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$$⊢\left\{x\in {\mathbb{N}}_0|\phi \right\}\subseteq {\mathbb{N}}_0$$
2		ssnn0fi	$$⊢\left\{x\in {\mathbb{N}}_0|\phi \right\}\subseteq {\mathbb{N}}_0\to \left(\left\{x\in {\mathbb{N}}_0|\phi \right\}\in \mathrm{Fin}\leftrightarrow \exists s\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_0\left(s<y\to y\notin \left\{x\in {\mathbb{N}}_0|\phi \right\}\right)\right)$$
3		nnel	$$⊢\neg y\notin \left\{x\in {\mathbb{N}}_0|\phi \right\}\leftrightarrow y\in \left\{x\in {\mathbb{N}}_0|\phi \right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}x{\mathbb{N}}_0$$
6		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi$$
7	6	nfn	$$⊢Ⅎx\neg \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi$$
8		sbceq2a	$$⊢y=x\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \phi \right)$$
9	8	equcoms	$$⊢x=y\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \phi \right)$$
10	9	con2bid	$$⊢x=y\to \left(\phi \leftrightarrow \neg \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)$$
11	4 5 7 10	elrabf	$$⊢y\in \left\{x\in {\mathbb{N}}_0|\phi \right\}\leftrightarrow \left(y\in {\mathbb{N}}_0\wedge \neg \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)$$
12	11	baib	$$⊢y\in {\mathbb{N}}_0\to \left(y\in \left\{x\in {\mathbb{N}}_0|\phi \right\}\leftrightarrow \neg \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)$$
13	3 12	syl5bb	$$⊢y\in {\mathbb{N}}_0\to \left(\neg y\notin \left\{x\in {\mathbb{N}}_0|\phi \right\}\leftrightarrow \neg \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)$$
14	13	con4bid	$$⊢y\in {\mathbb{N}}_0\to \left(y\notin \left\{x\in {\mathbb{N}}_0|\phi \right\}\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)$$
15	14	imbi2d	$$⊢y\in {\mathbb{N}}_0\to \left(\left(s<y\to y\notin \left\{x\in {\mathbb{N}}_0|\phi \right\}\right)\leftrightarrow \left(s<y\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)\right)$$
16	15	ralbiia	$$⊢\forall y\in {\mathbb{N}}_0\left(s<y\to y\notin \left\{x\in {\mathbb{N}}_0|\phi \right\}\right)\leftrightarrow \forall y\in {\mathbb{N}}_0\left(s<y\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)$$
17		nfv	$$⊢Ⅎxs<y$$
18	17 6	nfim	$$⊢Ⅎx\left(s<y\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)$$
19		nfv	$$⊢Ⅎy\left(s<x\to \neg \phi \right)$$
20		breq2	$$⊢y=x\to \left(s<y\leftrightarrow s<x\right)$$
21	20 8	imbi12d	$$⊢y=x\to \left(\left(s<y\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)\leftrightarrow \left(s<x\to \neg \phi \right)\right)$$
22	18 19 21	cbvralw	$$⊢\forall y\in {\mathbb{N}}_0\left(s<y\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\neg \phi \right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(s<x\to \neg \phi \right)$$
23	16 22	bitri	$$⊢\forall y\in {\mathbb{N}}_0\left(s<y\to y\notin \left\{x\in {\mathbb{N}}_0|\phi \right\}\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(s<x\to \neg \phi \right)$$
24	23	a1i	$$⊢\left(\left\{x\in {\mathbb{N}}_0|\phi \right\}\subseteq {\mathbb{N}}_0\wedge s\in {\mathbb{N}}_0\right)\to \left(\forall y\in {\mathbb{N}}_0\left(s<y\to y\notin \left\{x\in {\mathbb{N}}_0|\phi \right\}\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(s<x\to \neg \phi \right)\right)$$
25	24	rexbidva	$$⊢\left\{x\in {\mathbb{N}}_0|\phi \right\}\subseteq {\mathbb{N}}_0\to \left(\exists s\in {\mathbb{N}}_0\forall y\in {\mathbb{N}}_0\left(s<y\to y\notin \left\{x\in {\mathbb{N}}_0|\phi \right\}\right)\leftrightarrow \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to \neg \phi \right)\right)$$
26	2 25	bitrd	$$⊢\left\{x\in {\mathbb{N}}_0|\phi \right\}\subseteq {\mathbb{N}}_0\to \left(\left\{x\in {\mathbb{N}}_0|\phi \right\}\in \mathrm{Fin}\leftrightarrow \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to \neg \phi \right)\right)$$
27	1 26	ax-mp	$$⊢\left\{x\in {\mathbb{N}}_0|\phi \right\}\in \mathrm{Fin}\leftrightarrow \exists s\in {\mathbb{N}}_0\forall x\in {\mathbb{N}}_0\left(s<x\to \neg \phi \right)$$