| Step | Hyp | Ref | Expression | 
						
							| 1 |  | 0sno | ⊢  0s   ∈   No | 
						
							| 2 | 1 | elexi | ⊢  0s   ∈  V | 
						
							| 3 | 2 | elintab | ⊢ (  0s   ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) }  ↔  ∀ 𝑥 ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  →   0s   ∈  𝑥 ) ) | 
						
							| 4 |  | simpl | ⊢ ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  →   0s   ∈  𝑥 ) | 
						
							| 5 | 3 4 | mpgbir | ⊢  0s   ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } | 
						
							| 6 |  | oveq1 | ⊢ ( 𝑦  =  𝑧  →  ( 𝑦  +s   1s  )  =  ( 𝑧  +s   1s  ) ) | 
						
							| 7 | 6 | eleq1d | ⊢ ( 𝑦  =  𝑧  →  ( ( 𝑦  +s   1s  )  ∈  𝑥  ↔  ( 𝑧  +s   1s  )  ∈  𝑥 ) ) | 
						
							| 8 | 7 | rspccv | ⊢ ( ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥  →  ( 𝑧  ∈  𝑥  →  ( 𝑧  +s   1s  )  ∈  𝑥 ) ) | 
						
							| 9 | 8 | adantl | ⊢ ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  →  ( 𝑧  ∈  𝑥  →  ( 𝑧  +s   1s  )  ∈  𝑥 ) ) | 
						
							| 10 | 9 | a2i | ⊢ ( ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  →  𝑧  ∈  𝑥 )  →  ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  →  ( 𝑧  +s   1s  )  ∈  𝑥 ) ) | 
						
							| 11 | 10 | alimi | ⊢ ( ∀ 𝑥 ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  →  𝑧  ∈  𝑥 )  →  ∀ 𝑥 ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  →  ( 𝑧  +s   1s  )  ∈  𝑥 ) ) | 
						
							| 12 |  | vex | ⊢ 𝑧  ∈  V | 
						
							| 13 | 12 | elintab | ⊢ ( 𝑧  ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) }  ↔  ∀ 𝑥 ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  →  𝑧  ∈  𝑥 ) ) | 
						
							| 14 |  | ovex | ⊢ ( 𝑧  +s   1s  )  ∈  V | 
						
							| 15 | 14 | elintab | ⊢ ( ( 𝑧  +s   1s  )  ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) }  ↔  ∀ 𝑥 ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  →  ( 𝑧  +s   1s  )  ∈  𝑥 ) ) | 
						
							| 16 | 11 13 15 | 3imtr4i | ⊢ ( 𝑧  ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) }  →  ( 𝑧  +s   1s  )  ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } ) | 
						
							| 17 | 16 | rgen | ⊢ ∀ 𝑧  ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } ( 𝑧  +s   1s  )  ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } | 
						
							| 18 |  | peano5n0s | ⊢ ( (  0s   ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) }  ∧  ∀ 𝑧  ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } ( 𝑧  +s   1s  )  ∈  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } )  →  ℕ0s  ⊆  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } ) | 
						
							| 19 | 5 17 18 | mp2an | ⊢ ℕ0s  ⊆  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } | 
						
							| 20 |  | 0n0s | ⊢  0s   ∈  ℕ0s | 
						
							| 21 |  | peano2n0s | ⊢ ( 𝑦  ∈  ℕ0s  →  ( 𝑦  +s   1s  )  ∈  ℕ0s ) | 
						
							| 22 | 21 | rgen | ⊢ ∀ 𝑦  ∈  ℕ0s ( 𝑦  +s   1s  )  ∈  ℕ0s | 
						
							| 23 |  | n0sex | ⊢ ℕ0s  ∈  V | 
						
							| 24 |  | eleq2 | ⊢ ( 𝑥  =  ℕ0s  →  (  0s   ∈  𝑥  ↔   0s   ∈  ℕ0s ) ) | 
						
							| 25 |  | eleq2 | ⊢ ( 𝑥  =  ℕ0s  →  ( ( 𝑦  +s   1s  )  ∈  𝑥  ↔  ( 𝑦  +s   1s  )  ∈  ℕ0s ) ) | 
						
							| 26 | 25 | raleqbi1dv | ⊢ ( 𝑥  =  ℕ0s  →  ( ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥  ↔  ∀ 𝑦  ∈  ℕ0s ( 𝑦  +s   1s  )  ∈  ℕ0s ) ) | 
						
							| 27 | 24 26 | anbi12d | ⊢ ( 𝑥  =  ℕ0s  →  ( (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 )  ↔  (  0s   ∈  ℕ0s  ∧  ∀ 𝑦  ∈  ℕ0s ( 𝑦  +s   1s  )  ∈  ℕ0s ) ) ) | 
						
							| 28 | 23 27 | elab | ⊢ ( ℕ0s  ∈  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) }  ↔  (  0s   ∈  ℕ0s  ∧  ∀ 𝑦  ∈  ℕ0s ( 𝑦  +s   1s  )  ∈  ℕ0s ) ) | 
						
							| 29 | 20 22 28 | mpbir2an | ⊢ ℕ0s  ∈  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } | 
						
							| 30 |  | intss1 | ⊢ ( ℕ0s  ∈  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) }  →  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) }  ⊆  ℕ0s ) | 
						
							| 31 | 29 30 | ax-mp | ⊢ ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) }  ⊆  ℕ0s | 
						
							| 32 | 19 31 | eqssi | ⊢ ℕ0s  =  ∩  { 𝑥  ∣  (  0s   ∈  𝑥  ∧  ∀ 𝑦  ∈  𝑥 ( 𝑦  +s   1s  )  ∈  𝑥 ) } |