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

Metamath Proof Explorer

Theorem dfnn3

Description: Alternate definition of the set of positive integers. Definition of positive integers in Apostol p. 22. (Contributed by NM, 3-Jul-2005)

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

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( 𝑥 = 𝑧 → ( 1 ∈ 𝑥 ↔ 1 ∈ 𝑧 ) )
2 eleq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 + 1 ) ∈ 𝑥 ↔ ( 𝑦 + 1 ) ∈ 𝑧 ) )
3 2 raleqbi1dv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝑧 ( 𝑦 + 1 ) ∈ 𝑧 ) )
4 1 3 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ↔ ( 1 ∈ 𝑧 ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑦 + 1 ) ∈ 𝑧 ) ) )
5 dfnn2 ⊢ ℕ = ∩ { 𝑧 ∣ ( 1 ∈ 𝑧 ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑦 + 1 ) ∈ 𝑧 ) }
6 5 eqeq2i ⊢ ( 𝑥 = ℕ ↔ 𝑥 = ∩ { 𝑧 ∣ ( 1 ∈ 𝑧 ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑦 + 1 ) ∈ 𝑧 ) } )
7 eleq2 ⊢ ( 𝑥 = ℕ → ( 1 ∈ 𝑥 ↔ 1 ∈ ℕ ) )
8 eleq2 ⊢ ( 𝑥 = ℕ → ( ( 𝑦 + 1 ) ∈ 𝑥 ↔ ( 𝑦 + 1 ) ∈ ℕ ) )
9 8 raleqbi1dv ⊢ ( 𝑥 = ℕ → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ ℕ ( 𝑦 + 1 ) ∈ ℕ ) )
10 7 9 anbi12d ⊢ ( 𝑥 = ℕ → ( ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ↔ ( 1 ∈ ℕ ∧ ∀ 𝑦 ∈ ℕ ( 𝑦 + 1 ) ∈ ℕ ) ) )
11 6 10 sylbir ⊢ ( 𝑥 = ∩ { 𝑧 ∣ ( 1 ∈ 𝑧 ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑦 + 1 ) ∈ 𝑧 ) } → ( ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ↔ ( 1 ∈ ℕ ∧ ∀ 𝑦 ∈ ℕ ( 𝑦 + 1 ) ∈ ℕ ) ) )
12 nnssre ⊢ ℕ ⊆ ℝ
13 5 12 eqsstrri ⊢ ∩ { 𝑧 ∣ ( 1 ∈ 𝑧 ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑦 + 1 ) ∈ 𝑧 ) } ⊆ ℝ
14 1nn ⊢ 1 ∈ ℕ
15 peano2nn ⊢ ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ )
16 15 rgen ⊢ ∀ 𝑦 ∈ ℕ ( 𝑦 + 1 ) ∈ ℕ
17 14 16 pm3.2i ⊢ ( 1 ∈ ℕ ∧ ∀ 𝑦 ∈ ℕ ( 𝑦 + 1 ) ∈ ℕ )
18 13 17 pm3.2i ⊢ ( ∩ { 𝑧 ∣ ( 1 ∈ 𝑧 ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑦 + 1 ) ∈ 𝑧 ) } ⊆ ℝ ∧ ( 1 ∈ ℕ ∧ ∀ 𝑦 ∈ ℕ ( 𝑦 + 1 ) ∈ ℕ ) )
19 4 11 18 intabs ⊢ ∩ { 𝑥 ∣ ( 𝑥 ⊆ ℝ ∧ ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ) } = ∩ { 𝑥 ∣ ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) }
20 3anass ⊢ ( ( 𝑥 ⊆ ℝ ∧ 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ↔ ( 𝑥 ⊆ ℝ ∧ ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ) )
21 20 abbii ⊢ { 𝑥 ∣ ( 𝑥 ⊆ ℝ ∧ 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ⊆ ℝ ∧ ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ) }
22 21 inteqi ⊢ ∩ { 𝑥 ∣ ( 𝑥 ⊆ ℝ ∧ 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) } = ∩ { 𝑥 ∣ ( 𝑥 ⊆ ℝ ∧ ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) ) }
23 dfnn2 ⊢ ℕ = ∩ { 𝑥 ∣ ( 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) }
24 19 22 23 3eqtr4ri ⊢ ℕ = ∩ { 𝑥 ∣ ( 𝑥 ⊆ ℝ ∧ 1 ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 + 1 ) ∈ 𝑥 ) }