Step 
Hyp 
Ref 
Expression 
1 

find.1 
⊢ ( 𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) 
2 
1

simp1i 
⊢ 𝐴 ⊆ ω 
3 

3simpc 
⊢ ( ( 𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) → ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) ) 
4 
1 3

axmp 
⊢ ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) 
5 

dfral 
⊢ ( ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) 
6 

alral 
⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) 
7 
5 6

sylbi 
⊢ ( ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 → ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) 
8 
7

anim2i 
⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) → ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ) 
9 
4 8

axmp 
⊢ ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) 
10 

peano5 
⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ω ⊆ 𝐴 ) 
11 
9 10

axmp 
⊢ ω ⊆ 𝐴 
12 
2 11

eqssi 
⊢ 𝐴 = ω 