Theorem dfn0s2

Description: Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	dfn0s2	⊢ ℕ0s = ∩ { 𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 +s 1s ) ∈ 𝑥 ) }

Proof

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