Theorem peano5n0s 27935

Description: Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)

Assertion

Ref	Expression
peano5n0s	⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ℕ0s ⊆ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem peano5n0s

Dummy variables 𝑛 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-n0s 27931	. . 3 ⊢ ℕ0s = (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) “ ω)
2		df-ima 5688	. . 3 ⊢ (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) “ ω) = ran (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)
3	1, 2	eqtri 2758	. 2 ⊢ ℕ0s = ran (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)
4		frfnom 8437	. . . . 5 ⊢ (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω) Fn ω
5	4	a1i 11	. . . 4 ⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω) Fn ω)
6		fveq2 6890	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) = ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘∅))
7	6	eleq1d 2816	. . . . . . 7 ⊢ (𝑦 = ∅ → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) ∈ 𝐴 ↔ ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘∅) ∈ 𝐴))
8		fveq2 6890	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) = ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧))
9	8	eleq1d 2816	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) ∈ 𝐴 ↔ ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) ∈ 𝐴))
10		fveq2 6890	. . . . . . . 8 ⊢ (𝑦 = suc 𝑧 → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) = ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘suc 𝑧))
11	10	eleq1d 2816	. . . . . . 7 ⊢ (𝑦 = suc 𝑧 → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) ∈ 𝐴 ↔ ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘suc 𝑧) ∈ 𝐴))
12		fr0g 8438	. . . . . . . . 9 ⊢ ( 0s ∈ 𝐴 → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘∅) = 0s )
13		id 22	. . . . . . . . 9 ⊢ ( 0s ∈ 𝐴 → 0s ∈ 𝐴)
14	12, 13	eqeltrd 2831	. . . . . . . 8 ⊢ ( 0s ∈ 𝐴 → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘∅) ∈ 𝐴)
15	14	adantr 479	. . . . . . 7 ⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘∅) ∈ 𝐴)
16		oveq1 7418	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) → (𝑥 +s 1s ) = (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ))
17	16	eleq1d 2816	. . . . . . . . . . . 12 ⊢ (𝑥 = ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) → ((𝑥 +s 1s ) ∈ 𝐴 ↔ (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ) ∈ 𝐴))
18	17	rspccv 3608	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴 → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) ∈ 𝐴 → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ) ∈ 𝐴))
19	18	adantl 480	. . . . . . . . . 10 ⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) ∈ 𝐴 → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ) ∈ 𝐴))
20	19	imp 405	. . . . . . . . 9 ⊢ ((( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) ∧ ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) ∈ 𝐴) → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ) ∈ 𝐴)
21		ovex 7444	. . . . . . . . . . 11 ⊢ (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ) ∈ V
22		eqid 2730	. . . . . . . . . . . 12 ⊢ (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω) = (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)
23		oveq1 7418	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑛 → (𝑦 +s 1s ) = (𝑛 +s 1s ))
24		oveq1 7418	. . . . . . . . . . . 12 ⊢ (𝑦 = ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) → (𝑦 +s 1s ) = (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ))
25	22, 23, 24	frsucmpt2 8442	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ω ∧ (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ) ∈ V) → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘suc 𝑧) = (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ))
26	21, 25	mpan2 687	. . . . . . . . . 10 ⊢ (𝑧 ∈ ω → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘suc 𝑧) = (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ))
27	26	eleq1d 2816	. . . . . . . . 9 ⊢ (𝑧 ∈ ω → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘suc 𝑧) ∈ 𝐴 ↔ (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) +s 1s ) ∈ 𝐴))
28	20, 27	imbitrrid 245	. . . . . . . 8 ⊢ (𝑧 ∈ ω → ((( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) ∧ ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) ∈ 𝐴) → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘suc 𝑧) ∈ 𝐴))
29	28	expd 414	. . . . . . 7 ⊢ (𝑧 ∈ ω → (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → (((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑧) ∈ 𝐴 → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘suc 𝑧) ∈ 𝐴)))
30	7, 9, 11, 15, 29	finds2 7893	. . . . . 6 ⊢ (𝑦 ∈ ω → (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) ∈ 𝐴))
31	30	com12 32	. . . . 5 ⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → (𝑦 ∈ ω → ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) ∈ 𝐴))
32	31	ralrimiv 3143	. . . 4 ⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ∀𝑦 ∈ ω ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) ∈ 𝐴)
33		ffnfv 7119	. . . 4 ⊢ ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω):ω⟶𝐴 ↔ ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω) Fn ω ∧ ∀𝑦 ∈ ω ((rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω)‘𝑦) ∈ 𝐴))
34	5, 32, 33	sylanbrc 581	. . 3 ⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω):ω⟶𝐴)
35	34	frnd 6724	. 2 ⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ran (rec((𝑛 ∈ V ↦ (𝑛 +s 1s )), 0s ) ↾ ω) ⊆ 𝐴)
36	3, 35	eqsstrid 4029	1 ⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ℕ0s ⊆ 𝐴)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  ∀wral 3059  Vcvv 3472   ⊆ wss 3947  ∅c0 4321   ↦ cmpt 5230  ran crn 5676   ↾ cres 5677   “ cima 5678  suc csuc 6365   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542  (class class class)co 7411  ωcom 7857  reccrdg 8411   0_s c0s 27560   1_s c1s 27561   +_s cadds 27681  ℕ_0scnn0s 27929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-n0s 27931

This theorem is referenced by:  n0ssno  27936  dfn0s2  27941  n0sind  27942