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

Theorem nnsf 12783
 Description: Domain and range of 𝑆. Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.)
Hypothesis
Ref Expression
nns.s 𝑆 = (𝑝 ∈ ℕ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))))
Assertion
Ref Expression
nnsf 𝑆:ℕ⟶ℕ
Distinct variable group:   𝑖,𝑝
Allowed substitution hints:   𝑆(𝑖,𝑝)

Proof of Theorem nnsf
Dummy variables 𝑓 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nns.s . 2 𝑆 = (𝑝 ∈ ℕ ↦ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))))
2 1lt2o 6269 . . . . . . 7 1o ∈ 2o
32a1i 9 . . . . . 6 ((𝑝 ∈ ℕ𝑖 ∈ ω) → 1o ∈ 2o)
4 nninff 12782 . . . . . . . 8 (𝑝 ∈ ℕ𝑝:ω⟶2o)
54adantr 272 . . . . . . 7 ((𝑝 ∈ ℕ𝑖 ∈ ω) → 𝑝:ω⟶2o)
6 nnpredcl 4474 . . . . . . . 8 (𝑖 ∈ ω → 𝑖 ∈ ω)
76adantl 273 . . . . . . 7 ((𝑝 ∈ ℕ𝑖 ∈ ω) → 𝑖 ∈ ω)
85, 7ffvelrnd 5488 . . . . . 6 ((𝑝 ∈ ℕ𝑖 ∈ ω) → (𝑝 𝑖) ∈ 2o)
9 nndceq0 4469 . . . . . . 7 (𝑖 ∈ ω → DECID 𝑖 = ∅)
109adantl 273 . . . . . 6 ((𝑝 ∈ ℕ𝑖 ∈ ω) → DECID 𝑖 = ∅)
113, 8, 10ifcldcd 3454 . . . . 5 ((𝑝 ∈ ℕ𝑖 ∈ ω) → if(𝑖 = ∅, 1o, (𝑝 𝑖)) ∈ 2o)
12 eqid 2100 . . . . 5 (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))
1311, 12fmptd 5506 . . . 4 (𝑝 ∈ ℕ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))):ω⟶2o)
14 2onn 6347 . . . . 5 2o ∈ ω
15 omex 4445 . . . . 5 ω ∈ V
16 elmapg 6485 . . . . 5 ((2o ∈ ω ∧ ω ∈ V) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) ∈ (2o𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))):ω⟶2o))
1714, 15, 16mp2an 420 . . . 4 ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) ∈ (2o𝑚 ω) ↔ (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))):ω⟶2o)
1813, 17sylibr 133 . . 3 (𝑝 ∈ ℕ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) ∈ (2o𝑚 ω))
19 1on 6250 . . . . . . . . 9 1o ∈ On
2019ontrci 4287 . . . . . . . 8 Tr 1o
212a1i 9 . . . . . . . . . . 11 ((𝑝 ∈ ℕ𝑗 ∈ ω) → 1o ∈ 2o)
224adantr 272 . . . . . . . . . . . 12 ((𝑝 ∈ ℕ𝑗 ∈ ω) → 𝑝:ω⟶2o)
23 peano2 4447 . . . . . . . . . . . . . 14 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
2423adantl 273 . . . . . . . . . . . . 13 ((𝑝 ∈ ℕ𝑗 ∈ ω) → suc 𝑗 ∈ ω)
25 nnpredcl 4474 . . . . . . . . . . . . 13 (suc 𝑗 ∈ ω → suc 𝑗 ∈ ω)
2624, 25syl 14 . . . . . . . . . . . 12 ((𝑝 ∈ ℕ𝑗 ∈ ω) → suc 𝑗 ∈ ω)
2722, 26ffvelrnd 5488 . . . . . . . . . . 11 ((𝑝 ∈ ℕ𝑗 ∈ ω) → (𝑝 suc 𝑗) ∈ 2o)
28 nndceq0 4469 . . . . . . . . . . . 12 (suc 𝑗 ∈ ω → DECID suc 𝑗 = ∅)
2924, 28syl 14 . . . . . . . . . . 11 ((𝑝 ∈ ℕ𝑗 ∈ ω) → DECID suc 𝑗 = ∅)
3021, 27, 29ifcldcd 3454 . . . . . . . . . 10 ((𝑝 ∈ ℕ𝑗 ∈ ω) → if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ∈ 2o)
3130adantr 272 . . . . . . . . 9 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ∈ 2o)
32 df-2o 6244 . . . . . . . . 9 2o = suc 1o
3331, 32syl6eleq 2192 . . . . . . . 8 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ∈ suc 1o)
34 trsucss 4283 . . . . . . . 8 (Tr 1o → (if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ∈ suc 1o → if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ⊆ 1o))
3520, 33, 34mpsyl 65 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ⊆ 1o)
36 iftrue 3426 . . . . . . . 8 (𝑗 = ∅ → if(𝑗 = ∅, 1o, (𝑝 𝑗)) = 1o)
3736adantl 273 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(𝑗 = ∅, 1o, (𝑝 𝑗)) = 1o)
3835, 37sseqtr4d 3086 . . . . . 6 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ⊆ if(𝑗 = ∅, 1o, (𝑝 𝑗)))
39 simpr 109 . . . . . . . . . . . 12 ((𝑝 ∈ ℕ𝑗 ∈ ω) → 𝑗 ∈ ω)
4039adantr 272 . . . . . . . . . . 11 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ∈ ω)
41 nnord 4463 . . . . . . . . . . 11 (𝑗 ∈ ω → Ord 𝑗)
42 ordtr 4238 . . . . . . . . . . 11 (Ord 𝑗 → Tr 𝑗)
4340, 41, 423syl 17 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → Tr 𝑗)
44 unisucg 4274 . . . . . . . . . . 11 (𝑗 ∈ ω → (Tr 𝑗 suc 𝑗 = 𝑗))
4540, 44syl 14 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (Tr 𝑗 suc 𝑗 = 𝑗))
4643, 45mpbid 146 . . . . . . . . 9 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → suc 𝑗 = 𝑗)
4746fveq2d 5357 . . . . . . . 8 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝 suc 𝑗) = (𝑝𝑗))
48 simpr 109 . . . . . . . . . . . 12 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ¬ 𝑗 = ∅)
4948neqned 2274 . . . . . . . . . . 11 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ≠ ∅)
50 nnsucpred 4468 . . . . . . . . . . 11 ((𝑗 ∈ ω ∧ 𝑗 ≠ ∅) → suc 𝑗 = 𝑗)
5140, 49, 50syl2anc 406 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → suc 𝑗 = 𝑗)
5251fveq2d 5357 . . . . . . . . 9 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘suc 𝑗) = (𝑝𝑗))
53 suceq 4262 . . . . . . . . . . . 12 (𝑘 = 𝑗 → suc 𝑘 = suc 𝑗)
5453fveq2d 5357 . . . . . . . . . . 11 (𝑘 = 𝑗 → (𝑝‘suc 𝑘) = (𝑝‘suc 𝑗))
55 fveq2 5353 . . . . . . . . . . 11 (𝑘 = 𝑗 → (𝑝𝑘) = (𝑝 𝑗))
5654, 55sseq12d 3078 . . . . . . . . . 10 (𝑘 = 𝑗 → ((𝑝‘suc 𝑘) ⊆ (𝑝𝑘) ↔ (𝑝‘suc 𝑗) ⊆ (𝑝 𝑗)))
57 fveq1 5352 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑝 → (𝑓‘suc 𝑗) = (𝑝‘suc 𝑗))
58 fveq1 5352 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑝 → (𝑓𝑗) = (𝑝𝑗))
5957, 58sseq12d 3078 . . . . . . . . . . . . . . 15 (𝑓 = 𝑝 → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ (𝑝‘suc 𝑗) ⊆ (𝑝𝑗)))
6059ralbidv 2396 . . . . . . . . . . . . . 14 (𝑓 = 𝑝 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝𝑗)))
61 df-nninf 6919 . . . . . . . . . . . . . 14 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗)}
6260, 61elrab2 2796 . . . . . . . . . . . . 13 (𝑝 ∈ ℕ ↔ (𝑝 ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝𝑗)))
6362simprbi 271 . . . . . . . . . . . 12 (𝑝 ∈ ℕ → ∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝𝑗))
64 suceq 4262 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → suc 𝑗 = suc 𝑘)
6564fveq2d 5357 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → (𝑝‘suc 𝑗) = (𝑝‘suc 𝑘))
66 fveq2 5353 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → (𝑝𝑗) = (𝑝𝑘))
6765, 66sseq12d 3078 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → ((𝑝‘suc 𝑗) ⊆ (𝑝𝑗) ↔ (𝑝‘suc 𝑘) ⊆ (𝑝𝑘)))
6867cbvralv 2612 . . . . . . . . . . . 12 (∀𝑗 ∈ ω (𝑝‘suc 𝑗) ⊆ (𝑝𝑗) ↔ ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝𝑘))
6963, 68sylib 121 . . . . . . . . . . 11 (𝑝 ∈ ℕ → ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝𝑘))
7069ad2antrr 475 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ∀𝑘 ∈ ω (𝑝‘suc 𝑘) ⊆ (𝑝𝑘))
71 nnpredcl 4474 . . . . . . . . . . . 12 (𝑗 ∈ ω → 𝑗 ∈ ω)
7271adantl 273 . . . . . . . . . . 11 ((𝑝 ∈ ℕ𝑗 ∈ ω) → 𝑗 ∈ ω)
7372adantr 272 . . . . . . . . . 10 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → 𝑗 ∈ ω)
7456, 70, 73rspcdva 2749 . . . . . . . . 9 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝‘suc 𝑗) ⊆ (𝑝 𝑗))
7552, 74eqsstr3d 3084 . . . . . . . 8 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝𝑗) ⊆ (𝑝 𝑗))
7647, 75eqsstrd 3083 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → (𝑝 suc 𝑗) ⊆ (𝑝 𝑗))
77 peano3 4448 . . . . . . . . . 10 (𝑗 ∈ ω → suc 𝑗 ≠ ∅)
7877neneqd 2288 . . . . . . . . 9 (𝑗 ∈ ω → ¬ suc 𝑗 = ∅)
7978ad2antlr 476 . . . . . . . 8 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → ¬ suc 𝑗 = ∅)
8079iffalsed 3431 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) = (𝑝 suc 𝑗))
8148iffalsed 3431 . . . . . . 7 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(𝑗 = ∅, 1o, (𝑝 𝑗)) = (𝑝 𝑗))
8276, 80, 813sstr4d 3092 . . . . . 6 (((𝑝 ∈ ℕ𝑗 ∈ ω) ∧ ¬ 𝑗 = ∅) → if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ⊆ if(𝑗 = ∅, 1o, (𝑝 𝑗)))
83 nndceq0 4469 . . . . . . . 8 (𝑗 ∈ ω → DECID 𝑗 = ∅)
8483adantl 273 . . . . . . 7 ((𝑝 ∈ ℕ𝑗 ∈ ω) → DECID 𝑗 = ∅)
85 exmiddc 788 . . . . . . 7 (DECID 𝑗 = ∅ → (𝑗 = ∅ ∨ ¬ 𝑗 = ∅))
8684, 85syl 14 . . . . . 6 ((𝑝 ∈ ℕ𝑗 ∈ ω) → (𝑗 = ∅ ∨ ¬ 𝑗 = ∅))
8738, 82, 86mpjaodan 753 . . . . 5 ((𝑝 ∈ ℕ𝑗 ∈ ω) → if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ⊆ if(𝑗 = ∅, 1o, (𝑝 𝑗)))
88 eqeq1 2106 . . . . . . . 8 (𝑖 = suc 𝑗 → (𝑖 = ∅ ↔ suc 𝑗 = ∅))
89 unieq 3692 . . . . . . . . 9 (𝑖 = suc 𝑗 𝑖 = suc 𝑗)
9089fveq2d 5357 . . . . . . . 8 (𝑖 = suc 𝑗 → (𝑝 𝑖) = (𝑝 suc 𝑗))
9188, 90ifbieq2d 3443 . . . . . . 7 (𝑖 = suc 𝑗 → if(𝑖 = ∅, 1o, (𝑝 𝑖)) = if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)))
9291, 12fvmptg 5429 . . . . . 6 ((suc 𝑗 ∈ ω ∧ if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)) ∈ 2o) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘suc 𝑗) = if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)))
9324, 30, 92syl2anc 406 . . . . 5 ((𝑝 ∈ ℕ𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘suc 𝑗) = if(suc 𝑗 = ∅, 1o, (𝑝 suc 𝑗)))
9422, 72ffvelrnd 5488 . . . . . . 7 ((𝑝 ∈ ℕ𝑗 ∈ ω) → (𝑝 𝑗) ∈ 2o)
9521, 94, 84ifcldcd 3454 . . . . . 6 ((𝑝 ∈ ℕ𝑗 ∈ ω) → if(𝑗 = ∅, 1o, (𝑝 𝑗)) ∈ 2o)
96 eqeq1 2106 . . . . . . . 8 (𝑖 = 𝑗 → (𝑖 = ∅ ↔ 𝑗 = ∅))
97 unieq 3692 . . . . . . . . 9 (𝑖 = 𝑗 𝑖 = 𝑗)
9897fveq2d 5357 . . . . . . . 8 (𝑖 = 𝑗 → (𝑝 𝑖) = (𝑝 𝑗))
9996, 98ifbieq2d 3443 . . . . . . 7 (𝑖 = 𝑗 → if(𝑖 = ∅, 1o, (𝑝 𝑖)) = if(𝑗 = ∅, 1o, (𝑝 𝑗)))
10099, 12fvmptg 5429 . . . . . 6 ((𝑗 ∈ ω ∧ if(𝑗 = ∅, 1o, (𝑝 𝑗)) ∈ 2o) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘𝑗) = if(𝑗 = ∅, 1o, (𝑝 𝑗)))
10139, 95, 100syl2anc 406 . . . . 5 ((𝑝 ∈ ℕ𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘𝑗) = if(𝑗 = ∅, 1o, (𝑝 𝑗)))
10287, 93, 1013sstr4d 3092 . . . 4 ((𝑝 ∈ ℕ𝑗 ∈ ω) → ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘𝑗))
103102ralrimiva 2464 . . 3 (𝑝 ∈ ℕ → ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘𝑗))
104 fveq1 5352 . . . . . 6 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) → (𝑓‘suc 𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘suc 𝑗))
105 fveq1 5352 . . . . . 6 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) → (𝑓𝑗) = ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘𝑗))
106104, 105sseq12d 3078 . . . . 5 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘𝑗)))
107106ralbidv 2396 . . . 4 (𝑓 = (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘𝑗)))
108107, 61elrab2 2796 . . 3 ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) ∈ ℕ ↔ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖)))‘𝑗)))
10918, 103, 108sylanbrc 411 . 2 (𝑝 ∈ ℕ → (𝑖 ∈ ω ↦ if(𝑖 = ∅, 1o, (𝑝 𝑖))) ∈ ℕ)
1101, 109fmpti 5504 1 𝑆:ℕ⟶ℕ
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ∧ wa 103   ↔ wb 104   ∨ wo 670  DECID wdc 786   = wceq 1299   ∈ wcel 1448   ≠ wne 2267  ∀wral 2375  Vcvv 2641   ⊆ wss 3021  ∅c0 3310  ifcif 3421  ∪ cuni 3683   ↦ cmpt 3929  Tr wtr 3966  Ord word 4222  suc csuc 4225  ωcom 4442  ⟶wf 5055  ‘cfv 5059  (class class class)co 5706  1oc1o 6236  2oc2o 6237   ↑𝑚 cmap 6472  ℕ∞xnninf 6917 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-nul 3994  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-iinf 4440 This theorem depends on definitions:  df-bi 116  df-dc 787  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-ral 2380  df-rex 2381  df-rab 2384  df-v 2643  df-sbc 2863  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-nul 3311  df-if 3422  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-int 3719  df-br 3876  df-opab 3930  df-mpt 3931  df-tr 3967  df-id 4153  df-iord 4226  df-on 4228  df-suc 4231  df-iom 4443  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-ima 4490  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-fv 5067  df-ov 5709  df-oprab 5710  df-mpo 5711  df-1o 6243  df-2o 6244  df-map 6474  df-nninf 6919 This theorem is referenced by:  peano4nninf  12784
 Copyright terms: Public domain W3C validator