Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  peano4nninf GIF version

Theorem peano4nninf 13418
 Description: The successor function on ℕ∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.)
Hypothesis
Ref Expression
peano4nninf.s 𝑆 = (𝑝 ∈ ℕ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))))
Assertion
Ref Expression
peano4nninf 𝑆:ℕ1-1→ℕ
Distinct variable groups:   𝑆,𝑖   𝑖,𝑝
Allowed substitution hint:   𝑆(𝑝)

Proof of Theorem peano4nninf
Dummy variables 𝑘 𝑥 𝑦 𝑓 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano4nninf.s . . 3 𝑆 = (𝑝 ∈ ℕ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))))
21nnsf 13417 . 2 𝑆:ℕ⟶ℕ
3 fveq1 5431 . . . . . . . . . . 11 (𝑓 = 𝑥 → (𝑓‘suc 𝑗) = (𝑥‘suc 𝑗))
4 fveq1 5431 . . . . . . . . . . 11 (𝑓 = 𝑥 → (𝑓𝑗) = (𝑥𝑗))
53, 4sseq12d 3134 . . . . . . . . . 10 (𝑓 = 𝑥 → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ (𝑥‘suc 𝑗) ⊆ (𝑥𝑗)))
65ralbidv 2439 . . . . . . . . 9 (𝑓 = 𝑥 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω (𝑥‘suc 𝑗) ⊆ (𝑥𝑗)))
7 df-nninf 7021 . . . . . . . . 9 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗)}
86, 7elrab2 2848 . . . . . . . 8 (𝑥 ∈ ℕ ↔ (𝑥 ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑥‘suc 𝑗) ⊆ (𝑥𝑗)))
98simplbi 272 . . . . . . 7 (𝑥 ∈ ℕ𝑥 ∈ (2o𝑚 ω))
10 elmapfn 6576 . . . . . . 7 (𝑥 ∈ (2o𝑚 ω) → 𝑥 Fn ω)
119, 10syl 14 . . . . . 6 (𝑥 ∈ ℕ𝑥 Fn ω)
1211ad2antrr 480 . . . . 5 (((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) → 𝑥 Fn ω)
13 fveq1 5431 . . . . . . . . . . 11 (𝑓 = 𝑦 → (𝑓‘suc 𝑗) = (𝑦‘suc 𝑗))
14 fveq1 5431 . . . . . . . . . . 11 (𝑓 = 𝑦 → (𝑓𝑗) = (𝑦𝑗))
1513, 14sseq12d 3134 . . . . . . . . . 10 (𝑓 = 𝑦 → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ (𝑦‘suc 𝑗) ⊆ (𝑦𝑗)))
1615ralbidv 2439 . . . . . . . . 9 (𝑓 = 𝑦 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω (𝑦‘suc 𝑗) ⊆ (𝑦𝑗)))
1716, 7elrab2 2848 . . . . . . . 8 (𝑦 ∈ ℕ ↔ (𝑦 ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑦‘suc 𝑗) ⊆ (𝑦𝑗)))
1817simplbi 272 . . . . . . 7 (𝑦 ∈ ℕ𝑦 ∈ (2o𝑚 ω))
19 elmapfn 6576 . . . . . . 7 (𝑦 ∈ (2o𝑚 ω) → 𝑦 Fn ω)
2018, 19syl 14 . . . . . 6 (𝑦 ∈ ℕ𝑦 Fn ω)
2120ad2antlr 481 . . . . 5 (((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) → 𝑦 Fn ω)
22 simplr 520 . . . . . . 7 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → (𝑆𝑥) = (𝑆𝑦))
2322fveq1d 5434 . . . . . 6 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆𝑥)‘suc 𝑘) = ((𝑆𝑦)‘suc 𝑘))
24 fveq1 5431 . . . . . . . . . . . 12 (𝑝 = 𝑥 → (𝑝 𝑖) = (𝑥 𝑖))
2524ifeq2d 3496 . . . . . . . . . . 11 (𝑝 = 𝑥 → if(𝑖 = ∅, 1o, (𝑝 𝑖)) = if(𝑖 = ∅, 1o, (𝑥 𝑖)))
2625mpteq2dv 4028 . . . . . . . . . 10 (𝑝 = 𝑥 → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑥 𝑖))))
27 omex 4517 . . . . . . . . . . 11 ω ∈ V
2827mptex 5657 . . . . . . . . . 10 (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑥 𝑖))) ∈ V
2926, 1, 28fvmpt 5509 . . . . . . . . 9 (𝑥 ∈ ℕ → (𝑆𝑥) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑥 𝑖))))
3029ad3antrrr 484 . . . . . . . 8 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → (𝑆𝑥) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑥 𝑖))))
31 simpr 109 . . . . . . . . . 10 (((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → 𝑖 = suc 𝑘)
3231eqeq1d 2149 . . . . . . . . 9 (((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → (𝑖 = ∅ ↔ suc 𝑘 = ∅))
3331unieqd 3756 . . . . . . . . . 10 (((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → 𝑖 = suc 𝑘)
3433fveq2d 5436 . . . . . . . . 9 (((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → (𝑥 𝑖) = (𝑥 suc 𝑘))
3532, 34ifbieq2d 3502 . . . . . . . 8 (((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → if(𝑖 = ∅, 1o, (𝑥 𝑖)) = if(suc 𝑘 = ∅, 1o, (𝑥 suc 𝑘)))
36 peano2 4519 . . . . . . . . 9 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
3736adantl 275 . . . . . . . 8 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ ω)
38 1lt2o 6350 . . . . . . . . . 10 1o ∈ 2o
3938a1i 9 . . . . . . . . 9 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → 1o ∈ 2o)
40 nninff 13416 . . . . . . . . . . 11 (𝑥 ∈ ℕ𝑥:ω⟶2o)
4140ad3antrrr 484 . . . . . . . . . 10 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → 𝑥:ω⟶2o)
42 nnpredcl 4547 . . . . . . . . . . 11 (suc 𝑘 ∈ ω → suc 𝑘 ∈ ω)
4337, 42syl 14 . . . . . . . . . 10 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → suc 𝑘 ∈ ω)
4441, 43ffvelrnd 5567 . . . . . . . . 9 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → (𝑥 suc 𝑘) ∈ 2o)
45 nndceq0 4542 . . . . . . . . . 10 (suc 𝑘 ∈ ω → DECID suc 𝑘 = ∅)
4637, 45syl 14 . . . . . . . . 9 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → DECID suc 𝑘 = ∅)
4739, 44, 46ifcldcd 3513 . . . . . . . 8 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1o, (𝑥 suc 𝑘)) ∈ 2o)
4830, 35, 37, 47fvmptd 5513 . . . . . . 7 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆𝑥)‘suc 𝑘) = if(suc 𝑘 = ∅, 1o, (𝑥 suc 𝑘)))
49 peano3 4520 . . . . . . . . . 10 (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
5049adantl 275 . . . . . . . . 9 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → suc 𝑘 ≠ ∅)
5150neneqd 2330 . . . . . . . 8 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → ¬ suc 𝑘 = ∅)
5251iffalsed 3490 . . . . . . 7 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1o, (𝑥 suc 𝑘)) = (𝑥 suc 𝑘))
53 nnord 4536 . . . . . . . . . . 11 (𝑘 ∈ ω → Ord 𝑘)
54 ordtr 4310 . . . . . . . . . . 11 (Ord 𝑘 → Tr 𝑘)
5553, 54syl 14 . . . . . . . . . 10 (𝑘 ∈ ω → Tr 𝑘)
56 unisucg 4346 . . . . . . . . . 10 (𝑘 ∈ ω → (Tr 𝑘 suc 𝑘 = 𝑘))
5755, 56mpbid 146 . . . . . . . . 9 (𝑘 ∈ ω → suc 𝑘 = 𝑘)
5857fveq2d 5436 . . . . . . . 8 (𝑘 ∈ ω → (𝑥 suc 𝑘) = (𝑥𝑘))
5958adantl 275 . . . . . . 7 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → (𝑥 suc 𝑘) = (𝑥𝑘))
6048, 52, 593eqtrd 2177 . . . . . 6 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆𝑥)‘suc 𝑘) = (𝑥𝑘))
61 fveq1 5431 . . . . . . . . . . . 12 (𝑝 = 𝑦 → (𝑝 𝑖) = (𝑦 𝑖))
6261ifeq2d 3496 . . . . . . . . . . 11 (𝑝 = 𝑦 → if(𝑖 = ∅, 1o, (𝑝 𝑖)) = if(𝑖 = ∅, 1o, (𝑦 𝑖)))
6362mpteq2dv 4028 . . . . . . . . . 10 (𝑝 = 𝑦 → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑦 𝑖))))
6427mptex 5657 . . . . . . . . . 10 (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑦 𝑖))) ∈ V
6563, 1, 64fvmpt 5509 . . . . . . . . 9 (𝑦 ∈ ℕ → (𝑆𝑦) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑦 𝑖))))
6665ad3antlr 485 . . . . . . . 8 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → (𝑆𝑦) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑦 𝑖))))
6733fveq2d 5436 . . . . . . . . 9 (((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → (𝑦 𝑖) = (𝑦 suc 𝑘))
6832, 67ifbieq2d 3502 . . . . . . . 8 (((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) ∧ 𝑖 = suc 𝑘) → if(𝑖 = ∅, 1o, (𝑦 𝑖)) = if(suc 𝑘 = ∅, 1o, (𝑦 suc 𝑘)))
69 nninff 13416 . . . . . . . . . . 11 (𝑦 ∈ ℕ𝑦:ω⟶2o)
7069ad3antlr 485 . . . . . . . . . 10 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → 𝑦:ω⟶2o)
7170, 43ffvelrnd 5567 . . . . . . . . 9 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → (𝑦 suc 𝑘) ∈ 2o)
7239, 71, 46ifcldcd 3513 . . . . . . . 8 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1o, (𝑦 suc 𝑘)) ∈ 2o)
7366, 68, 37, 72fvmptd 5513 . . . . . . 7 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆𝑦)‘suc 𝑘) = if(suc 𝑘 = ∅, 1o, (𝑦 suc 𝑘)))
7451iffalsed 3490 . . . . . . 7 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → if(suc 𝑘 = ∅, 1o, (𝑦 suc 𝑘)) = (𝑦 suc 𝑘))
7557fveq2d 5436 . . . . . . . 8 (𝑘 ∈ ω → (𝑦 suc 𝑘) = (𝑦𝑘))
7675adantl 275 . . . . . . 7 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → (𝑦 suc 𝑘) = (𝑦𝑘))
7773, 74, 763eqtrd 2177 . . . . . 6 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → ((𝑆𝑦)‘suc 𝑘) = (𝑦𝑘))
7823, 60, 773eqtr3d 2181 . . . . 5 ((((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) ∧ 𝑘 ∈ ω) → (𝑥𝑘) = (𝑦𝑘))
7912, 21, 78eqfnfvd 5532 . . . 4 (((𝑥 ∈ ℕ𝑦 ∈ ℕ) ∧ (𝑆𝑥) = (𝑆𝑦)) → 𝑥 = 𝑦)
8079ex 114 . . 3 ((𝑥 ∈ ℕ𝑦 ∈ ℕ) → ((𝑆𝑥) = (𝑆𝑦) → 𝑥 = 𝑦))
8180rgen2a 2490 . 2 𝑥 ∈ ℕ𝑦 ∈ ℕ ((𝑆𝑥) = (𝑆𝑦) → 𝑥 = 𝑦)
82 dff13 5680 . 2 (𝑆:ℕ1-1→ℕ ↔ (𝑆:ℕ⟶ℕ ∧ ∀𝑥 ∈ ℕ𝑦 ∈ ℕ ((𝑆𝑥) = (𝑆𝑦) → 𝑥 = 𝑦)))
832, 81, 82mpbir2an 927 1 𝑆:ℕ1-1→ℕ
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103  DECID wdc 820   = wceq 1332   ∈ wcel 1481   ≠ wne 2309  ∀wral 2417   ⊆ wss 3077  ∅c0 3369  ifcif 3480  ∪ cuni 3745   ↦ cmpt 3998  Tr wtr 4035  Ord word 4294  suc csuc 4297  ωcom 4514   Fn wfn 5129  ⟶wf 5130  –1-1→wf1 5131  ‘cfv 5134  (class class class)co 5785  1oc1o 6317  2oc2o 6318   ↑𝑚 cmap 6553  ℕ∞xnninf 7020 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4141  ax-un 4365  ax-setind 4462  ax-iinf 4512 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-if 3481  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4225  df-iord 4298  df-on 4300  df-suc 4303  df-iom 4515  df-xp 4556  df-rel 4557  df-cnv 4558  df-co 4559  df-dm 4560  df-rn 4561  df-res 4562  df-ima 4563  df-iota 5099  df-fun 5136  df-fn 5137  df-f 5138  df-f1 5139  df-fo 5140  df-f1o 5141  df-fv 5142  df-ov 5788  df-oprab 5789  df-mpo 5790  df-1o 6324  df-2o 6325  df-map 6555  df-nninf 7021 This theorem is referenced by:  exmidsbthrlem  13435
 Copyright terms: Public domain W3C validator