ennnfonelemhf1o - Intuitionistic Logic Explorer

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

Theorem ennnfonelemhf1o 12784

Description: Lemma for ennnfone 12796. Each of the functions in 𝐻 is one to one and onto an image of 𝐹. (Contributed by Jim Kingdon, 17-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(𝐺, 𝐽)
ennnfonelemhf1o.p	⊢ (𝜑 → 𝑃 ∈ ℕ₀)

**Assertion**
Ref	Expression
ennnfonelemhf1o	⊢ (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃)))

Distinct variable groups: 𝐴,𝑗,𝑥,𝑦 𝑗,𝐹,𝑘,𝑥,𝑦 𝑗,𝐺 𝑗,𝐻,𝑘,𝑥,𝑦 𝑗,𝐽 𝑗,𝑁,𝑘,𝑥,𝑦 𝜑,𝑗,𝑘,𝑥,𝑦 Allowed substitution hints: 𝜑(𝑛) 𝐴(𝑘,𝑛) 𝑃(𝑥,𝑦,𝑗,𝑘,𝑛) 𝐹(𝑛) 𝐺(𝑥,𝑦,𝑘,𝑛) 𝐻(𝑛) 𝐽(𝑥,𝑦,𝑘,𝑛) 𝑁(𝑛)

Proof of Theorem ennnfonelemhf1o Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ennnfonelemhf1o.p	. 2 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
2		fveq2 5576	. . . . 5 ⊢ (𝑤 = 0 → (𝐻‘𝑤) = (𝐻‘0))
3	2	dmeqd 4880	. . . . 5 ⊢ (𝑤 = 0 → dom (𝐻‘𝑤) = dom (𝐻‘0))
4		fveq2 5576	. . . . . 6 ⊢ (𝑤 = 0 → (^◡𝑁‘𝑤) = (^◡𝑁‘0))
5	4	imaeq2d 5022	. . . . 5 ⊢ (𝑤 = 0 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘0)))
6	2, 3, 5	f1oeq123d 5516	. . . 4 ⊢ (𝑤 = 0 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (^◡𝑁‘0))))
7	6	imbi2d 230	. . 3 ⊢ (𝑤 = 0 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (^◡𝑁‘0)))))
8		fveq2 5576	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐻‘𝑤) = (𝐻‘𝑘))
9	8	dmeqd 4880	. . . . 5 ⊢ (𝑤 = 𝑘 → dom (𝐻‘𝑤) = dom (𝐻‘𝑘))
10		fveq2 5576	. . . . . 6 ⊢ (𝑤 = 𝑘 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑘))
11	10	imaeq2d 5022	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑘)))
12	8, 9, 11	f1oeq123d 5516	. . . 4 ⊢ (𝑤 = 𝑘 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))))
13	12	imbi2d 230	. . 3 ⊢ (𝑤 = 𝑘 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))))
14		fveq2 5576	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐻‘𝑤) = (𝐻‘(𝑘 + 1)))
15	14	dmeqd 4880	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → dom (𝐻‘𝑤) = dom (𝐻‘(𝑘 + 1)))
16		fveq2 5576	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → (^◡𝑁‘𝑤) = (^◡𝑁‘(𝑘 + 1)))
17	16	imaeq2d 5022	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘(𝑘 + 1))))
18	14, 15, 17	f1oeq123d 5516	. . . 4 ⊢ (𝑤 = (𝑘 + 1) → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1)))))
19	18	imbi2d 230	. . 3 ⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))))
20		fveq2 5576	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐻‘𝑤) = (𝐻‘𝑃))
21	20	dmeqd 4880	. . . . 5 ⊢ (𝑤 = 𝑃 → dom (𝐻‘𝑤) = dom (𝐻‘𝑃))
22		fveq2 5576	. . . . . 6 ⊢ (𝑤 = 𝑃 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑃))
23	22	imaeq2d 5022	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑃)))
24	20, 21, 23	f1oeq123d 5516	. . . 4 ⊢ (𝑤 = 𝑃 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃))))
25	24	imbi2d 230	. . 3 ⊢ (𝑤 = 𝑃 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃)))))
26		f1o0 5559	. . . 4 ⊢ ∅:∅–1-1-onto→∅
27		ennnfonelemh.dceq	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
28		ennnfonelemh.f	. . . . . 6 ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
29		ennnfonelemh.ne	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
30		ennnfonelemh.g	. . . . . 6 ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑_pm ω), 𝑦 ∈ ω ↦ if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹‘𝑦)⟩})))
31		ennnfonelemh.n	. . . . . 6 ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
32		ennnfonelemh.j	. . . . . 6 ⊢ 𝐽 = (𝑥 ∈ ℕ₀ ↦ if(𝑥 = 0, ∅, (^◡𝑁‘(𝑥 − 1))))
33		ennnfonelemh.h	. . . . . 6 ⊢ 𝐻 = seq0(𝐺, 𝐽)
34	27, 28, 29, 30, 31, 32, 33	ennnfonelem0 12776	. . . . 5 ⊢ (𝜑 → (𝐻‘0) = ∅)
35	34	dmeqd 4880	. . . . . 6 ⊢ (𝜑 → dom (𝐻‘0) = dom ∅)
36		dm0 4892	. . . . . 6 ⊢ dom ∅ = ∅
37	35, 36	eqtrdi 2254	. . . . 5 ⊢ (𝜑 → dom (𝐻‘0) = ∅)
38		0zd 9384	. . . . . . . . . . . 12 ⊢ (⊤ → 0 ∈ ℤ)
39	38, 31	frec2uz0d 10544	. . . . . . . . . . 11 ⊢ (⊤ → (𝑁‘∅) = 0)
40	39	mptru 1382	. . . . . . . . . 10 ⊢ (𝑁‘∅) = 0
41	40	fveq2i 5579	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = (^◡𝑁‘0)
42	38, 31	frec2uzf1od 10551	. . . . . . . . . . 11 ⊢ (⊤ → 𝑁:ω–1-1-onto→(ℤ_≥‘0))
43	42	mptru 1382	. . . . . . . . . 10 ⊢ 𝑁:ω–1-1-onto→(ℤ_≥‘0)
44		peano1 4642	. . . . . . . . . 10 ⊢ ∅ ∈ ω
45		f1ocnvfv1 5846	. . . . . . . . . 10 ⊢ ((𝑁:ω–1-1-onto→(ℤ_≥‘0) ∧ ∅ ∈ ω) → (^◡𝑁‘(𝑁‘∅)) = ∅)
46	43, 44, 45	mp2an 426	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = ∅
47	41, 46	eqtr3i 2228	. . . . . . . 8 ⊢ (^◡𝑁‘0) = ∅
48	47	imaeq2i 5020	. . . . . . 7 ⊢ (𝐹 “ (^◡𝑁‘0)) = (𝐹 “ ∅)
49		ima0 5041	. . . . . . 7 ⊢ (𝐹 “ ∅) = ∅
50	48, 49	eqtri 2226	. . . . . 6 ⊢ (𝐹 “ (^◡𝑁‘0)) = ∅
51	50	a1i 9	. . . . 5 ⊢ (𝜑 → (𝐹 “ (^◡𝑁‘0)) = ∅)
52	34, 37, 51	f1oeq123d 5516	. . . 4 ⊢ (𝜑 → ((𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (^◡𝑁‘0)) ↔ ∅:∅–1-1-onto→∅))
53	26, 52	mpbiri 168	. . 3 ⊢ (𝜑 → (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (^◡𝑁‘0)))
54		simplr 528	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))
55	27	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
56	28	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹:ω–onto→𝐴)
57	29	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
58		simplr 528	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝑘 ∈ ℕ₀)
59	55, 56, 57, 30, 31, 32, 33, 58	ennnfonelemp1 12777	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})))
60	59	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})))
61		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
62	61	iftrued 3578	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = (𝐻‘𝑘))
63	60, 62	eqtrd 2238	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = (𝐻‘𝑘))
64	63	dmeqd 4880	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = dom (𝐻‘𝑘))
65		0zd 9384	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 0 ∈ ℤ)
66	31	frechashgf1o 10573	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑁:ω–1-1-onto→ℕ₀
67	66	a1i 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝑁:ω–1-1-onto→ℕ₀)
68		f1ocnv 5535	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁:ω–1-1-onto→ℕ₀ → ^◡𝑁:ℕ₀–1-1-onto→ω)
69		f1of 5522	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡𝑁:ℕ₀–1-1-onto→ω → ^◡𝑁:ℕ₀⟶ω)
70	67, 68, 69	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ^◡𝑁:ℕ₀⟶ω)
71	70, 58	ffvelcdmd 5716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘𝑘) ∈ ω)
72	65, 31, 71	frec2uzsucd 10546	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = ((𝑁‘(^◡𝑁‘𝑘)) + 1))
73		f1ocnvfv2 5847	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
74	66, 58, 73	sylancr 414	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
75	74	oveq1d 5959	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝑁‘(^◡𝑁‘𝑘)) + 1) = (𝑘 + 1))
76	72, 75	eqtrd 2238	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = (𝑘 + 1))
77	76	fveq2d 5580	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = (^◡𝑁‘(𝑘 + 1)))
78		peano2 4643	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑁‘𝑘) ∈ ω → suc (^◡𝑁‘𝑘) ∈ ω)
79	71, 78	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → suc (^◡𝑁‘𝑘) ∈ ω)
80		f1ocnvfv1 5846	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ suc (^◡𝑁‘𝑘) ∈ ω) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
81	66, 79, 80	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
82	77, 81	eqtr3d 2240	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = suc (^◡𝑁‘𝑘))
83		df-suc 4418	. . . . . . . . . . . . . 14 ⊢ suc (^◡𝑁‘𝑘) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})
84	82, 83	eqtrdi 2254	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)}))
85	84	imaeq2d 5022	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})))
86		imaundi 5095	. . . . . . . . . . . 12 ⊢ (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)}))
87	85, 86	eqtrdi 2254	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
88	87	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
89	61	snssd 3778	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)))
90		ssequn2 3346	. . . . . . . . . . . 12 ⊢ ({(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)) ↔ ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
91	89, 90	sylib 122	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
92		fofn 5500	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ω–onto→𝐴 → 𝐹 Fn ω)
93	56, 92	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹 Fn ω)
94		fnsnfv 5638	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn ω ∧ (^◡𝑁‘𝑘) ∈ ω) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
95	93, 71, 94	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
96	95	uneq2d 3327	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
97	96	eqeq1d 2214	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)) ↔ ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})) = (𝐹 “ (^◡𝑁‘𝑘))))
98	97	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)) ↔ ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})) = (𝐹 “ (^◡𝑁‘𝑘))))
99	91, 98	mpbid 147	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})) = (𝐹 “ (^◡𝑁‘𝑘)))
100	88, 99	eqtrd 2238	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ (^◡𝑁‘𝑘)))
101	63, 64, 100	f1oeq123d 5516	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))) ↔ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))))
102	54, 101	mpbird 167	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))
103		simplr 528	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))
104	55, 56, 57, 30, 31, 32, 33, 58	ennnfonelemom 12779	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
105	104	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
106		fof 5498	. . . . . . . . . . . . . 14 ⊢ (𝐹:ω–onto→𝐴 → 𝐹:ω⟶𝐴)
107	56, 106	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹:ω⟶𝐴)
108	107, 71	ffvelcdmd 5716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
109	108	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
110		f1osng 5563	. . . . . . . . . . 11 ⊢ ((dom (𝐻‘𝑘) ∈ ω ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴) → {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→{(𝐹‘(^◡𝑁‘𝑘))})
111	105, 109, 110	syl2anc 411	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→{(𝐹‘(^◡𝑁‘𝑘))})
112	95	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
113		f1oeq3 5512	. . . . . . . . . . 11 ⊢ ({(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}) → ({⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→{(𝐹‘(^◡𝑁‘𝑘))} ↔ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→(𝐹 “ {(^◡𝑁‘𝑘)})))
114	112, 113	syl 14	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ({⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→{(𝐹‘(^◡𝑁‘𝑘))} ↔ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→(𝐹 “ {(^◡𝑁‘𝑘)})))
115	111, 114	mpbid 147	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→(𝐹 “ {(^◡𝑁‘𝑘)}))
116		nnord 4660	. . . . . . . . . 10 ⊢ (dom (𝐻‘𝑘) ∈ ω → Ord dom (𝐻‘𝑘))
117		orddisj 4594	. . . . . . . . . 10 ⊢ (Ord dom (𝐻‘𝑘) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
118	105, 116, 117	3syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
119	112	ineq2d 3374	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})))
120		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
121		disjsn 3695	. . . . . . . . . . 11 ⊢ (((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅ ↔ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
122	120, 121	sylibr 134	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅)
123	119, 122	eqtr3d 2240	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})) = ∅)
124		f1oun 5542	. . . . . . . . 9 ⊢ ((((𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)) ∧ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→(𝐹 “ {(^◡𝑁‘𝑘)})) ∧ ((dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅ ∧ ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})) = ∅)) → ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}):(dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})–1-1-onto→((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
125	103, 115, 118, 123, 124	syl22anc 1251	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}):(dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})–1-1-onto→((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
126	59	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})))
127	120	iffalsed 3581	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}))
128	126, 127	eqtrd 2238	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}))
129	55	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
130	56	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → 𝐹:ω–onto→𝐴)
131	57	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
132	58	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → 𝑘 ∈ ℕ₀)
133	129, 130, 131, 30, 31, 32, 33, 132, 120	ennnfonelemhdmp1 12780	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = suc dom (𝐻‘𝑘))
134		df-suc 4418	. . . . . . . . . 10 ⊢ suc dom (𝐻‘𝑘) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})
135	133, 134	eqtrdi 2254	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)}))
136	87	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
137	128, 135, 136	f1oeq123d 5516	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))) ↔ ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}):(dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})–1-1-onto→((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)}))))
138	125, 137	mpbird 167	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))
139	55, 56, 71	ennnfonelemdc 12770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
140		exmiddc 838	. . . . . . . 8 ⊢ (DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
141	139, 140	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
142	102, 138, 141	mpjaodan 800	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))
143	142	ex 115	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1)))))
144	143	expcom 116	. . . 4 ⊢ (𝑘 ∈ ℕ₀ → (𝜑 → ((𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))))
145	144	a2d 26	. . 3 ⊢ (𝑘 ∈ ℕ₀ → ((𝜑 → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝜑 → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))))
146	7, 13, 19, 25, 53, 145	nn0ind 9487	. 2 ⊢ (𝑃 ∈ ℕ₀ → (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃))))
147	1, 146	mpcom 36	1 ⊢ (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 DECID wdc 836 = wceq 1373 ⊤wtru 1374 ∈ wcel 2176 ≠ wne 2376 ∀wral 2484 ∃wrex 2485 ∪ cun 3164 ∩ cin 3165 ⊆ wss 3166 ∅c0 3460 ifcif 3571 {csn 3633 ⟨cop 3636 ↦ cmpt 4105 Ord word 4409 suc csuc 4412 ωcom 4638 ^◡ccnv 4674 dom cdm 4675 “ cima 4678 Fn wfn 5266 ⟶wf 5267 –onto→wfo 5269 –1-1-onto→wf1o 5270 ‘cfv 5271 (class class class)co 5944 ∈ cmpo 5946 freccfrec 6476 ↑_pm cpm 6736 0cc0 7925 1c1 7926 + caddc 7928 − cmin 8243 ℕ₀cn0 9295 ℤcz 9372 ℤ_≥cuz 9648 seqcseq 10592

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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-coll 4159 ax-sep 4162 ax-nul 4170 ax-pow 4218 ax-pr 4253 ax-un 4480 ax-setind 4585 ax-iinf 4636 ax-cnex 8016 ax-resscn 8017 ax-1cn 8018 ax-1re 8019 ax-icn 8020 ax-addcl 8021 ax-addrcl 8022 ax-mulcl 8023 ax-addcom 8025 ax-addass 8027 ax-distr 8029 ax-i2m1 8030 ax-0lt1 8031 ax-0id 8033 ax-rnegex 8034 ax-cnre 8036 ax-pre-ltirr 8037 ax-pre-ltwlin 8038 ax-pre-lttrn 8039 ax-pre-ltadd 8041

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-nel 2472 df-ral 2489 df-rex 2490 df-reu 2491 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-if 3572 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-iun 3929 df-br 4045 df-opab 4106 df-mpt 4107 df-tr 4143 df-id 4340 df-iord 4413 df-on 4415 df-ilim 4416 df-suc 4418 df-iom 4639 df-xp 4681 df-rel 4682 df-cnv 4683 df-co 4684 df-dm 4685 df-rn 4686 df-res 4687 df-ima 4688 df-iota 5232 df-fun 5273 df-fn 5274 df-f 5275 df-f1 5276 df-fo 5277 df-f1o 5278 df-fv 5279 df-riota 5899 df-ov 5947 df-oprab 5948 df-mpo 5949 df-1st 6226 df-2nd 6227 df-recs 6391 df-frec 6477 df-pm 6738 df-pnf 8109 df-mnf 8110 df-xr 8111 df-ltxr 8112 df-le 8113 df-sub 8245 df-neg 8246 df-inn 9037 df-n0 9296 df-z 9373 df-uz 9649 df-seqfrec 10593

This theorem is referenced by: ennnfonelemex 12785 ennnfonelemf1 12789 ennnfonelemrn 12790

W3C validator