Metamath Proof Explorer

Theorem dfnn2

Description: Alternate definition of the set of positive integers. This was our original definition, before the current df-nn replaced it. This definition requires the axiom of infinity to ensure it has the properties we expect. (Contributed by Jeff Hankins, 12-Sep-2013) (Revised by Mario Carneiro, 3-May-2014)

Ref Expression
Assertion dfnn2 ℕ = ∩ { 𝑥 ∣ ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) }

Proof

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