ennnfonelemhf1o - Intuitionistic Logic Explorer

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

Theorem ennnfonelemhf1o 13164

Description: Lemma for ennnfone 13176. 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 5670	. . . . 5 ⊢ (𝑤 = 0 → (𝐻‘𝑤) = (𝐻‘0))
3	2	dmeqd 4958	. . . . 5 ⊢ (𝑤 = 0 → dom (𝐻‘𝑤) = dom (𝐻‘0))
4		fveq2 5670	. . . . . 6 ⊢ (𝑤 = 0 → (^◡𝑁‘𝑤) = (^◡𝑁‘0))
5	4	imaeq2d 5101	. . . . 5 ⊢ (𝑤 = 0 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘0)))
6	2, 3, 5	f1oeq123d 5608	. . . 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 5670	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐻‘𝑤) = (𝐻‘𝑘))
9	8	dmeqd 4958	. . . . 5 ⊢ (𝑤 = 𝑘 → dom (𝐻‘𝑤) = dom (𝐻‘𝑘))
10		fveq2 5670	. . . . . 6 ⊢ (𝑤 = 𝑘 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑘))
11	10	imaeq2d 5101	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑘)))
12	8, 9, 11	f1oeq123d 5608	. . . 4 ⊢ (𝑤 = 𝑘 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))))
13	12	imbi2d 230	. . 3 ⊢ (𝑤 = 𝑘 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))))
14		fveq2 5670	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐻‘𝑤) = (𝐻‘(𝑘 + 1)))
15	14	dmeqd 4958	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → dom (𝐻‘𝑤) = dom (𝐻‘(𝑘 + 1)))
16		fveq2 5670	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → (^◡𝑁‘𝑤) = (^◡𝑁‘(𝑘 + 1)))
17	16	imaeq2d 5101	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘(𝑘 + 1))))
18	14, 15, 17	f1oeq123d 5608	. . . 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 5670	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐻‘𝑤) = (𝐻‘𝑃))
21	20	dmeqd 4958	. . . . 5 ⊢ (𝑤 = 𝑃 → dom (𝐻‘𝑤) = dom (𝐻‘𝑃))
22		fveq2 5670	. . . . . 6 ⊢ (𝑤 = 𝑃 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑃))
23	22	imaeq2d 5101	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑃)))
24	20, 21, 23	f1oeq123d 5608	. . . 4 ⊢ (𝑤 = 𝑃 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃))))
25	24	imbi2d 230	. . 3 ⊢ (𝑤 = 𝑃 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃)))))
26		f1o0 5653	. . . 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 13156	. . . . 5 ⊢ (𝜑 → (𝐻‘0) = ∅)
35	34	dmeqd 4958	. . . . . 6 ⊢ (𝜑 → dom (𝐻‘0) = dom ∅)
36		dm0 4970	. . . . . 6 ⊢ dom ∅ = ∅
37	35, 36	eqtrdi 2281	. . . . 5 ⊢ (𝜑 → dom (𝐻‘0) = ∅)
38		0zd 9589	. . . . . . . . . . . 12 ⊢ (⊤ → 0 ∈ ℤ)
39	38, 31	frec2uz0d 10761	. . . . . . . . . . 11 ⊢ (⊤ → (𝑁‘∅) = 0)
40	39	mptru 1407	. . . . . . . . . 10 ⊢ (𝑁‘∅) = 0
41	40	fveq2i 5673	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = (^◡𝑁‘0)
42	38, 31	frec2uzf1od 10768	. . . . . . . . . . 11 ⊢ (⊤ → 𝑁:ω–1-1-onto→(ℤ_≥‘0))
43	42	mptru 1407	. . . . . . . . . 10 ⊢ 𝑁:ω–1-1-onto→(ℤ_≥‘0)
44		peano1 4716	. . . . . . . . . 10 ⊢ ∅ ∈ ω
45		f1ocnvfv1 5950	. . . . . . . . . 10 ⊢ ((𝑁:ω–1-1-onto→(ℤ_≥‘0) ∧ ∅ ∈ ω) → (^◡𝑁‘(𝑁‘∅)) = ∅)
46	43, 44, 45	mp2an 426	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = ∅
47	41, 46	eqtr3i 2255	. . . . . . . 8 ⊢ (^◡𝑁‘0) = ∅
48	47	imaeq2i 5099	. . . . . . 7 ⊢ (𝐹 “ (^◡𝑁‘0)) = (𝐹 “ ∅)
49		ima0 5121	. . . . . . 7 ⊢ (𝐹 “ ∅) = ∅
50	48, 49	eqtri 2253	. . . . . 6 ⊢ (𝐹 “ (^◡𝑁‘0)) = ∅
51	50	a1i 9	. . . . 5 ⊢ (𝜑 → (𝐹 “ (^◡𝑁‘0)) = ∅)
52	34, 37, 51	f1oeq123d 5608	. . . 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 529	. . . . . . . 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 529	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝑘 ∈ ℕ₀)
59	55, 56, 57, 30, 31, 32, 33, 58	ennnfonelemp1 13157	. . . . . . . . . . 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 3629	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = (𝐻‘𝑘))
63	60, 62	eqtrd 2265	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = (𝐻‘𝑘))
64	63	dmeqd 4958	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = dom (𝐻‘𝑘))
65		0zd 9589	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 0 ∈ ℤ)
66	31	frechashgf1o 10790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑁:ω–1-1-onto→ℕ₀
67	66	a1i 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝑁:ω–1-1-onto→ℕ₀)
68		f1ocnv 5627	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁:ω–1-1-onto→ℕ₀ → ^◡𝑁:ℕ₀–1-1-onto→ω)
69		f1of 5614	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡𝑁:ℕ₀–1-1-onto→ω → ^◡𝑁:ℕ₀⟶ω)
70	67, 68, 69	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ^◡𝑁:ℕ₀⟶ω)
71	70, 58	ffvelcdmd 5813	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘𝑘) ∈ ω)
72	65, 31, 71	frec2uzsucd 10763	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = ((𝑁‘(^◡𝑁‘𝑘)) + 1))
73		f1ocnvfv2 5951	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
74	66, 58, 73	sylancr 414	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
75	74	oveq1d 6065	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝑁‘(^◡𝑁‘𝑘)) + 1) = (𝑘 + 1))
76	72, 75	eqtrd 2265	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = (𝑘 + 1))
77	76	fveq2d 5674	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = (^◡𝑁‘(𝑘 + 1)))
78		peano2 4717	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑁‘𝑘) ∈ ω → suc (^◡𝑁‘𝑘) ∈ ω)
79	71, 78	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → suc (^◡𝑁‘𝑘) ∈ ω)
80		f1ocnvfv1 5950	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ suc (^◡𝑁‘𝑘) ∈ ω) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
81	66, 79, 80	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
82	77, 81	eqtr3d 2267	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = suc (^◡𝑁‘𝑘))
83		df-suc 4492	. . . . . . . . . . . . . 14 ⊢ suc (^◡𝑁‘𝑘) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})
84	82, 83	eqtrdi 2281	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)}))
85	84	imaeq2d 5101	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})))
86		imaundi 5175	. . . . . . . . . . . 12 ⊢ (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)}))
87	85, 86	eqtrdi 2281	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
88	87	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
89	61	snssd 3839	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)))
90		ssequn2 3392	. . . . . . . . . . . 12 ⊢ ({(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)) ↔ ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
91	89, 90	sylib 122	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
92		fofn 5592	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ω–onto→𝐴 → 𝐹 Fn ω)
93	56, 92	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹 Fn ω)
94		fnsnfv 5736	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn ω ∧ (^◡𝑁‘𝑘) ∈ ω) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
95	93, 71, 94	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
96	95	uneq2d 3373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
97	96	eqeq1d 2241	. . . . . . . . . . . 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 2265	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ (^◡𝑁‘𝑘)))
101	63, 64, 100	f1oeq123d 5608	. . . . . . . 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 529	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))
104	55, 56, 57, 30, 31, 32, 33, 58	ennnfonelemom 13159	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
105	104	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
106		fof 5590	. . . . . . . . . . . . . 14 ⊢ (𝐹:ω–onto→𝐴 → 𝐹:ω⟶𝐴)
107	56, 106	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹:ω⟶𝐴)
108	107, 71	ffvelcdmd 5813	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
109	108	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
110		f1osng 5657	. . . . . . . . . . 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 5604	. . . . . . . . . . 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 4734	. . . . . . . . . 10 ⊢ (dom (𝐻‘𝑘) ∈ ω → Ord dom (𝐻‘𝑘))
117		orddisj 4668	. . . . . . . . . 10 ⊢ (Ord dom (𝐻‘𝑘) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
118	105, 116, 117	3syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
119	112	ineq2d 3422	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})))
120		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
121		disjsn 3751	. . . . . . . . . . 11 ⊢ (((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅ ↔ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
122	120, 121	sylibr 134	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅)
123	119, 122	eqtr3d 2267	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})) = ∅)
124		f1oun 5634	. . . . . . . . 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 1275	. . . . . . . 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 3632	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}))
128	126, 127	eqtrd 2265	. . . . . . . . 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 13160	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = suc dom (𝐻‘𝑘))
134		df-suc 4492	. . . . . . . . . 10 ⊢ suc dom (𝐻‘𝑘) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})
135	133, 134	eqtrdi 2281	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)}))
136	87	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
137	128, 135, 136	f1oeq123d 5608	. . . . . . . 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 13150	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
140		exmiddc 844	. . . . . . . 8 ⊢ (DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
141	139, 140	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
142	102, 138, 141	mpjaodan 806	. . . . . 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 9692	. 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 716 DECID wdc 842 = wceq 1398 ⊤wtru 1399 ∈ wcel 2203 ≠ wne 2412 ∀wral 2520 ∃wrex 2521 ∪ cun 3209 ∩ cin 3210 ⊆ wss 3211 ∅c0 3508 ifcif 3620 {csn 3689 ⟨cop 3692 ↦ cmpt 4171 Ord word 4483 suc csuc 4486 ωcom 4712 ^◡ccnv 4748 dom cdm 4749 “ cima 4752 Fn wfn 5347 ⟶wf 5348 –onto→wfo 5350 –1-1-onto→wf1o 5351 ‘cfv 5352 (class class class)co 6050 ∈ cmpo 6052 freccfrec 6621 ↑_pm cpm 6883 0cc0 8127 1c1 8128 + caddc 8130 − cmin 8444 ℕ₀cn0 9496 ℤcz 9577 ℤ_≥cuz 9853 seqcseq 10809

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-coll 4225 ax-sep 4228 ax-nul 4236 ax-pow 4287 ax-pr 4322 ax-un 4554 ax-setind 4659 ax-iinf 4710 ax-cnex 8218 ax-resscn 8219 ax-1cn 8220 ax-1re 8221 ax-icn 8222 ax-addcl 8223 ax-addrcl 8224 ax-mulcl 8225 ax-addcom 8227 ax-addass 8229 ax-distr 8231 ax-i2m1 8232 ax-0lt1 8233 ax-0id 8235 ax-rnegex 8236 ax-cnre 8238 ax-pre-ltirr 8239 ax-pre-ltwlin 8240 ax-pre-lttrn 8241 ax-pre-ltadd 8243

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rab 2529 df-v 2815 df-sbc 3043 df-csb 3139 df-dif 3213 df-un 3215 df-in 3217 df-ss 3224 df-nul 3509 df-if 3621 df-pw 3671 df-sn 3695 df-pr 3696 df-op 3698 df-uni 3915 df-int 3950 df-iun 3993 df-br 4110 df-opab 4172 df-mpt 4173 df-tr 4209 df-id 4414 df-iord 4487 df-on 4489 df-ilim 4490 df-suc 4492 df-iom 4713 df-xp 4755 df-rel 4756 df-cnv 4757 df-co 4758 df-dm 4759 df-rn 4760 df-res 4761 df-ima 4762 df-iota 5312 df-fun 5354 df-fn 5355 df-f 5356 df-f1 5357 df-fo 5358 df-f1o 5359 df-fv 5360 df-riota 6003 df-ov 6053 df-oprab 6054 df-mpo 6055 df-1st 6334 df-2nd 6335 df-recs 6536 df-frec 6622 df-pm 6885 df-pnf 8310 df-mnf 8311 df-xr 8312 df-ltxr 8313 df-le 8314 df-sub 8446 df-neg 8447 df-inn 9238 df-n0 9497 df-z 9578 df-uz 9854 df-seqfrec 10810

This theorem is referenced by: ennnfonelemex 13165 ennnfonelemf1 13169 ennnfonelemrn 13170

W3C validator