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

Theorem ennnfonelemkh 12412
Description: Lemma for ennnfone 12425. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 DECID π‘₯ = 𝑦)
ennnfonelemh.f (πœ‘ β†’ 𝐹:ω–onto→𝐴)
ennnfonelemh.ne (πœ‘ β†’ βˆ€π‘› ∈ Ο‰ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))
ennnfonelemh.g 𝐺 = (π‘₯ ∈ (𝐴 ↑pm Ο‰), 𝑦 ∈ Ο‰ ↦ if((πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑦), π‘₯, (π‘₯ βˆͺ {⟨dom π‘₯, (πΉβ€˜π‘¦)⟩})))
ennnfonelemh.n 𝑁 = frec((π‘₯ ∈ β„€ ↦ (π‘₯ + 1)), 0)
ennnfonelemh.j 𝐽 = (π‘₯ ∈ β„•0 ↦ if(π‘₯ = 0, βˆ…, (β—‘π‘β€˜(π‘₯ βˆ’ 1))))
ennnfonelemh.h 𝐻 = seq0(𝐺, 𝐽)
ennnfonelemkh.p (πœ‘ β†’ 𝑃 ∈ β„•0)
Assertion
Ref Expression
ennnfonelemkh (πœ‘ β†’ dom (π»β€˜π‘ƒ) βŠ† (β—‘π‘β€˜π‘ƒ))
Distinct variable groups:   𝐴,𝑗,π‘₯,𝑦   π‘₯,𝐹,𝑦   𝑗,𝐺   𝑗,𝐻,π‘₯,𝑦   𝑗,𝐽   𝑗,𝑁,π‘₯,𝑦   πœ‘,𝑗,π‘₯,𝑦
Allowed substitution hints:   πœ‘(π‘˜,𝑛)   𝐴(π‘˜,𝑛)   𝑃(π‘₯,𝑦,𝑗,π‘˜,𝑛)   𝐹(𝑗,π‘˜,𝑛)   𝐺(π‘₯,𝑦,π‘˜,𝑛)   𝐻(π‘˜,𝑛)   𝐽(π‘₯,𝑦,π‘˜,𝑛)   𝑁(π‘˜,𝑛)

Proof of Theorem ennnfonelemkh
Dummy variables π‘š 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ennnfonelemkh.p . 2 (πœ‘ β†’ 𝑃 ∈ β„•0)
2 fveq2 5515 . . . . . . 7 (𝑀 = 0 β†’ (π»β€˜π‘€) = (π»β€˜0))
32dmeqd 4829 . . . . . 6 (𝑀 = 0 β†’ dom (π»β€˜π‘€) = dom (π»β€˜0))
4 fveq2 5515 . . . . . 6 (𝑀 = 0 β†’ (β—‘π‘β€˜π‘€) = (β—‘π‘β€˜0))
53, 4sseq12d 3186 . . . . 5 (𝑀 = 0 β†’ (dom (π»β€˜π‘€) βŠ† (β—‘π‘β€˜π‘€) ↔ dom (π»β€˜0) βŠ† (β—‘π‘β€˜0)))
65imbi2d 230 . . . 4 (𝑀 = 0 β†’ ((πœ‘ β†’ dom (π»β€˜π‘€) βŠ† (β—‘π‘β€˜π‘€)) ↔ (πœ‘ β†’ dom (π»β€˜0) βŠ† (β—‘π‘β€˜0))))
7 fveq2 5515 . . . . . . 7 (𝑀 = π‘š β†’ (π»β€˜π‘€) = (π»β€˜π‘š))
87dmeqd 4829 . . . . . 6 (𝑀 = π‘š β†’ dom (π»β€˜π‘€) = dom (π»β€˜π‘š))
9 fveq2 5515 . . . . . 6 (𝑀 = π‘š β†’ (β—‘π‘β€˜π‘€) = (β—‘π‘β€˜π‘š))
108, 9sseq12d 3186 . . . . 5 (𝑀 = π‘š β†’ (dom (π»β€˜π‘€) βŠ† (β—‘π‘β€˜π‘€) ↔ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)))
1110imbi2d 230 . . . 4 (𝑀 = π‘š β†’ ((πœ‘ β†’ dom (π»β€˜π‘€) βŠ† (β—‘π‘β€˜π‘€)) ↔ (πœ‘ β†’ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š))))
12 fveq2 5515 . . . . . . 7 (𝑀 = (π‘š + 1) β†’ (π»β€˜π‘€) = (π»β€˜(π‘š + 1)))
1312dmeqd 4829 . . . . . 6 (𝑀 = (π‘š + 1) β†’ dom (π»β€˜π‘€) = dom (π»β€˜(π‘š + 1)))
14 fveq2 5515 . . . . . 6 (𝑀 = (π‘š + 1) β†’ (β—‘π‘β€˜π‘€) = (β—‘π‘β€˜(π‘š + 1)))
1513, 14sseq12d 3186 . . . . 5 (𝑀 = (π‘š + 1) β†’ (dom (π»β€˜π‘€) βŠ† (β—‘π‘β€˜π‘€) ↔ dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1))))
1615imbi2d 230 . . . 4 (𝑀 = (π‘š + 1) β†’ ((πœ‘ β†’ dom (π»β€˜π‘€) βŠ† (β—‘π‘β€˜π‘€)) ↔ (πœ‘ β†’ dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1)))))
17 fveq2 5515 . . . . . . 7 (𝑀 = 𝑃 β†’ (π»β€˜π‘€) = (π»β€˜π‘ƒ))
1817dmeqd 4829 . . . . . 6 (𝑀 = 𝑃 β†’ dom (π»β€˜π‘€) = dom (π»β€˜π‘ƒ))
19 fveq2 5515 . . . . . 6 (𝑀 = 𝑃 β†’ (β—‘π‘β€˜π‘€) = (β—‘π‘β€˜π‘ƒ))
2018, 19sseq12d 3186 . . . . 5 (𝑀 = 𝑃 β†’ (dom (π»β€˜π‘€) βŠ† (β—‘π‘β€˜π‘€) ↔ dom (π»β€˜π‘ƒ) βŠ† (β—‘π‘β€˜π‘ƒ)))
2120imbi2d 230 . . . 4 (𝑀 = 𝑃 β†’ ((πœ‘ β†’ dom (π»β€˜π‘€) βŠ† (β—‘π‘β€˜π‘€)) ↔ (πœ‘ β†’ dom (π»β€˜π‘ƒ) βŠ† (β—‘π‘β€˜π‘ƒ))))
22 ennnfonelemh.dceq . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 DECID π‘₯ = 𝑦)
23 ennnfonelemh.f . . . . . . . . 9 (πœ‘ β†’ 𝐹:ω–onto→𝐴)
24 ennnfonelemh.ne . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘› ∈ Ο‰ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))
25 ennnfonelemh.g . . . . . . . . 9 𝐺 = (π‘₯ ∈ (𝐴 ↑pm Ο‰), 𝑦 ∈ Ο‰ ↦ if((πΉβ€˜π‘¦) ∈ (𝐹 β€œ 𝑦), π‘₯, (π‘₯ βˆͺ {⟨dom π‘₯, (πΉβ€˜π‘¦)⟩})))
26 ennnfonelemh.n . . . . . . . . 9 𝑁 = frec((π‘₯ ∈ β„€ ↦ (π‘₯ + 1)), 0)
27 ennnfonelemh.j . . . . . . . . 9 𝐽 = (π‘₯ ∈ β„•0 ↦ if(π‘₯ = 0, βˆ…, (β—‘π‘β€˜(π‘₯ βˆ’ 1))))
28 ennnfonelemh.h . . . . . . . . 9 𝐻 = seq0(𝐺, 𝐽)
2922, 23, 24, 25, 26, 27, 28ennnfonelem0 12405 . . . . . . . 8 (πœ‘ β†’ (π»β€˜0) = βˆ…)
3029dmeqd 4829 . . . . . . 7 (πœ‘ β†’ dom (π»β€˜0) = dom βˆ…)
31 dm0 4841 . . . . . . 7 dom βˆ… = βˆ…
3230, 31eqtrdi 2226 . . . . . 6 (πœ‘ β†’ dom (π»β€˜0) = βˆ…)
33 0ss 3461 . . . . . 6 βˆ… βŠ† (β—‘π‘β€˜0)
3432, 33eqsstrdi 3207 . . . . 5 (πœ‘ β†’ dom (π»β€˜0) βŠ† (β—‘π‘β€˜0))
3534a1i 9 . . . 4 (0 ∈ β„€ β†’ (πœ‘ β†’ dom (π»β€˜0) βŠ† (β—‘π‘β€˜0)))
3626frechashgf1o 10427 . . . . . . . . . . . . . 14 𝑁:ω–1-1-ontoβ†’β„•0
37 f1of 5461 . . . . . . . . . . . . . 14 (𝑁:ω–1-1-ontoβ†’β„•0 β†’ 𝑁:Ο‰βŸΆβ„•0)
3836, 37mp1i 10 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ 𝑁:Ο‰βŸΆβ„•0)
3922ad2antrr 488 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦ ∈ 𝐴 DECID π‘₯ = 𝑦)
4023ad2antrr 488 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ 𝐹:ω–onto→𝐴)
4124ad2antrr 488 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ βˆ€π‘› ∈ Ο‰ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))
42 simplr 528 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ π‘š ∈ (β„€β‰₯β€˜0))
43 nn0uz 9561 . . . . . . . . . . . . . . . . 17 β„•0 = (β„€β‰₯β€˜0)
4442, 43eleqtrrdi 2271 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ π‘š ∈ β„•0)
45 peano2nn0 9215 . . . . . . . . . . . . . . . 16 (π‘š ∈ β„•0 β†’ (π‘š + 1) ∈ β„•0)
4644, 45syl 14 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (π‘š + 1) ∈ β„•0)
4739, 40, 41, 25, 26, 27, 28, 46ennnfonelemom 12408 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ dom (π»β€˜(π‘š + 1)) ∈ Ο‰)
4847adantr 276 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) ∈ Ο‰)
4938, 48ffvelcdmd 5652 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜(π‘š + 1))) ∈ β„•0)
5049nn0red 9229 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜(π‘š + 1))) ∈ ℝ)
5144nn0red 9229 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ π‘š ∈ ℝ)
5251adantr 276 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ π‘š ∈ ℝ)
53 peano2re 8092 . . . . . . . . . . . 12 (π‘š ∈ ℝ β†’ (π‘š + 1) ∈ ℝ)
5452, 53syl 14 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘š + 1) ∈ ℝ)
5539, 40, 41, 25, 26, 27, 28, 44ennnfonelemp1 12406 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (π»β€˜(π‘š + 1)) = if((πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)), (π»β€˜π‘š), ((π»β€˜π‘š) βˆͺ {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩})))
5655adantr 276 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π»β€˜(π‘š + 1)) = if((πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)), (π»β€˜π‘š), ((π»β€˜π‘š) βˆͺ {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩})))
57 simpr 110 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)))
5857iftrued 3541 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ if((πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)), (π»β€˜π‘š), ((π»β€˜π‘š) βˆͺ {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩})) = (π»β€˜π‘š))
5956, 58eqtrd 2210 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π»β€˜(π‘š + 1)) = (π»β€˜π‘š))
6059dmeqd 4829 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) = dom (π»β€˜π‘š))
6160fveq2d 5519 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜(π‘š + 1))) = (π‘β€˜dom (π»β€˜π‘š)))
62 simpr 110 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š))
63 0zd 9264 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ 0 ∈ β„€)
6439, 40, 41, 25, 26, 27, 28, 44ennnfonelemom 12408 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ dom (π»β€˜π‘š) ∈ Ο‰)
65 f1ocnv 5474 . . . . . . . . . . . . . . . . . . . 20 (𝑁:ω–1-1-ontoβ†’β„•0 β†’ ◑𝑁:β„•0–1-1-ontoβ†’Ο‰)
6636, 65ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ◑𝑁:β„•0–1-1-ontoβ†’Ο‰
67 f1of 5461 . . . . . . . . . . . . . . . . . . 19 (◑𝑁:β„•0–1-1-ontoβ†’Ο‰ β†’ ◑𝑁:β„•0βŸΆΟ‰)
6866, 67mp1i 10 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ ◑𝑁:β„•0βŸΆΟ‰)
69 id 19 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ β„•0 β†’ π‘š ∈ β„•0)
7068, 69ffvelcdmd 5652 . . . . . . . . . . . . . . . . 17 (π‘š ∈ β„•0 β†’ (β—‘π‘β€˜π‘š) ∈ Ο‰)
7144, 70syl 14 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (β—‘π‘β€˜π‘š) ∈ Ο‰)
7263, 26, 64, 71frec2uzled 10428 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š) ↔ (π‘β€˜dom (π»β€˜π‘š)) ≀ (π‘β€˜(β—‘π‘β€˜π‘š))))
7362, 72mpbid 147 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (π‘β€˜dom (π»β€˜π‘š)) ≀ (π‘β€˜(β—‘π‘β€˜π‘š)))
74 f1ocnvfv2 5778 . . . . . . . . . . . . . . 15 ((𝑁:ω–1-1-ontoβ†’β„•0 ∧ π‘š ∈ β„•0) β†’ (π‘β€˜(β—‘π‘β€˜π‘š)) = π‘š)
7536, 44, 74sylancr 414 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (π‘β€˜(β—‘π‘β€˜π‘š)) = π‘š)
7673, 75breqtrd 4029 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (π‘β€˜dom (π»β€˜π‘š)) ≀ π‘š)
7776adantr 276 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜π‘š)) ≀ π‘š)
7861, 77eqbrtrd 4025 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ π‘š)
7952lep1d 8887 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ π‘š ≀ (π‘š + 1))
8050, 52, 54, 78, 79letrd 8080 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ (π‘š + 1))
81 f1ocnvfv2 5778 . . . . . . . . . . . 12 ((𝑁:ω–1-1-ontoβ†’β„•0 ∧ (π‘š + 1) ∈ β„•0) β†’ (π‘β€˜(β—‘π‘β€˜(π‘š + 1))) = (π‘š + 1))
8236, 46, 81sylancr 414 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (π‘β€˜(β—‘π‘β€˜(π‘š + 1))) = (π‘š + 1))
8382adantr 276 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜(β—‘π‘β€˜(π‘š + 1))) = (π‘š + 1))
8480, 83breqtrrd 4031 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ (π‘β€˜(β—‘π‘β€˜(π‘š + 1))))
8566, 67mp1i 10 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ ◑𝑁:β„•0βŸΆΟ‰)
8685, 46ffvelcdmd 5652 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (β—‘π‘β€˜(π‘š + 1)) ∈ Ο‰)
8763, 26, 47, 86frec2uzled 10428 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1)) ↔ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ (π‘β€˜(β—‘π‘β€˜(π‘š + 1)))))
8887adantr 276 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1)) ↔ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ (π‘β€˜(β—‘π‘β€˜(π‘š + 1)))))
8984, 88mpbird 167 . . . . . . . 8 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1)))
9055adantr 276 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π»β€˜(π‘š + 1)) = if((πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)), (π»β€˜π‘š), ((π»β€˜π‘š) βˆͺ {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩})))
91 simpr 110 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)))
9291iffalsed 3544 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ if((πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)), (π»β€˜π‘š), ((π»β€˜π‘š) βˆͺ {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩})) = ((π»β€˜π‘š) βˆͺ {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩}))
9390, 92eqtrd 2210 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π»β€˜(π‘š + 1)) = ((π»β€˜π‘š) βˆͺ {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩}))
9493dmeqd 4829 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) = dom ((π»β€˜π‘š) βˆͺ {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩}))
95 dmun 4834 . . . . . . . . . . . . . . . 16 dom ((π»β€˜π‘š) βˆͺ {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩}) = (dom (π»β€˜π‘š) βˆͺ dom {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩})
9694, 95eqtrdi 2226 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) = (dom (π»β€˜π‘š) βˆͺ dom {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩}))
97 fof 5438 . . . . . . . . . . . . . . . . . . . 20 (𝐹:ω–onto→𝐴 β†’ 𝐹:Ο‰βŸΆπ΄)
9840, 97syl 14 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ 𝐹:Ο‰βŸΆπ΄)
9998, 71ffvelcdmd 5652 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ 𝐴)
10099adantr 276 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ 𝐴)
101 dmsnopg 5100 . . . . . . . . . . . . . . . . 17 ((πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ 𝐴 β†’ dom {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩} = {dom (π»β€˜π‘š)})
102100, 101syl 14 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩} = {dom (π»β€˜π‘š)})
103102uneq2d 3289 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (dom (π»β€˜π‘š) βˆͺ dom {⟨dom (π»β€˜π‘š), (πΉβ€˜(β—‘π‘β€˜π‘š))⟩}) = (dom (π»β€˜π‘š) βˆͺ {dom (π»β€˜π‘š)}))
10496, 103eqtrd 2210 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) = (dom (π»β€˜π‘š) βˆͺ {dom (π»β€˜π‘š)}))
105 df-suc 4371 . . . . . . . . . . . . . 14 suc dom (π»β€˜π‘š) = (dom (π»β€˜π‘š) βˆͺ {dom (π»β€˜π‘š)})
106104, 105eqtr4di 2228 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) = suc dom (π»β€˜π‘š))
107 simplr 528 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š))
10871adantr 276 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (β—‘π‘β€˜π‘š) ∈ Ο‰)
109 nnsucsssuc 6492 . . . . . . . . . . . . . . 15 ((dom (π»β€˜π‘š) ∈ Ο‰ ∧ (β—‘π‘β€˜π‘š) ∈ Ο‰) β†’ (dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š) ↔ suc dom (π»β€˜π‘š) βŠ† suc (β—‘π‘β€˜π‘š)))
11064, 108, 109syl2an2r 595 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š) ↔ suc dom (π»β€˜π‘š) βŠ† suc (β—‘π‘β€˜π‘š)))
111107, 110mpbid 147 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ suc dom (π»β€˜π‘š) βŠ† suc (β—‘π‘β€˜π‘š))
112106, 111eqsstrd 3191 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) βŠ† suc (β—‘π‘β€˜π‘š))
113 0zd 9264 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ 0 ∈ β„€)
11447adantr 276 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) ∈ Ο‰)
115 peano2 4594 . . . . . . . . . . . . . 14 ((β—‘π‘β€˜π‘š) ∈ Ο‰ β†’ suc (β—‘π‘β€˜π‘š) ∈ Ο‰)
116108, 115syl 14 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ suc (β—‘π‘β€˜π‘š) ∈ Ο‰)
117113, 26, 114, 116frec2uzled 10428 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (dom (π»β€˜(π‘š + 1)) βŠ† suc (β—‘π‘β€˜π‘š) ↔ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ (π‘β€˜suc (β—‘π‘β€˜π‘š))))
118112, 117mpbid 147 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ (π‘β€˜suc (β—‘π‘β€˜π‘š)))
119113, 26, 108frec2uzsucd 10400 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜suc (β—‘π‘β€˜π‘š)) = ((π‘β€˜(β—‘π‘β€˜π‘š)) + 1))
12075adantr 276 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜(β—‘π‘β€˜π‘š)) = π‘š)
121120oveq1d 5889 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ ((π‘β€˜(β—‘π‘β€˜π‘š)) + 1) = (π‘š + 1))
122119, 121eqtrd 2210 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜suc (β—‘π‘β€˜π‘š)) = (π‘š + 1))
123118, 122breqtrd 4029 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ (π‘š + 1))
12482adantr 276 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜(β—‘π‘β€˜(π‘š + 1))) = (π‘š + 1))
125123, 124breqtrrd 4031 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ (π‘β€˜(β—‘π‘β€˜(π‘š + 1))))
12686adantr 276 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (β—‘π‘β€˜(π‘š + 1)) ∈ Ο‰)
127113, 26, 114, 126frec2uzled 10428 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ (dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1)) ↔ (π‘β€˜dom (π»β€˜(π‘š + 1))) ≀ (π‘β€˜(β—‘π‘β€˜(π‘š + 1)))))
128125, 127mpbird 167 . . . . . . . 8 ((((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) ∧ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))) β†’ dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1)))
12939, 40, 71ennnfonelemdc 12399 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ DECID (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)))
130 exmiddc 836 . . . . . . . . 9 (DECID (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)) β†’ ((πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)) ∨ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))))
131129, 130syl 14 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ ((πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š)) ∨ Β¬ (πΉβ€˜(β—‘π‘β€˜π‘š)) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘š))))
13289, 128, 131mpjaodan 798 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) ∧ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1)))
133132ex 115 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (β„€β‰₯β€˜0)) β†’ (dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š) β†’ dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1))))
134133expcom 116 . . . . 5 (π‘š ∈ (β„€β‰₯β€˜0) β†’ (πœ‘ β†’ (dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š) β†’ dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1)))))
135134a2d 26 . . . 4 (π‘š ∈ (β„€β‰₯β€˜0) β†’ ((πœ‘ β†’ dom (π»β€˜π‘š) βŠ† (β—‘π‘β€˜π‘š)) β†’ (πœ‘ β†’ dom (π»β€˜(π‘š + 1)) βŠ† (β—‘π‘β€˜(π‘š + 1)))))
1366, 11, 16, 21, 35, 135uzind4 9587 . . 3 (𝑃 ∈ (β„€β‰₯β€˜0) β†’ (πœ‘ β†’ dom (π»β€˜π‘ƒ) βŠ† (β—‘π‘β€˜π‘ƒ)))
137136, 43eleq2s 2272 . 2 (𝑃 ∈ β„•0 β†’ (πœ‘ β†’ dom (π»β€˜π‘ƒ) βŠ† (β—‘π‘β€˜π‘ƒ)))
1381, 137mpcom 36 1 (πœ‘ β†’ dom (π»β€˜π‘ƒ) βŠ† (β—‘π‘β€˜π‘ƒ))
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708  DECID wdc 834   = wceq 1353   ∈ wcel 2148   β‰  wne 2347  βˆ€wral 2455  βˆƒwrex 2456   βˆͺ cun 3127   βŠ† wss 3129  βˆ…c0 3422  ifcif 3534  {csn 3592  βŸ¨cop 3595   class class class wbr 4003   ↦ cmpt 4064  suc csuc 4365  Ο‰com 4589  β—‘ccnv 4625  dom cdm 4626   β€œ cima 4629  βŸΆwf 5212  β€“ontoβ†’wfo 5214  β€“1-1-ontoβ†’wf1o 5215  β€˜cfv 5216  (class class class)co 5874   ∈ cmpo 5876  freccfrec 6390   ↑pm cpm 6648  β„cr 7809  0cc0 7810  1c1 7811   + caddc 7813   ≀ cle 7992   βˆ’ cmin 8127  β„•0cn0 9175  β„€cz 9252  β„€β‰₯cuz 9527  seqcseq 10444
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-addcom 7910  ax-addass 7912  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-0id 7918  ax-rnegex 7919  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-ltadd 7926
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-frec 6391  df-pm 6650  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-inn 8919  df-n0 9176  df-z 9253  df-uz 9528  df-seqfrec 10445
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator