ennnfonelemkh - Intuitionistic Logic Explorer

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

Theorem ennnfonelemkh 12413

Description: Lemma for ennnfone 12426. 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	⊢ 𝐽 = (𝑥 ∈ ℕ₀ ↦ if(𝑥 = 0, ∅, (^◡𝑁‘(𝑥 − 1))))
ennnfonelemh.h	⊢ 𝐻 = seq0(𝐺, 𝐽)
ennnfonelemkh.p	⊢ (𝜑 → 𝑃 ∈ ℕ₀)

**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.

Step	Hyp	Ref	Expression
1		ennnfonelemkh.p	. 2 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
2		fveq2 5516	. . . . . . 7 ⊢ (𝑤 = 0 → (𝐻‘𝑤) = (𝐻‘0))
3	2	dmeqd 4830	. . . . . 6 ⊢ (𝑤 = 0 → dom (𝐻‘𝑤) = dom (𝐻‘0))
4		fveq2 5516	. . . . . 6 ⊢ (𝑤 = 0 → (^◡𝑁‘𝑤) = (^◡𝑁‘0))
5	3, 4	sseq12d 3187	. . . . 5 ⊢ (𝑤 = 0 → (dom (𝐻‘𝑤) ⊆ (^◡𝑁‘𝑤) ↔ dom (𝐻‘0) ⊆ (^◡𝑁‘0)))
6	5	imbi2d 230	. . . 4 ⊢ (𝑤 = 0 → ((𝜑 → dom (𝐻‘𝑤) ⊆ (^◡𝑁‘𝑤)) ↔ (𝜑 → dom (𝐻‘0) ⊆ (^◡𝑁‘0))))
7		fveq2 5516	. . . . . . 7 ⊢ (𝑤 = 𝑚 → (𝐻‘𝑤) = (𝐻‘𝑚))
8	7	dmeqd 4830	. . . . . 6 ⊢ (𝑤 = 𝑚 → dom (𝐻‘𝑤) = dom (𝐻‘𝑚))
9		fveq2 5516	. . . . . 6 ⊢ (𝑤 = 𝑚 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑚))
10	8, 9	sseq12d 3187	. . . . 5 ⊢ (𝑤 = 𝑚 → (dom (𝐻‘𝑤) ⊆ (^◡𝑁‘𝑤) ↔ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)))
11	10	imbi2d 230	. . . 4 ⊢ (𝑤 = 𝑚 → ((𝜑 → dom (𝐻‘𝑤) ⊆ (^◡𝑁‘𝑤)) ↔ (𝜑 → dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚))))
12		fveq2 5516	. . . . . . 7 ⊢ (𝑤 = (𝑚 + 1) → (𝐻‘𝑤) = (𝐻‘(𝑚 + 1)))
13	12	dmeqd 4830	. . . . . 6 ⊢ (𝑤 = (𝑚 + 1) → dom (𝐻‘𝑤) = dom (𝐻‘(𝑚 + 1)))
14		fveq2 5516	. . . . . 6 ⊢ (𝑤 = (𝑚 + 1) → (^◡𝑁‘𝑤) = (^◡𝑁‘(𝑚 + 1)))
15	13, 14	sseq12d 3187	. . . . 5 ⊢ (𝑤 = (𝑚 + 1) → (dom (𝐻‘𝑤) ⊆ (^◡𝑁‘𝑤) ↔ dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1))))
16	15	imbi2d 230	. . . 4 ⊢ (𝑤 = (𝑚 + 1) → ((𝜑 → dom (𝐻‘𝑤) ⊆ (^◡𝑁‘𝑤)) ↔ (𝜑 → dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1)))))
17		fveq2 5516	. . . . . . 7 ⊢ (𝑤 = 𝑃 → (𝐻‘𝑤) = (𝐻‘𝑃))
18	17	dmeqd 4830	. . . . . 6 ⊢ (𝑤 = 𝑃 → dom (𝐻‘𝑤) = dom (𝐻‘𝑃))
19		fveq2 5516	. . . . . 6 ⊢ (𝑤 = 𝑃 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑃))
20	18, 19	sseq12d 3187	. . . . 5 ⊢ (𝑤 = 𝑃 → (dom (𝐻‘𝑤) ⊆ (^◡𝑁‘𝑤) ↔ dom (𝐻‘𝑃) ⊆ (^◡𝑁‘𝑃)))
21	20	imbi2d 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 ⊢ 𝐽 = (𝑥 ∈ ℕ₀ ↦ if(𝑥 = 0, ∅, (^◡𝑁‘(𝑥 − 1))))
28		ennnfonelemh.h	. . . . . . . . 9 ⊢ 𝐻 = seq0(𝐺, 𝐽)
29	22, 23, 24, 25, 26, 27, 28	ennnfonelem0 12406	. . . . . . . 8 ⊢ (𝜑 → (𝐻‘0) = ∅)
30	29	dmeqd 4830	. . . . . . 7 ⊢ (𝜑 → dom (𝐻‘0) = dom ∅)
31		dm0 4842	. . . . . . 7 ⊢ dom ∅ = ∅
32	30, 31	eqtrdi 2226	. . . . . 6 ⊢ (𝜑 → dom (𝐻‘0) = ∅)
33		0ss 3462	. . . . . 6 ⊢ ∅ ⊆ (^◡𝑁‘0)
34	32, 33	eqsstrdi 3208	. . . . 5 ⊢ (𝜑 → dom (𝐻‘0) ⊆ (^◡𝑁‘0))
35	34	a1i 9	. . . 4 ⊢ (0 ∈ ℤ → (𝜑 → dom (𝐻‘0) ⊆ (^◡𝑁‘0)))
36	26	frechashgf1o 10428	. . . . . . . . . . . . . 14 ⊢ 𝑁:ω–1-1-onto→ℕ₀
37		f1of 5462	. . . . . . . . . . . . . 14 ⊢ (𝑁:ω–1-1-onto→ℕ₀ → 𝑁:ω⟶ℕ₀)
38	36, 37	mp1i 10	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → 𝑁:ω⟶ℕ₀)
39	22	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
40	23	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → 𝐹:ω–onto→𝐴)
41	24	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
42		simplr 528	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → 𝑚 ∈ (ℤ_≥‘0))
43		nn0uz 9562	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥‘0)
44	42, 43	eleqtrrdi 2271	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → 𝑚 ∈ ℕ₀)
45		peano2nn0 9216	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℕ₀ → (𝑚 + 1) ∈ ℕ₀)
46	44, 45	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (𝑚 + 1) ∈ ℕ₀)
47	39, 40, 41, 25, 26, 27, 28, 46	ennnfonelemom 12409	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → dom (𝐻‘(𝑚 + 1)) ∈ ω)
48	47	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) ∈ ω)
49	38, 48	ffvelcdmd 5653	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘(𝑚 + 1))) ∈ ℕ₀)
50	49	nn0red 9230	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘(𝑚 + 1))) ∈ ℝ)
51	44	nn0red 9230	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → 𝑚 ∈ ℝ)
52	51	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → 𝑚 ∈ ℝ)
53		peano2re 8093	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℝ → (𝑚 + 1) ∈ ℝ)
54	52, 53	syl 14	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑚 + 1) ∈ ℝ)
55	39, 40, 41, 25, 26, 27, 28, 44	ennnfonelemp1 12407	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (𝐻‘(𝑚 + 1)) = if((𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)), (𝐻‘𝑚), ((𝐻‘𝑚) ∪ {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩})))
56	55	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝐻‘(𝑚 + 1)) = if((𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)), (𝐻‘𝑚), ((𝐻‘𝑚) ∪ {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩})))
57		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)))
58	57	iftrued 3542	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → if((𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)), (𝐻‘𝑚), ((𝐻‘𝑚) ∪ {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩})) = (𝐻‘𝑚))
59	56, 58	eqtrd 2210	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝐻‘(𝑚 + 1)) = (𝐻‘𝑚))
60	59	dmeqd 4830	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) = dom (𝐻‘𝑚))
61	60	fveq2d 5520	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘(𝑚 + 1))) = (𝑁‘dom (𝐻‘𝑚)))
62		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚))
63		0zd 9265	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → 0 ∈ ℤ)
64	39, 40, 41, 25, 26, 27, 28, 44	ennnfonelemom 12409	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → dom (𝐻‘𝑚) ∈ ω)
65		f1ocnv 5475	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁:ω–1-1-onto→ℕ₀ → ^◡𝑁:ℕ₀–1-1-onto→ω)
66	36, 65	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ^◡𝑁:ℕ₀–1-1-onto→ω
67		f1of 5462	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡𝑁:ℕ₀–1-1-onto→ω → ^◡𝑁:ℕ₀⟶ω)
68	66, 67	mp1i 10	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ₀ → ^◡𝑁:ℕ₀⟶ω)
69		id 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℕ₀)
70	68, 69	ffvelcdmd 5653	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ₀ → (^◡𝑁‘𝑚) ∈ ω)
71	44, 70	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (^◡𝑁‘𝑚) ∈ ω)
72	63, 26, 64, 71	frec2uzled 10429	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚) ↔ (𝑁‘dom (𝐻‘𝑚)) ≤ (𝑁‘(^◡𝑁‘𝑚))))
73	62, 72	mpbid 147	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (𝑁‘dom (𝐻‘𝑚)) ≤ (𝑁‘(^◡𝑁‘𝑚)))
74		f1ocnvfv2 5779	. . . . . . . . . . . . . . 15 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ 𝑚 ∈ ℕ₀) → (𝑁‘(^◡𝑁‘𝑚)) = 𝑚)
75	36, 44, 74	sylancr 414	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (𝑁‘(^◡𝑁‘𝑚)) = 𝑚)
76	73, 75	breqtrd 4030	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (𝑁‘dom (𝐻‘𝑚)) ≤ 𝑚)
77	76	adantr 276	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘𝑚)) ≤ 𝑚)
78	61, 77	eqbrtrd 4026	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ 𝑚)
79	52	lep1d 8888	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → 𝑚 ≤ (𝑚 + 1))
80	50, 52, 54, 78, 79	letrd 8081	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ (𝑚 + 1))
81		f1ocnvfv2 5779	. . . . . . . . . . . 12 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ (𝑚 + 1) ∈ ℕ₀) → (𝑁‘(^◡𝑁‘(𝑚 + 1))) = (𝑚 + 1))
82	36, 46, 81	sylancr 414	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (𝑁‘(^◡𝑁‘(𝑚 + 1))) = (𝑚 + 1))
83	82	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘(^◡𝑁‘(𝑚 + 1))) = (𝑚 + 1))
84	80, 83	breqtrrd 4032	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ (𝑁‘(^◡𝑁‘(𝑚 + 1))))
85	66, 67	mp1i 10	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → ^◡𝑁:ℕ₀⟶ω)
86	85, 46	ffvelcdmd 5653	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (^◡𝑁‘(𝑚 + 1)) ∈ ω)
87	63, 26, 47, 86	frec2uzled 10429	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1)) ↔ (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ (𝑁‘(^◡𝑁‘(𝑚 + 1)))))
88	87	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1)) ↔ (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ (𝑁‘(^◡𝑁‘(𝑚 + 1)))))
89	84, 88	mpbird 167	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1)))
90	55	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝐻‘(𝑚 + 1)) = if((𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)), (𝐻‘𝑚), ((𝐻‘𝑚) ∪ {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩})))
91		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)))
92	91	iffalsed 3545	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → if((𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)), (𝐻‘𝑚), ((𝐻‘𝑚) ∪ {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩})) = ((𝐻‘𝑚) ∪ {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩}))
93	90, 92	eqtrd 2210	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝐻‘(𝑚 + 1)) = ((𝐻‘𝑚) ∪ {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩}))
94	93	dmeqd 4830	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) = dom ((𝐻‘𝑚) ∪ {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩}))
95		dmun 4835	. . . . . . . . . . . . . . . 16 ⊢ dom ((𝐻‘𝑚) ∪ {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩}) = (dom (𝐻‘𝑚) ∪ dom {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩})
96	94, 95	eqtrdi 2226	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) = (dom (𝐻‘𝑚) ∪ dom {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩}))
97		fof 5439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹:ω–onto→𝐴 → 𝐹:ω⟶𝐴)
98	40, 97	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → 𝐹:ω⟶𝐴)
99	98, 71	ffvelcdmd 5653	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (𝐹‘(^◡𝑁‘𝑚)) ∈ 𝐴)
100	99	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝐹‘(^◡𝑁‘𝑚)) ∈ 𝐴)
101		dmsnopg 5101	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(^◡𝑁‘𝑚)) ∈ 𝐴 → dom {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩} = {dom (𝐻‘𝑚)})
102	100, 101	syl 14	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩} = {dom (𝐻‘𝑚)})
103	102	uneq2d 3290	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (dom (𝐻‘𝑚) ∪ dom {⟨dom (𝐻‘𝑚), (𝐹‘(^◡𝑁‘𝑚))⟩}) = (dom (𝐻‘𝑚) ∪ {dom (𝐻‘𝑚)}))
104	96, 103	eqtrd 2210	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) = (dom (𝐻‘𝑚) ∪ {dom (𝐻‘𝑚)}))
105		df-suc 4372	. . . . . . . . . . . . . 14 ⊢ suc dom (𝐻‘𝑚) = (dom (𝐻‘𝑚) ∪ {dom (𝐻‘𝑚)})
106	104, 105	eqtr4di 2228	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) = suc dom (𝐻‘𝑚))
107		simplr 528	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚))
108	71	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (^◡𝑁‘𝑚) ∈ ω)
109		nnsucsssuc 6493	. . . . . . . . . . . . . . 15 ⊢ ((dom (𝐻‘𝑚) ∈ ω ∧ (^◡𝑁‘𝑚) ∈ ω) → (dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚) ↔ suc dom (𝐻‘𝑚) ⊆ suc (^◡𝑁‘𝑚)))
110	64, 108, 109	syl2an2r 595	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚) ↔ suc dom (𝐻‘𝑚) ⊆ suc (^◡𝑁‘𝑚)))
111	107, 110	mpbid 147	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → suc dom (𝐻‘𝑚) ⊆ suc (^◡𝑁‘𝑚))
112	106, 111	eqsstrd 3192	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) ⊆ suc (^◡𝑁‘𝑚))
113		0zd 9265	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → 0 ∈ ℤ)
114	47	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) ∈ ω)
115		peano2 4595	. . . . . . . . . . . . . 14 ⊢ ((^◡𝑁‘𝑚) ∈ ω → suc (^◡𝑁‘𝑚) ∈ ω)
116	108, 115	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → suc (^◡𝑁‘𝑚) ∈ ω)
117	113, 26, 114, 116	frec2uzled 10429	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (dom (𝐻‘(𝑚 + 1)) ⊆ suc (^◡𝑁‘𝑚) ↔ (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ (𝑁‘suc (^◡𝑁‘𝑚))))
118	112, 117	mpbid 147	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ (𝑁‘suc (^◡𝑁‘𝑚)))
119	113, 26, 108	frec2uzsucd 10401	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘suc (^◡𝑁‘𝑚)) = ((𝑁‘(^◡𝑁‘𝑚)) + 1))
120	75	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘(^◡𝑁‘𝑚)) = 𝑚)
121	120	oveq1d 5890	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → ((𝑁‘(^◡𝑁‘𝑚)) + 1) = (𝑚 + 1))
122	119, 121	eqtrd 2210	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘suc (^◡𝑁‘𝑚)) = (𝑚 + 1))
123	118, 122	breqtrd 4030	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ (𝑚 + 1))
124	82	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘(^◡𝑁‘(𝑚 + 1))) = (𝑚 + 1))
125	123, 124	breqtrrd 4032	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ (𝑁‘(^◡𝑁‘(𝑚 + 1))))
126	86	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (^◡𝑁‘(𝑚 + 1)) ∈ ω)
127	113, 26, 114, 126	frec2uzled 10429	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → (dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1)) ↔ (𝑁‘dom (𝐻‘(𝑚 + 1))) ≤ (𝑁‘(^◡𝑁‘(𝑚 + 1)))))
128	125, 127	mpbird 167	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) ∧ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))) → dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1)))
129	39, 40, 71	ennnfonelemdc 12400	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → DECID (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)))
130		exmiddc 836	. . . . . . . . 9 ⊢ (DECID (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)) → ((𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))))
131	129, 130	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → ((𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑚)) ∈ (𝐹 “ (^◡𝑁‘𝑚))))
132	89, 128, 131	mpjaodan 798	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) ∧ dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1)))
133	132	ex 115	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘0)) → (dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚) → dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1))))
134	133	expcom 116	. . . . 5 ⊢ (𝑚 ∈ (ℤ_≥‘0) → (𝜑 → (dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚) → dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1)))))
135	134	a2d 26	. . . 4 ⊢ (𝑚 ∈ (ℤ_≥‘0) → ((𝜑 → dom (𝐻‘𝑚) ⊆ (^◡𝑁‘𝑚)) → (𝜑 → dom (𝐻‘(𝑚 + 1)) ⊆ (^◡𝑁‘(𝑚 + 1)))))
136	6, 11, 16, 21, 35, 135	uzind4 9588	. . 3 ⊢ (𝑃 ∈ (ℤ_≥‘0) → (𝜑 → dom (𝐻‘𝑃) ⊆ (^◡𝑁‘𝑃)))
137	136, 43	eleq2s 2272	. 2 ⊢ (𝑃 ∈ ℕ₀ → (𝜑 → dom (𝐻‘𝑃) ⊆ (^◡𝑁‘𝑃)))
138	1, 137	mpcom 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 3128 ⊆ wss 3130 ∅c0 3423 ifcif 3535 {csn 3593 ⟨cop 3596 class class class wbr 4004 ↦ cmpt 4065 suc csuc 4366 ωcom 4590 ^◡ccnv 4626 dom cdm 4627 “ cima 4630 ⟶wf 5213 –onto→wfo 5215 –1-1-onto→wf1o 5216 ‘cfv 5217 (class class class)co 5875 ∈ cmpo 5877 freccfrec 6391 ↑_pm cpm 6649 ℝcr 7810 0cc0 7811 1c1 7812 + caddc 7814 ≤ cle 7993 − cmin 8128 ℕ₀cn0 9176 ℤcz 9253 ℤ_≥cuz 9528 seqcseq 10445

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 4119 ax-sep 4122 ax-nul 4130 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-setind 4537 ax-iinf 4588 ax-cnex 7902 ax-resscn 7903 ax-1cn 7904 ax-1re 7905 ax-icn 7906 ax-addcl 7907 ax-addrcl 7908 ax-mulcl 7909 ax-addcom 7911 ax-addass 7913 ax-distr 7915 ax-i2m1 7916 ax-0lt1 7917 ax-0id 7919 ax-rnegex 7920 ax-cnre 7922 ax-pre-ltirr 7923 ax-pre-ltwlin 7924 ax-pre-lttrn 7925 ax-pre-ltadd 7927

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 2740 df-sbc 2964 df-csb 3059 df-dif 3132 df-un 3134 df-in 3136 df-ss 3143 df-nul 3424 df-if 3536 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-iun 3889 df-br 4005 df-opab 4066 df-mpt 4067 df-tr 4103 df-id 4294 df-iord 4367 df-on 4369 df-ilim 4370 df-suc 4372 df-iom 4591 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-ima 4640 df-iota 5179 df-fun 5219 df-fn 5220 df-f 5221 df-f1 5222 df-fo 5223 df-f1o 5224 df-fv 5225 df-riota 5831 df-ov 5878 df-oprab 5879 df-mpo 5880 df-1st 6141 df-2nd 6142 df-recs 6306 df-frec 6392 df-pm 6651 df-pnf 7994 df-mnf 7995 df-xr 7996 df-ltxr 7997 df-le 7998 df-sub 8130 df-neg 8131 df-inn 8920 df-n0 9177 df-z 9254 df-uz 9529 df-seqfrec 10446

This theorem is referenced by: (None)

W3C validator