ennnfonelemhf1o - Intuitionistic Logic Explorer

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

Theorem ennnfonelemhf1o 12630

Description: Lemma for ennnfone 12642. 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 5558	. . . . 5 ⊢ (𝑤 = 0 → (𝐻‘𝑤) = (𝐻‘0))
3	2	dmeqd 4868	. . . . 5 ⊢ (𝑤 = 0 → dom (𝐻‘𝑤) = dom (𝐻‘0))
4		fveq2 5558	. . . . . 6 ⊢ (𝑤 = 0 → (^◡𝑁‘𝑤) = (^◡𝑁‘0))
5	4	imaeq2d 5009	. . . . 5 ⊢ (𝑤 = 0 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘0)))
6	2, 3, 5	f1oeq123d 5498	. . . 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 5558	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐻‘𝑤) = (𝐻‘𝑘))
9	8	dmeqd 4868	. . . . 5 ⊢ (𝑤 = 𝑘 → dom (𝐻‘𝑤) = dom (𝐻‘𝑘))
10		fveq2 5558	. . . . . 6 ⊢ (𝑤 = 𝑘 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑘))
11	10	imaeq2d 5009	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑘)))
12	8, 9, 11	f1oeq123d 5498	. . . 4 ⊢ (𝑤 = 𝑘 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))))
13	12	imbi2d 230	. . 3 ⊢ (𝑤 = 𝑘 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))))
14		fveq2 5558	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐻‘𝑤) = (𝐻‘(𝑘 + 1)))
15	14	dmeqd 4868	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → dom (𝐻‘𝑤) = dom (𝐻‘(𝑘 + 1)))
16		fveq2 5558	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → (^◡𝑁‘𝑤) = (^◡𝑁‘(𝑘 + 1)))
17	16	imaeq2d 5009	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘(𝑘 + 1))))
18	14, 15, 17	f1oeq123d 5498	. . . 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 5558	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐻‘𝑤) = (𝐻‘𝑃))
21	20	dmeqd 4868	. . . . 5 ⊢ (𝑤 = 𝑃 → dom (𝐻‘𝑤) = dom (𝐻‘𝑃))
22		fveq2 5558	. . . . . 6 ⊢ (𝑤 = 𝑃 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑃))
23	22	imaeq2d 5009	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑃)))
24	20, 21, 23	f1oeq123d 5498	. . . 4 ⊢ (𝑤 = 𝑃 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃))))
25	24	imbi2d 230	. . 3 ⊢ (𝑤 = 𝑃 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃)))))
26		f1o0 5541	. . . 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 12622	. . . . 5 ⊢ (𝜑 → (𝐻‘0) = ∅)
35	34	dmeqd 4868	. . . . . 6 ⊢ (𝜑 → dom (𝐻‘0) = dom ∅)
36		dm0 4880	. . . . . 6 ⊢ dom ∅ = ∅
37	35, 36	eqtrdi 2245	. . . . 5 ⊢ (𝜑 → dom (𝐻‘0) = ∅)
38		0zd 9338	. . . . . . . . . . . 12 ⊢ (⊤ → 0 ∈ ℤ)
39	38, 31	frec2uz0d 10491	. . . . . . . . . . 11 ⊢ (⊤ → (𝑁‘∅) = 0)
40	39	mptru 1373	. . . . . . . . . 10 ⊢ (𝑁‘∅) = 0
41	40	fveq2i 5561	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = (^◡𝑁‘0)
42	38, 31	frec2uzf1od 10498	. . . . . . . . . . 11 ⊢ (⊤ → 𝑁:ω–1-1-onto→(ℤ_≥‘0))
43	42	mptru 1373	. . . . . . . . . 10 ⊢ 𝑁:ω–1-1-onto→(ℤ_≥‘0)
44		peano1 4630	. . . . . . . . . 10 ⊢ ∅ ∈ ω
45		f1ocnvfv1 5824	. . . . . . . . . 10 ⊢ ((𝑁:ω–1-1-onto→(ℤ_≥‘0) ∧ ∅ ∈ ω) → (^◡𝑁‘(𝑁‘∅)) = ∅)
46	43, 44, 45	mp2an 426	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = ∅
47	41, 46	eqtr3i 2219	. . . . . . . 8 ⊢ (^◡𝑁‘0) = ∅
48	47	imaeq2i 5007	. . . . . . 7 ⊢ (𝐹 “ (^◡𝑁‘0)) = (𝐹 “ ∅)
49		ima0 5028	. . . . . . 7 ⊢ (𝐹 “ ∅) = ∅
50	48, 49	eqtri 2217	. . . . . 6 ⊢ (𝐹 “ (^◡𝑁‘0)) = ∅
51	50	a1i 9	. . . . 5 ⊢ (𝜑 → (𝐹 “ (^◡𝑁‘0)) = ∅)
52	34, 37, 51	f1oeq123d 5498	. . . 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 12623	. . . . . . . . . . 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 3568	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = (𝐻‘𝑘))
63	60, 62	eqtrd 2229	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = (𝐻‘𝑘))
64	63	dmeqd 4868	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = dom (𝐻‘𝑘))
65		0zd 9338	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 0 ∈ ℤ)
66	31	frechashgf1o 10520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑁:ω–1-1-onto→ℕ₀
67	66	a1i 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝑁:ω–1-1-onto→ℕ₀)
68		f1ocnv 5517	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁:ω–1-1-onto→ℕ₀ → ^◡𝑁:ℕ₀–1-1-onto→ω)
69		f1of 5504	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡𝑁:ℕ₀–1-1-onto→ω → ^◡𝑁:ℕ₀⟶ω)
70	67, 68, 69	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ^◡𝑁:ℕ₀⟶ω)
71	70, 58	ffvelcdmd 5698	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘𝑘) ∈ ω)
72	65, 31, 71	frec2uzsucd 10493	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = ((𝑁‘(^◡𝑁‘𝑘)) + 1))
73		f1ocnvfv2 5825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
74	66, 58, 73	sylancr 414	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
75	74	oveq1d 5937	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝑁‘(^◡𝑁‘𝑘)) + 1) = (𝑘 + 1))
76	72, 75	eqtrd 2229	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = (𝑘 + 1))
77	76	fveq2d 5562	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = (^◡𝑁‘(𝑘 + 1)))
78		peano2 4631	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑁‘𝑘) ∈ ω → suc (^◡𝑁‘𝑘) ∈ ω)
79	71, 78	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → suc (^◡𝑁‘𝑘) ∈ ω)
80		f1ocnvfv1 5824	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ suc (^◡𝑁‘𝑘) ∈ ω) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
81	66, 79, 80	sylancr 414	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
82	77, 81	eqtr3d 2231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = suc (^◡𝑁‘𝑘))
83		df-suc 4406	. . . . . . . . . . . . . 14 ⊢ suc (^◡𝑁‘𝑘) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})
84	82, 83	eqtrdi 2245	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)}))
85	84	imaeq2d 5009	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})))
86		imaundi 5082	. . . . . . . . . . . 12 ⊢ (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)}))
87	85, 86	eqtrdi 2245	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
88	87	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
89	61	snssd 3767	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)))
90		ssequn2 3336	. . . . . . . . . . . 12 ⊢ ({(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)) ↔ ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
91	89, 90	sylib 122	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
92		fofn 5482	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ω–onto→𝐴 → 𝐹 Fn ω)
93	56, 92	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹 Fn ω)
94		fnsnfv 5620	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn ω ∧ (^◡𝑁‘𝑘) ∈ ω) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
95	93, 71, 94	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
96	95	uneq2d 3317	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
97	96	eqeq1d 2205	. . . . . . . . . . . 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 2229	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ (^◡𝑁‘𝑘)))
101	63, 64, 100	f1oeq123d 5498	. . . . . . . 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 12625	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
105	104	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
106		fof 5480	. . . . . . . . . . . . . 14 ⊢ (𝐹:ω–onto→𝐴 → 𝐹:ω⟶𝐴)
107	56, 106	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹:ω⟶𝐴)
108	107, 71	ffvelcdmd 5698	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
109	108	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
110		f1osng 5545	. . . . . . . . . . 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 5494	. . . . . . . . . . 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 4648	. . . . . . . . . 10 ⊢ (dom (𝐻‘𝑘) ∈ ω → Ord dom (𝐻‘𝑘))
117		orddisj 4582	. . . . . . . . . 10 ⊢ (Ord dom (𝐻‘𝑘) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
118	105, 116, 117	3syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
119	112	ineq2d 3364	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})))
120		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
121		disjsn 3684	. . . . . . . . . . 11 ⊢ (((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅ ↔ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
122	120, 121	sylibr 134	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅)
123	119, 122	eqtr3d 2231	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})) = ∅)
124		f1oun 5524	. . . . . . . . 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 1250	. . . . . . . 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 3571	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}))
128	126, 127	eqtrd 2229	. . . . . . . . 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 12626	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = suc dom (𝐻‘𝑘))
134		df-suc 4406	. . . . . . . . . 10 ⊢ suc dom (𝐻‘𝑘) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})
135	133, 134	eqtrdi 2245	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)}))
136	87	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
137	128, 135, 136	f1oeq123d 5498	. . . . . . . 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 12616	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
140		exmiddc 837	. . . . . . . 8 ⊢ (DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
141	139, 140	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
142	102, 138, 141	mpjaodan 799	. . . . . 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 9440	. 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 709 DECID wdc 835 = wceq 1364 ⊤wtru 1365 ∈ wcel 2167 ≠ wne 2367 ∀wral 2475 ∃wrex 2476 ∪ cun 3155 ∩ cin 3156 ⊆ wss 3157 ∅c0 3450 ifcif 3561 {csn 3622 ⟨cop 3625 ↦ cmpt 4094 Ord word 4397 suc csuc 4400 ωcom 4626 ^◡ccnv 4662 dom cdm 4663 “ cima 4666 Fn wfn 5253 ⟶wf 5254 –onto→wfo 5256 –1-1-onto→wf1o 5257 ‘cfv 5258 (class class class)co 5922 ∈ cmpo 5924 freccfrec 6448 ↑_pm cpm 6708 0cc0 7879 1c1 7880 + caddc 7882 − cmin 8197 ℕ₀cn0 9249 ℤcz 9326 ℤ_≥cuz 9601 seqcseq 10539

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 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-addcom 7979 ax-addass 7981 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-0id 7987 ax-rnegex 7988 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-ltadd 7995

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-frec 6449 df-pm 6710 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-inn 8991 df-n0 9250 df-z 9327 df-uz 9602 df-seqfrec 10540

This theorem is referenced by: ennnfonelemex 12631 ennnfonelemf1 12635 ennnfonelemrn 12636

W3C validator