Step 
Hyp 
Ref 
Expression 
1 

rabid2 
⊢ ( ( ℕ_{0} ↑_{m} 1_{o} ) = { 𝑓 ∈ ( ℕ_{0} ↑_{m} 1_{o} ) ∣ ( ^{◡} 𝑓 “ ℕ ) ∈ Fin } ↔ ∀ 𝑓 ∈ ( ℕ_{0} ↑_{m} 1_{o} ) ( ^{◡} 𝑓 “ ℕ ) ∈ Fin ) 
2 

df1o2 
⊢ 1_{o} = { ∅ } 
3 

snfi 
⊢ { ∅ } ∈ Fin 
4 
2 3

eqeltri 
⊢ 1_{o} ∈ Fin 
5 

cnvimass 
⊢ ( ^{◡} 𝑓 “ ℕ ) ⊆ dom 𝑓 
6 

elmapi 
⊢ ( 𝑓 ∈ ( ℕ_{0} ↑_{m} 1_{o} ) → 𝑓 : 1_{o} ⟶ ℕ_{0} ) 
7 
5 6

fssdm 
⊢ ( 𝑓 ∈ ( ℕ_{0} ↑_{m} 1_{o} ) → ( ^{◡} 𝑓 “ ℕ ) ⊆ 1_{o} ) 
8 

ssfi 
⊢ ( ( 1_{o} ∈ Fin ∧ ( ^{◡} 𝑓 “ ℕ ) ⊆ 1_{o} ) → ( ^{◡} 𝑓 “ ℕ ) ∈ Fin ) 
9 
4 7 8

sylancr 
⊢ ( 𝑓 ∈ ( ℕ_{0} ↑_{m} 1_{o} ) → ( ^{◡} 𝑓 “ ℕ ) ∈ Fin ) 
10 
1 9

mprgbir 
⊢ ( ℕ_{0} ↑_{m} 1_{o} ) = { 𝑓 ∈ ( ℕ_{0} ↑_{m} 1_{o} ) ∣ ( ^{◡} 𝑓 “ ℕ ) ∈ Fin } 