This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( { 𝑥 ∈ ℕ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 bitrid ⊢ ( 𝑦 ∈ ℕ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 ( 𝑠 < 𝑥 → ¬ 𝜑 ) )