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	⊢ ( { 𝑥 ∈ ℕ0 ∣ 𝜑 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		ssrab2	⊢ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ⊆ ℕ0
2		ssnn0fi	⊢ ( { 𝑥 ∈ ℕ0 ∣ 𝜑 } ⊆ ℕ0 → ( { 𝑥 ∈ ℕ0 ∣ 𝜑 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑠 < 𝑦 → 𝑦 ∉ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ) ) )
3		nnel	⊢ ( ¬ 𝑦 ∉ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∈ ℕ0 ∣ 𝜑 } )
4		nfcv	⊢ Ⅎ 𝑥 𝑦
5		nfcv	⊢ Ⅎ 𝑥 ℕ0
6		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] ¬ 𝜑
7	6	nfn	⊢ Ⅎ 𝑥 ¬ [ 𝑦 / 𝑥 ] ¬ 𝜑
8		sbceq2a	⊢ ( 𝑦 = 𝑥 → ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ 𝜑 ) )
9	8	equcoms	⊢ ( 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ 𝜑 ) )
10	9	con2bid	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ ¬ [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
11	4 5 7 10	elrabf	⊢ ( 𝑦 ∈ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ↔ ( 𝑦 ∈ ℕ0 ∧ ¬ [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
12	11	baib	⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 ∈ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ↔ ¬ [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
13	3 12	syl5bb	⊢ ( 𝑦 ∈ ℕ0 → ( ¬ 𝑦 ∉ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ↔ ¬ [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
14	13	con4bid	⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 ∉ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
15	14	imbi2d	⊢ ( 𝑦 ∈ ℕ0 → ( ( 𝑠 < 𝑦 → 𝑦 ∉ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ) ↔ ( 𝑠 < 𝑦 → [ 𝑦 / 𝑥 ] ¬ 𝜑 ) ) )
16	15	ralbiia	⊢ ( ∀ 𝑦 ∈ ℕ0 ( 𝑠 < 𝑦 → 𝑦 ∉ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ) ↔ ∀ 𝑦 ∈ ℕ0 ( 𝑠 < 𝑦 → [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
17		nfv	⊢ Ⅎ 𝑥 𝑠 < 𝑦
18	17 6	nfim	⊢ Ⅎ 𝑥 ( 𝑠 < 𝑦 → [ 𝑦 / 𝑥 ] ¬ 𝜑 )
19		nfv	⊢ Ⅎ 𝑦 ( 𝑠 < 𝑥 → ¬ 𝜑 )
20		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝑠 < 𝑦 ↔ 𝑠 < 𝑥 ) )
21	20 8	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑠 < 𝑦 → [ 𝑦 / 𝑥 ] ¬ 𝜑 ) ↔ ( 𝑠 < 𝑥 → ¬ 𝜑 ) ) )
22	18 19 21	cbvralw	⊢ ( ∀ 𝑦 ∈ ℕ0 ( 𝑠 < 𝑦 → [ 𝑦 / 𝑥 ] ¬ 𝜑 ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ 𝜑 ) )
23	16 22	bitri	⊢ ( ∀ 𝑦 ∈ ℕ0 ( 𝑠 < 𝑦 → 𝑦 ∉ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ 𝜑 ) )
24	23	a1i	⊢ ( ( { 𝑥 ∈ ℕ0 ∣ 𝜑 } ⊆ ℕ0 ∧ 𝑠 ∈ ℕ0 ) → ( ∀ 𝑦 ∈ ℕ0 ( 𝑠 < 𝑦 → 𝑦 ∉ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ) ↔ ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ 𝜑 ) ) )
25	24	rexbidva	⊢ ( { 𝑥 ∈ ℕ0 ∣ 𝜑 } ⊆ ℕ0 → ( ∃ 𝑠 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑠 < 𝑦 → 𝑦 ∉ { 𝑥 ∈ ℕ0 ∣ 𝜑 } ) ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ 𝜑 ) ) )
26	2 25	bitrd	⊢ ( { 𝑥 ∈ ℕ0 ∣ 𝜑 } ⊆ ℕ0 → ( { 𝑥 ∈ ℕ0 ∣ 𝜑 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ 𝜑 ) ) )
27	1 26	ax-mp	⊢ ( { 𝑥 ∈ ℕ0 ∣ 𝜑 } ∈ Fin ↔ ∃ 𝑠 ∈ ℕ0 ∀ 𝑥 ∈ ℕ0 ( 𝑠 < 𝑥 → ¬ 𝜑 ) )