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 ) ∈ 𝑥 ) }