ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnnninfeq2 GIF version

Theorem nnnninfeq2 7140
Description: Mapping of a natural number to an element of . Similar to nnnninfeq 7139 but if we have information about a single 1o digit, that gives information about all previous digits. (Contributed by Jim Kingdon, 4-Aug-2022.)
Hypotheses
Ref Expression
nnnninfeq2.p (𝜑𝑃 ∈ ℕ)
nnnninfeq2.n (𝜑𝑁 ∈ ω)
nnnninfeq2.1 (𝜑 → (𝑃 𝑁) = 1o)
nnnninfeq2.0 (𝜑 → (𝑃𝑁) = ∅)
Assertion
Ref Expression
nnnninfeq2 (𝜑𝑃 = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)))
Distinct variable groups:   𝑖,𝑁   𝜑,𝑖
Allowed substitution hint:   𝑃(𝑖)

Proof of Theorem nnnninfeq2
Dummy variables 𝑤 𝑥 𝑓 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnnninfeq2.p . 2 (𝜑𝑃 ∈ ℕ)
2 nnnninfeq2.n . 2 (𝜑𝑁 ∈ ω)
3 nnnninfeq2.1 . . 3 (𝜑 → (𝑃 𝑁) = 1o)
42adantr 276 . . . 4 ((𝜑 ∧ (𝑃 𝑁) = 1o) → 𝑁 ∈ ω)
5 unieq 3830 . . . . . . . 8 (𝑤 = ∅ → 𝑤 = ∅)
65fveqeq2d 5535 . . . . . . 7 (𝑤 = ∅ → ((𝑃 𝑤) = 1o ↔ (𝑃 ∅) = 1o))
76anbi2d 464 . . . . . 6 (𝑤 = ∅ → ((𝜑 ∧ (𝑃 𝑤) = 1o) ↔ (𝜑 ∧ (𝑃 ∅) = 1o)))
8 raleq 2683 . . . . . 6 (𝑤 = ∅ → (∀𝑥𝑤 (𝑃𝑥) = 1o ↔ ∀𝑥 ∈ ∅ (𝑃𝑥) = 1o))
97, 8imbi12d 234 . . . . 5 (𝑤 = ∅ → (((𝜑 ∧ (𝑃 𝑤) = 1o) → ∀𝑥𝑤 (𝑃𝑥) = 1o) ↔ ((𝜑 ∧ (𝑃 ∅) = 1o) → ∀𝑥 ∈ ∅ (𝑃𝑥) = 1o)))
10 unieq 3830 . . . . . . . 8 (𝑤 = 𝑘 𝑤 = 𝑘)
1110fveqeq2d 5535 . . . . . . 7 (𝑤 = 𝑘 → ((𝑃 𝑤) = 1o ↔ (𝑃 𝑘) = 1o))
1211anbi2d 464 . . . . . 6 (𝑤 = 𝑘 → ((𝜑 ∧ (𝑃 𝑤) = 1o) ↔ (𝜑 ∧ (𝑃 𝑘) = 1o)))
13 raleq 2683 . . . . . 6 (𝑤 = 𝑘 → (∀𝑥𝑤 (𝑃𝑥) = 1o ↔ ∀𝑥𝑘 (𝑃𝑥) = 1o))
1412, 13imbi12d 234 . . . . 5 (𝑤 = 𝑘 → (((𝜑 ∧ (𝑃 𝑤) = 1o) → ∀𝑥𝑤 (𝑃𝑥) = 1o) ↔ ((𝜑 ∧ (𝑃 𝑘) = 1o) → ∀𝑥𝑘 (𝑃𝑥) = 1o)))
15 unieq 3830 . . . . . . . 8 (𝑤 = suc 𝑘 𝑤 = suc 𝑘)
1615fveqeq2d 5535 . . . . . . 7 (𝑤 = suc 𝑘 → ((𝑃 𝑤) = 1o ↔ (𝑃 suc 𝑘) = 1o))
1716anbi2d 464 . . . . . 6 (𝑤 = suc 𝑘 → ((𝜑 ∧ (𝑃 𝑤) = 1o) ↔ (𝜑 ∧ (𝑃 suc 𝑘) = 1o)))
18 raleq 2683 . . . . . 6 (𝑤 = suc 𝑘 → (∀𝑥𝑤 (𝑃𝑥) = 1o ↔ ∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o))
1917, 18imbi12d 234 . . . . 5 (𝑤 = suc 𝑘 → (((𝜑 ∧ (𝑃 𝑤) = 1o) → ∀𝑥𝑤 (𝑃𝑥) = 1o) ↔ ((𝜑 ∧ (𝑃 suc 𝑘) = 1o) → ∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o)))
20 unieq 3830 . . . . . . . 8 (𝑤 = 𝑁 𝑤 = 𝑁)
2120fveqeq2d 5535 . . . . . . 7 (𝑤 = 𝑁 → ((𝑃 𝑤) = 1o ↔ (𝑃 𝑁) = 1o))
2221anbi2d 464 . . . . . 6 (𝑤 = 𝑁 → ((𝜑 ∧ (𝑃 𝑤) = 1o) ↔ (𝜑 ∧ (𝑃 𝑁) = 1o)))
23 raleq 2683 . . . . . 6 (𝑤 = 𝑁 → (∀𝑥𝑤 (𝑃𝑥) = 1o ↔ ∀𝑥𝑁 (𝑃𝑥) = 1o))
2422, 23imbi12d 234 . . . . 5 (𝑤 = 𝑁 → (((𝜑 ∧ (𝑃 𝑤) = 1o) → ∀𝑥𝑤 (𝑃𝑥) = 1o) ↔ ((𝜑 ∧ (𝑃 𝑁) = 1o) → ∀𝑥𝑁 (𝑃𝑥) = 1o)))
25 ral0 3536 . . . . . 6 𝑥 ∈ ∅ (𝑃𝑥) = 1o
2625a1i 9 . . . . 5 ((𝜑 ∧ (𝑃 ∅) = 1o) → ∀𝑥 ∈ ∅ (𝑃𝑥) = 1o)
27 uni0 3848 . . . . . . . . . . . . . . . 16 ∅ = ∅
28 unieq 3830 . . . . . . . . . . . . . . . 16 (𝑘 = ∅ → 𝑘 = ∅)
29 id 19 . . . . . . . . . . . . . . . 16 (𝑘 = ∅ → 𝑘 = ∅)
3027, 28, 293eqtr4a 2246 . . . . . . . . . . . . . . 15 (𝑘 = ∅ → 𝑘 = 𝑘)
3130fveq2d 5531 . . . . . . . . . . . . . 14 (𝑘 = ∅ → (𝑃 𝑘) = (𝑃𝑘))
32 nnord 4623 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ω → Ord 𝑘)
33 ordtr 4390 . . . . . . . . . . . . . . . . . . 19 (Ord 𝑘 → Tr 𝑘)
3432, 33syl 14 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ω → Tr 𝑘)
3534ad3antlr 493 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → Tr 𝑘)
36 unisucg 4426 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ω → (Tr 𝑘 suc 𝑘 = 𝑘))
3736ad3antlr 493 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → (Tr 𝑘 suc 𝑘 = 𝑘))
3835, 37mpbid 147 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → suc 𝑘 = 𝑘)
3938fveq2d 5531 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → (𝑃 suc 𝑘) = (𝑃𝑘))
40 simpr 110 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → (𝑃 suc 𝑘) = 1o)
4139, 40eqtr3d 2222 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → (𝑃𝑘) = 1o)
4231, 41sylan9eqr 2242 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ 𝑘 = ∅) → (𝑃 𝑘) = 1o)
43 nninff 7134 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ ℕ𝑃:ω⟶2o)
441, 43syl 14 . . . . . . . . . . . . . . . . . 18 (𝜑𝑃:ω⟶2o)
4544adantr 276 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ω) → 𝑃:ω⟶2o)
46 nnpredcl 4634 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ω → 𝑘 ∈ ω)
4746adantl 277 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ω) → 𝑘 ∈ ω)
4845, 47ffvelcdmd 5665 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ω) → (𝑃 𝑘) ∈ 2o)
49 el2oss1o 6457 . . . . . . . . . . . . . . . 16 ((𝑃 𝑘) ∈ 2o → (𝑃 𝑘) ⊆ 1o)
5048, 49syl 14 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ ω) → (𝑃 𝑘) ⊆ 1o)
5150ad3antrrr 492 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → (𝑃 𝑘) ⊆ 1o)
52 simp-4r 542 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → 𝑘 ∈ ω)
53 simpr 110 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → ¬ 𝑘 = ∅)
5453neqned 2364 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → 𝑘 ≠ ∅)
55 nnsucpred 4628 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ω ∧ 𝑘 ≠ ∅) → suc 𝑘 = 𝑘)
5652, 54, 55syl2anc 411 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → suc 𝑘 = 𝑘)
5756fveq2d 5531 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → (𝑃‘suc 𝑘) = (𝑃𝑘))
5841adantr 276 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → (𝑃𝑘) = 1o)
5957, 58eqtrd 2220 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → (𝑃‘suc 𝑘) = 1o)
60 suceq 4414 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑘 → suc 𝑗 = suc 𝑘)
6160fveq2d 5531 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑘 → (𝑃‘suc 𝑗) = (𝑃‘suc 𝑘))
62 fveq2 5527 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑘 → (𝑃𝑗) = (𝑃 𝑘))
6361, 62sseq12d 3198 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑘 → ((𝑃‘suc 𝑗) ⊆ (𝑃𝑗) ↔ (𝑃‘suc 𝑘) ⊆ (𝑃 𝑘)))
64 fveq1 5526 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑃 → (𝑓‘suc 𝑗) = (𝑃‘suc 𝑗))
65 fveq1 5526 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑃 → (𝑓𝑗) = (𝑃𝑗))
6664, 65sseq12d 3198 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑃 → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
6766ralbidv 2487 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝑃 → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
68 df-nninf 7132 . . . . . . . . . . . . . . . . . . . . 21 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗)}
6967, 68elrab2 2908 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ ℕ ↔ (𝑃 ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
701, 69sylib 122 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑃 ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗)))
7170simprd 114 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗))
7271ad3antrrr 492 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → ∀𝑗 ∈ ω (𝑃‘suc 𝑗) ⊆ (𝑃𝑗))
7346ad3antlr 493 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → 𝑘 ∈ ω)
7463, 72, 73rspcdva 2858 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → (𝑃‘suc 𝑘) ⊆ (𝑃 𝑘))
7574adantr 276 . . . . . . . . . . . . . . 15 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → (𝑃‘suc 𝑘) ⊆ (𝑃 𝑘))
7659, 75eqsstrrd 3204 . . . . . . . . . . . . . 14 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → 1o ⊆ (𝑃 𝑘))
7751, 76eqssd 3184 . . . . . . . . . . . . 13 (((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) ∧ ¬ 𝑘 = ∅) → (𝑃 𝑘) = 1o)
78 nndceq0 4629 . . . . . . . . . . . . . . 15 (𝑘 ∈ ω → DECID 𝑘 = ∅)
79 exmiddc 837 . . . . . . . . . . . . . . 15 (DECID 𝑘 = ∅ → (𝑘 = ∅ ∨ ¬ 𝑘 = ∅))
8078, 79syl 14 . . . . . . . . . . . . . 14 (𝑘 ∈ ω → (𝑘 = ∅ ∨ ¬ 𝑘 = ∅))
8180ad3antlr 493 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → (𝑘 = ∅ ∨ ¬ 𝑘 = ∅))
8242, 77, 81mpjaodan 799 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → (𝑃 𝑘) = 1o)
83 simplr 528 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o))
8482, 83mpd 13 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → ∀𝑥𝑘 (𝑃𝑥) = 1o)
85 fveqeq2 5536 . . . . . . . . . . . . 13 (𝑥 = 𝑘 → ((𝑃𝑥) = 1o ↔ (𝑃𝑘) = 1o))
8685ralunsn 3809 . . . . . . . . . . . 12 (𝑘 ∈ ω → (∀𝑥 ∈ (𝑘 ∪ {𝑘})(𝑃𝑥) = 1o ↔ (∀𝑥𝑘 (𝑃𝑥) = 1o ∧ (𝑃𝑘) = 1o)))
8786ad3antlr 493 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → (∀𝑥 ∈ (𝑘 ∪ {𝑘})(𝑃𝑥) = 1o ↔ (∀𝑥𝑘 (𝑃𝑥) = 1o ∧ (𝑃𝑘) = 1o)))
8884, 41, 87mpbir2and 945 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → ∀𝑥 ∈ (𝑘 ∪ {𝑘})(𝑃𝑥) = 1o)
89 df-suc 4383 . . . . . . . . . . 11 suc 𝑘 = (𝑘 ∪ {𝑘})
9089raleqi 2687 . . . . . . . . . 10 (∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o ↔ ∀𝑥 ∈ (𝑘 ∪ {𝑘})(𝑃𝑥) = 1o)
9188, 90sylibr 134 . . . . . . . . 9 ((((𝜑𝑘 ∈ ω) ∧ ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) ∧ (𝑃 suc 𝑘) = 1o) → ∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o)
9291exp31 364 . . . . . . . 8 ((𝜑𝑘 ∈ ω) → (((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o) → ((𝑃 suc 𝑘) = 1o → ∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o)))
9392expcom 116 . . . . . . 7 (𝑘 ∈ ω → (𝜑 → (((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o) → ((𝑃 suc 𝑘) = 1o → ∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o))))
9493a2d 26 . . . . . 6 (𝑘 ∈ ω → ((𝜑 → ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)) → (𝜑 → ((𝑃 suc 𝑘) = 1o → ∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o))))
95 impexp 263 . . . . . 6 (((𝜑 ∧ (𝑃 𝑘) = 1o) → ∀𝑥𝑘 (𝑃𝑥) = 1o) ↔ (𝜑 → ((𝑃 𝑘) = 1o → ∀𝑥𝑘 (𝑃𝑥) = 1o)))
96 impexp 263 . . . . . 6 (((𝜑 ∧ (𝑃 suc 𝑘) = 1o) → ∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o) ↔ (𝜑 → ((𝑃 suc 𝑘) = 1o → ∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o)))
9794, 95, 963imtr4g 205 . . . . 5 (𝑘 ∈ ω → (((𝜑 ∧ (𝑃 𝑘) = 1o) → ∀𝑥𝑘 (𝑃𝑥) = 1o) → ((𝜑 ∧ (𝑃 suc 𝑘) = 1o) → ∀𝑥 ∈ suc 𝑘(𝑃𝑥) = 1o)))
989, 14, 19, 24, 26, 97finds 4611 . . . 4 (𝑁 ∈ ω → ((𝜑 ∧ (𝑃 𝑁) = 1o) → ∀𝑥𝑁 (𝑃𝑥) = 1o))
994, 98mpcom 36 . . 3 ((𝜑 ∧ (𝑃 𝑁) = 1o) → ∀𝑥𝑁 (𝑃𝑥) = 1o)
1003, 99mpdan 421 . 2 (𝜑 → ∀𝑥𝑁 (𝑃𝑥) = 1o)
101 nnnninfeq2.0 . 2 (𝜑 → (𝑃𝑁) = ∅)
1021, 2, 100, 101nnnninfeq 7139 1 (𝜑𝑃 = (𝑖 ∈ ω ↦ if(𝑖𝑁, 1o, ∅)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  DECID wdc 835   = wceq 1363  wcel 2158  wne 2357  wral 2465  cun 3139  wss 3141  c0 3434  ifcif 3546  {csn 3604   cuni 3821  cmpt 4076  Tr wtr 4113  Ord word 4374  suc csuc 4377  ωcom 4601  wf 5224  cfv 5228  (class class class)co 5888  1oc1o 6423  2oc2o 6424  𝑚 cmap 6661  xnninf 7131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-rex 2471  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-iord 4378  df-on 4380  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-fv 5236  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1o 6430  df-2o 6431  df-map 6663  df-nninf 7132
This theorem is referenced by:  nninfisollemeq  7143
  Copyright terms: Public domain W3C validator