ennnfonelemhf1o - Intuitionistic Logic Explorer

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

Theorem ennnfonelemhf1o 12984

Description: Lemma for ennnfone 12996. 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 5627	. . . . 5 ⊢ (𝑤 = 0 → (𝐻‘𝑤) = (𝐻‘0))
3	2	dmeqd 4925	. . . . 5 ⊢ (𝑤 = 0 → dom (𝐻‘𝑤) = dom (𝐻‘0))
4		fveq2 5627	. . . . . 6 ⊢ (𝑤 = 0 → (^◡𝑁‘𝑤) = (^◡𝑁‘0))
5	4	imaeq2d 5068	. . . . 5 ⊢ (𝑤 = 0 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘0)))
6	2, 3, 5	f1oeq123d 5566	. . . 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 5627	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐻‘𝑤) = (𝐻‘𝑘))
9	8	dmeqd 4925	. . . . 5 ⊢ (𝑤 = 𝑘 → dom (𝐻‘𝑤) = dom (𝐻‘𝑘))
10		fveq2 5627	. . . . . 6 ⊢ (𝑤 = 𝑘 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑘))
11	10	imaeq2d 5068	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑘)))
12	8, 9, 11	f1oeq123d 5566	. . . 4 ⊢ (𝑤 = 𝑘 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))))
13	12	imbi2d 230	. . 3 ⊢ (𝑤 = 𝑘 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))))
14		fveq2 5627	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐻‘𝑤) = (𝐻‘(𝑘 + 1)))
15	14	dmeqd 4925	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → dom (𝐻‘𝑤) = dom (𝐻‘(𝑘 + 1)))
16		fveq2 5627	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → (^◡𝑁‘𝑤) = (^◡𝑁‘(𝑘 + 1)))
17	16	imaeq2d 5068	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘(𝑘 + 1))))
18	14, 15, 17	f1oeq123d 5566	. . . 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 5627	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐻‘𝑤) = (𝐻‘𝑃))
21	20	dmeqd 4925	. . . . 5 ⊢ (𝑤 = 𝑃 → dom (𝐻‘𝑤) = dom (𝐻‘𝑃))
22		fveq2 5627	. . . . . 6 ⊢ (𝑤 = 𝑃 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑃))
23	22	imaeq2d 5068	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑃)))
24	20, 21, 23	f1oeq123d 5566	. . . 4 ⊢ (𝑤 = 𝑃 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃))))
25	24	imbi2d 230	. . 3 ⊢ (𝑤 = 𝑃 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃)))))
26		f1o0 5610	. . . 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 12976	. . . . 5 ⊢ (𝜑 → (𝐻‘0) = ∅)
35	34	dmeqd 4925	. . . . . 6 ⊢ (𝜑 → dom (𝐻‘0) = dom ∅)
36		dm0 4937	. . . . . 6 ⊢ dom ∅ = ∅
37	35, 36	eqtrdi 2278	. . . . 5 ⊢ (𝜑 → dom (𝐻‘0) = ∅)
38		0zd 9458	. . . . . . . . . . . 12 ⊢ (⊤ → 0 ∈ ℤ)
39	38, 31	frec2uz0d 10621	. . . . . . . . . . 11 ⊢ (⊤ → (𝑁‘∅) = 0)
40	39	mptru 1404	. . . . . . . . . 10 ⊢ (𝑁‘∅) = 0
41	40	fveq2i 5630	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = (^◡𝑁‘0)
42	38, 31	frec2uzf1od 10628	. . . . . . . . . . 11 ⊢ (⊤ → 𝑁:ω–1-1-onto→(ℤ_≥‘0))
43	42	mptru 1404	. . . . . . . . . 10 ⊢ 𝑁:ω–1-1-onto→(ℤ_≥‘0)
44		peano1 4686	. . . . . . . . . 10 ⊢ ∅ ∈ ω
45		f1ocnvfv1 5901	. . . . . . . . . 10 ⊢ ((𝑁:ω–1-1-onto→(ℤ_≥‘0) ∧ ∅ ∈ ω) → (^◡𝑁‘(𝑁‘∅)) = ∅)
46	43, 44, 45	mp2an 426	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = ∅
47	41, 46	eqtr3i 2252	. . . . . . . 8 ⊢ (^◡𝑁‘0) = ∅
48	47	imaeq2i 5066	. . . . . . 7 ⊢ (𝐹 “ (^◡𝑁‘0)) = (𝐹 “ ∅)
49		ima0 5087	. . . . . . 7 ⊢ (𝐹 “ ∅) = ∅
50	48, 49	eqtri 2250	. . . . . 6 ⊢ (𝐹 “ (^◡𝑁‘0)) = ∅
51	50	a1i 9	. . . . 5 ⊢ (𝜑 → (𝐹 “ (^◡𝑁‘0)) = ∅)
52	34, 37, 51	f1oeq123d 5566	. . . 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 12977	. . . . . . . . . . 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 3609	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = (𝐻‘𝑘))
63	60, 62	eqtrd 2262	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = (𝐻‘𝑘))
64	63	dmeqd 4925	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = dom (𝐻‘𝑘))
65		0zd 9458	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 0 ∈ ℤ)
66	31	frechashgf1o 10650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑁:ω–1-1-onto→ℕ₀
67	66	a1i 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝑁:ω–1-1-onto→ℕ₀)
68		f1ocnv 5585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁:ω–1-1-onto→ℕ₀ → ^◡𝑁:ℕ₀–1-1-onto→ω)
69		f1of 5572	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡𝑁:ℕ₀–1-1-onto→ω → ^◡𝑁:ℕ₀⟶ω)
70	67, 68, 69	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ^◡𝑁:ℕ₀⟶ω)
71	70, 58	ffvelcdmd 5771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘𝑘) ∈ ω)
72	65, 31, 71	frec2uzsucd 10623	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = ((𝑁‘(^◡𝑁‘𝑘)) + 1))
73		f1ocnvfv2 5902	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
74	66, 58, 73	sylancr 414	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
75	74	oveq1d 6016	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝑁‘(^◡𝑁‘𝑘)) + 1) = (𝑘 + 1))
76	72, 75	eqtrd 2262	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = (𝑘 + 1))
77	76	fveq2d 5631	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = (^◡𝑁‘(𝑘 + 1)))
78		peano2 4687	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑁‘𝑘) ∈ ω → suc (^◡𝑁‘𝑘) ∈ ω)
79	71, 78	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → suc (^◡𝑁‘𝑘) ∈ ω)
80		f1ocnvfv1 5901	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ suc (^◡𝑁‘𝑘) ∈ ω) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
81	66, 79, 80	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
82	77, 81	eqtr3d 2264	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = suc (^◡𝑁‘𝑘))
83		df-suc 4462	. . . . . . . . . . . . . 14 ⊢ suc (^◡𝑁‘𝑘) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})
84	82, 83	eqtrdi 2278	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)}))
85	84	imaeq2d 5068	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})))
86		imaundi 5141	. . . . . . . . . . . 12 ⊢ (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)}))
87	85, 86	eqtrdi 2278	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
88	87	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
89	61	snssd 3813	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)))
90		ssequn2 3377	. . . . . . . . . . . 12 ⊢ ({(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)) ↔ ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
91	89, 90	sylib 122	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
92		fofn 5550	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ω–onto→𝐴 → 𝐹 Fn ω)
93	56, 92	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹 Fn ω)
94		fnsnfv 5693	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn ω ∧ (^◡𝑁‘𝑘) ∈ ω) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
95	93, 71, 94	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
96	95	uneq2d 3358	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
97	96	eqeq1d 2238	. . . . . . . . . . . 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 2262	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ (^◡𝑁‘𝑘)))
101	63, 64, 100	f1oeq123d 5566	. . . . . . . 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 12979	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
105	104	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
106		fof 5548	. . . . . . . . . . . . . 14 ⊢ (𝐹:ω–onto→𝐴 → 𝐹:ω⟶𝐴)
107	56, 106	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹:ω⟶𝐴)
108	107, 71	ffvelcdmd 5771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
109	108	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
110		f1osng 5614	. . . . . . . . . . 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 5562	. . . . . . . . . . 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 4704	. . . . . . . . . 10 ⊢ (dom (𝐻‘𝑘) ∈ ω → Ord dom (𝐻‘𝑘))
117		orddisj 4638	. . . . . . . . . 10 ⊢ (Ord dom (𝐻‘𝑘) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
118	105, 116, 117	3syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
119	112	ineq2d 3405	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})))
120		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
121		disjsn 3728	. . . . . . . . . . 11 ⊢ (((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅ ↔ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
122	120, 121	sylibr 134	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅)
123	119, 122	eqtr3d 2264	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})) = ∅)
124		f1oun 5592	. . . . . . . . 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 1272	. . . . . . . 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 3612	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}))
128	126, 127	eqtrd 2262	. . . . . . . . 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 12980	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = suc dom (𝐻‘𝑘))
134		df-suc 4462	. . . . . . . . . 10 ⊢ suc dom (𝐻‘𝑘) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})
135	133, 134	eqtrdi 2278	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)}))
136	87	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
137	128, 135, 136	f1oeq123d 5566	. . . . . . . 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 12970	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
140		exmiddc 841	. . . . . . . 8 ⊢ (DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
141	139, 140	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
142	102, 138, 141	mpjaodan 803	. . . . . 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 9561	. 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 713 DECID wdc 839 = wceq 1395 ⊤wtru 1396 ∈ wcel 2200 ≠ wne 2400 ∀wral 2508 ∃wrex 2509 ∪ cun 3195 ∩ cin 3196 ⊆ wss 3197 ∅c0 3491 ifcif 3602 {csn 3666 ⟨cop 3669 ↦ cmpt 4145 Ord word 4453 suc csuc 4456 ωcom 4682 ^◡ccnv 4718 dom cdm 4719 “ cima 4722 Fn wfn 5313 ⟶wf 5314 –onto→wfo 5316 –1-1-onto→wf1o 5317 ‘cfv 5318 (class class class)co 6001 ∈ cmpo 6003 freccfrec 6536 ↑_pm cpm 6796 0cc0 7999 1c1 8000 + caddc 8002 − cmin 8317 ℕ₀cn0 9369 ℤcz 9446 ℤ_≥cuz 9722 seqcseq 10669

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4199 ax-sep 4202 ax-nul 4210 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629 ax-iinf 4680 ax-cnex 8090 ax-resscn 8091 ax-1cn 8092 ax-1re 8093 ax-icn 8094 ax-addcl 8095 ax-addrcl 8096 ax-mulcl 8097 ax-addcom 8099 ax-addass 8101 ax-distr 8103 ax-i2m1 8104 ax-0lt1 8105 ax-0id 8107 ax-rnegex 8108 ax-cnre 8110 ax-pre-ltirr 8111 ax-pre-ltwlin 8112 ax-pre-lttrn 8113 ax-pre-ltadd 8115

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-tr 4183 df-id 4384 df-iord 4457 df-on 4459 df-ilim 4460 df-suc 4462 df-iom 4683 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-riota 5954 df-ov 6004 df-oprab 6005 df-mpo 6006 df-1st 6286 df-2nd 6287 df-recs 6451 df-frec 6537 df-pm 6798 df-pnf 8183 df-mnf 8184 df-xr 8185 df-ltxr 8186 df-le 8187 df-sub 8319 df-neg 8320 df-inn 9111 df-n0 9370 df-z 9447 df-uz 9723 df-seqfrec 10670

This theorem is referenced by: ennnfonelemex 12985 ennnfonelemf1 12989 ennnfonelemrn 12990

W3C validator