ennnfonelemhf1o - Intuitionistic Logic Explorer

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

Theorem ennnfonelemhf1o 12346

Description: Lemma for ennnfone 12358. 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 5486	. . . . 5 ⊢ (𝑤 = 0 → (𝐻‘𝑤) = (𝐻‘0))
3	2	dmeqd 4806	. . . . 5 ⊢ (𝑤 = 0 → dom (𝐻‘𝑤) = dom (𝐻‘0))
4		fveq2 5486	. . . . . 6 ⊢ (𝑤 = 0 → (^◡𝑁‘𝑤) = (^◡𝑁‘0))
5	4	imaeq2d 4946	. . . . 5 ⊢ (𝑤 = 0 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘0)))
6	2, 3, 5	f1oeq123d 5427	. . . 4 ⊢ (𝑤 = 0 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (^◡𝑁‘0))))
7	6	imbi2d 229	. . 3 ⊢ (𝑤 = 0 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (^◡𝑁‘0)))))
8		fveq2 5486	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐻‘𝑤) = (𝐻‘𝑘))
9	8	dmeqd 4806	. . . . 5 ⊢ (𝑤 = 𝑘 → dom (𝐻‘𝑤) = dom (𝐻‘𝑘))
10		fveq2 5486	. . . . . 6 ⊢ (𝑤 = 𝑘 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑘))
11	10	imaeq2d 4946	. . . . 5 ⊢ (𝑤 = 𝑘 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑘)))
12	8, 9, 11	f1oeq123d 5427	. . . 4 ⊢ (𝑤 = 𝑘 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))))
13	12	imbi2d 229	. . 3 ⊢ (𝑤 = 𝑘 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))))
14		fveq2 5486	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐻‘𝑤) = (𝐻‘(𝑘 + 1)))
15	14	dmeqd 4806	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → dom (𝐻‘𝑤) = dom (𝐻‘(𝑘 + 1)))
16		fveq2 5486	. . . . . 6 ⊢ (𝑤 = (𝑘 + 1) → (^◡𝑁‘𝑤) = (^◡𝑁‘(𝑘 + 1)))
17	16	imaeq2d 4946	. . . . 5 ⊢ (𝑤 = (𝑘 + 1) → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘(𝑘 + 1))))
18	14, 15, 17	f1oeq123d 5427	. . . 4 ⊢ (𝑤 = (𝑘 + 1) → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1)))))
19	18	imbi2d 229	. . 3 ⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))))
20		fveq2 5486	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐻‘𝑤) = (𝐻‘𝑃))
21	20	dmeqd 4806	. . . . 5 ⊢ (𝑤 = 𝑃 → dom (𝐻‘𝑤) = dom (𝐻‘𝑃))
22		fveq2 5486	. . . . . 6 ⊢ (𝑤 = 𝑃 → (^◡𝑁‘𝑤) = (^◡𝑁‘𝑃))
23	22	imaeq2d 4946	. . . . 5 ⊢ (𝑤 = 𝑃 → (𝐹 “ (^◡𝑁‘𝑤)) = (𝐹 “ (^◡𝑁‘𝑃)))
24	20, 21, 23	f1oeq123d 5427	. . . 4 ⊢ (𝑤 = 𝑃 → ((𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤)) ↔ (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃))))
25	24	imbi2d 229	. . 3 ⊢ (𝑤 = 𝑃 → ((𝜑 → (𝐻‘𝑤):dom (𝐻‘𝑤)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑤))) ↔ (𝜑 → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑃)))))
26		f1o0 5469	. . . 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 12338	. . . . 5 ⊢ (𝜑 → (𝐻‘0) = ∅)
35	34	dmeqd 4806	. . . . . 6 ⊢ (𝜑 → dom (𝐻‘0) = dom ∅)
36		dm0 4818	. . . . . 6 ⊢ dom ∅ = ∅
37	35, 36	eqtrdi 2215	. . . . 5 ⊢ (𝜑 → dom (𝐻‘0) = ∅)
38		0zd 9203	. . . . . . . . . . . 12 ⊢ (⊤ → 0 ∈ ℤ)
39	38, 31	frec2uz0d 10334	. . . . . . . . . . 11 ⊢ (⊤ → (𝑁‘∅) = 0)
40	39	mptru 1352	. . . . . . . . . 10 ⊢ (𝑁‘∅) = 0
41	40	fveq2i 5489	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = (^◡𝑁‘0)
42	38, 31	frec2uzf1od 10341	. . . . . . . . . . 11 ⊢ (⊤ → 𝑁:ω–1-1-onto→(ℤ_≥‘0))
43	42	mptru 1352	. . . . . . . . . 10 ⊢ 𝑁:ω–1-1-onto→(ℤ_≥‘0)
44		peano1 4571	. . . . . . . . . 10 ⊢ ∅ ∈ ω
45		f1ocnvfv1 5745	. . . . . . . . . 10 ⊢ ((𝑁:ω–1-1-onto→(ℤ_≥‘0) ∧ ∅ ∈ ω) → (^◡𝑁‘(𝑁‘∅)) = ∅)
46	43, 44, 45	mp2an 423	. . . . . . . . 9 ⊢ (^◡𝑁‘(𝑁‘∅)) = ∅
47	41, 46	eqtr3i 2188	. . . . . . . 8 ⊢ (^◡𝑁‘0) = ∅
48	47	imaeq2i 4944	. . . . . . 7 ⊢ (𝐹 “ (^◡𝑁‘0)) = (𝐹 “ ∅)
49		ima0 4963	. . . . . . 7 ⊢ (𝐹 “ ∅) = ∅
50	48, 49	eqtri 2186	. . . . . 6 ⊢ (𝐹 “ (^◡𝑁‘0)) = ∅
51	50	a1i 9	. . . . 5 ⊢ (𝜑 → (𝐹 “ (^◡𝑁‘0)) = ∅)
52	34, 37, 51	f1oeq123d 5427	. . . 4 ⊢ (𝜑 → ((𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (^◡𝑁‘0)) ↔ ∅:∅–1-1-onto→∅))
53	26, 52	mpbiri 167	. . 3 ⊢ (𝜑 → (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (^◡𝑁‘0)))
54		simplr 520	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))
55	27	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
56	28	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹:ω–onto→𝐴)
57	29	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
58		simplr 520	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝑘 ∈ ℕ₀)
59	55, 56, 57, 30, 31, 32, 33, 58	ennnfonelemp1 12339	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})))
60	59	adantr 274	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})))
61		simpr 109	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
62	61	iftrued 3527	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = (𝐻‘𝑘))
63	60, 62	eqtrd 2198	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = (𝐻‘𝑘))
64	63	dmeqd 4806	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = dom (𝐻‘𝑘))
65		0zd 9203	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 0 ∈ ℤ)
66	31	frechashgf1o 10363	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑁:ω–1-1-onto→ℕ₀
67	66	a1i 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝑁:ω–1-1-onto→ℕ₀)
68		f1ocnv 5445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁:ω–1-1-onto→ℕ₀ → ^◡𝑁:ℕ₀–1-1-onto→ω)
69		f1of 5432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡𝑁:ℕ₀–1-1-onto→ω → ^◡𝑁:ℕ₀⟶ω)
70	67, 68, 69	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ^◡𝑁:ℕ₀⟶ω)
71	70, 58	ffvelrnd 5621	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘𝑘) ∈ ω)
72	65, 31, 71	frec2uzsucd 10336	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = ((𝑁‘(^◡𝑁‘𝑘)) + 1))
73		f1ocnvfv2 5746	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
74	66, 58, 73	sylancr 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘(^◡𝑁‘𝑘)) = 𝑘)
75	74	oveq1d 5857	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝑁‘(^◡𝑁‘𝑘)) + 1) = (𝑘 + 1))
76	72, 75	eqtrd 2198	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝑁‘suc (^◡𝑁‘𝑘)) = (𝑘 + 1))
77	76	fveq2d 5490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = (^◡𝑁‘(𝑘 + 1)))
78		peano2 4572	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑁‘𝑘) ∈ ω → suc (^◡𝑁‘𝑘) ∈ ω)
79	71, 78	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → suc (^◡𝑁‘𝑘) ∈ ω)
80		f1ocnvfv1 5745	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁:ω–1-1-onto→ℕ₀ ∧ suc (^◡𝑁‘𝑘) ∈ ω) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
81	66, 79, 80	sylancr 411	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑁‘suc (^◡𝑁‘𝑘))) = suc (^◡𝑁‘𝑘))
82	77, 81	eqtr3d 2200	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = suc (^◡𝑁‘𝑘))
83		df-suc 4349	. . . . . . . . . . . . . 14 ⊢ suc (^◡𝑁‘𝑘) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})
84	82, 83	eqtrdi 2215	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (^◡𝑁‘(𝑘 + 1)) = ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)}))
85	84	imaeq2d 4946	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})))
86		imaundi 5016	. . . . . . . . . . . 12 ⊢ (𝐹 “ ((^◡𝑁‘𝑘) ∪ {(^◡𝑁‘𝑘)})) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)}))
87	85, 86	eqtrdi 2215	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
88	87	adantr 274	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
89	61	snssd 3718	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)))
90		ssequn2 3295	. . . . . . . . . . . 12 ⊢ ({(𝐹‘(^◡𝑁‘𝑘))} ⊆ (𝐹 “ (^◡𝑁‘𝑘)) ↔ ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
91	89, 90	sylib 121	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)))
92		fofn 5412	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ω–onto→𝐴 → 𝐹 Fn ω)
93	56, 92	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹 Fn ω)
94		fnsnfv 5545	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn ω ∧ (^◡𝑁‘𝑘) ∈ ω) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
95	93, 71, 94	syl2anc 409	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
96	95	uneq2d 3276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
97	96	eqeq1d 2174	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)) ↔ ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})) = (𝐹 “ (^◡𝑁‘𝑘))))
98	97	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (((𝐹 “ (^◡𝑁‘𝑘)) ∪ {(𝐹‘(^◡𝑁‘𝑘))}) = (𝐹 “ (^◡𝑁‘𝑘)) ↔ ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})) = (𝐹 “ (^◡𝑁‘𝑘))))
99	91, 98	mpbid 146	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})) = (𝐹 “ (^◡𝑁‘𝑘)))
100	88, 99	eqtrd 2198	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = (𝐹 “ (^◡𝑁‘𝑘)))
101	63, 64, 100	f1oeq123d 5427	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))) ↔ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))))
102	54, 101	mpbird 166	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))
103		simplr 520	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)))
104	55, 56, 57, 30, 31, 32, 33, 58	ennnfonelemom 12341	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
105	104	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘𝑘) ∈ ω)
106		fof 5410	. . . . . . . . . . . . . 14 ⊢ (𝐹:ω–onto→𝐴 → 𝐹:ω⟶𝐴)
107	56, 106	syl 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → 𝐹:ω⟶𝐴)
108	107, 71	ffvelrnd 5621	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
109	108	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴)
110		f1osng 5473	. . . . . . . . . . 11 ⊢ ((dom (𝐻‘𝑘) ∈ ω ∧ (𝐹‘(^◡𝑁‘𝑘)) ∈ 𝐴) → {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→{(𝐹‘(^◡𝑁‘𝑘))})
111	105, 109, 110	syl2anc 409	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→{(𝐹‘(^◡𝑁‘𝑘))})
112	95	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {(𝐹‘(^◡𝑁‘𝑘))} = (𝐹 “ {(^◡𝑁‘𝑘)}))
113		f1oeq3 5423	. . . . . . . . . . 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 146	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}:{dom (𝐻‘𝑘)}–1-1-onto→(𝐹 “ {(^◡𝑁‘𝑘)}))
116		nnord 4589	. . . . . . . . . 10 ⊢ (dom (𝐻‘𝑘) ∈ ω → Ord dom (𝐻‘𝑘))
117		orddisj 4523	. . . . . . . . . 10 ⊢ (Ord dom (𝐻‘𝑘) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
118	105, 116, 117	3syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (dom (𝐻‘𝑘) ∩ {dom (𝐻‘𝑘)}) = ∅)
119	112	ineq2d 3323	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})))
120		simpr 109	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
121		disjsn 3638	. . . . . . . . . . 11 ⊢ (((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅ ↔ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
122	120, 121	sylibr 133	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ {(𝐹‘(^◡𝑁‘𝑘))}) = ∅)
123	119, 122	eqtr3d 2200	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹 “ (^◡𝑁‘𝑘)) ∩ (𝐹 “ {(^◡𝑁‘𝑘)})) = ∅)
124		f1oun 5452	. . . . . . . . 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 1229	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}):(dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})–1-1-onto→((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
126	59	adantr 274	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})))
127	120	iffalsed 3530	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → if((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)), (𝐻‘𝑘), ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩})) = ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}))
128	126, 127	eqtrd 2198	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)) = ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}))
129	55	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
130	56	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → 𝐹:ω–onto→𝐴)
131	57	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
132	58	adantr 274	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → 𝑘 ∈ ℕ₀)
133	129, 130, 131, 30, 31, 32, 33, 132, 120	ennnfonelemhdmp1 12342	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = suc dom (𝐻‘𝑘))
134		df-suc 4349	. . . . . . . . . 10 ⊢ suc dom (𝐻‘𝑘) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})
135	133, 134	eqtrdi 2215	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → dom (𝐻‘(𝑘 + 1)) = (dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)}))
136	87	adantr 274	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐹 “ (^◡𝑁‘(𝑘 + 1))) = ((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)})))
137	128, 135, 136	f1oeq123d 5427	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → ((𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))) ↔ ((𝐻‘𝑘) ∪ {⟨dom (𝐻‘𝑘), (𝐹‘(^◡𝑁‘𝑘))⟩}):(dom (𝐻‘𝑘) ∪ {dom (𝐻‘𝑘)})–1-1-onto→((𝐹 “ (^◡𝑁‘𝑘)) ∪ (𝐹 “ {(^◡𝑁‘𝑘)}))))
138	125, 137	mpbird 166	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) ∧ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))
139	55, 56, 71	ennnfonelemdc 12332	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)))
140		exmiddc 826	. . . . . . . 8 ⊢ (DECID (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
141	139, 140	syl 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → ((𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘)) ∨ ¬ (𝐹‘(^◡𝑁‘𝑘)) ∈ (𝐹 “ (^◡𝑁‘𝑘))))
142	102, 138, 141	mpjaodan 788	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1))))
143	142	ex 114	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((𝐻‘𝑘):dom (𝐻‘𝑘)–1-1-onto→(𝐹 “ (^◡𝑁‘𝑘)) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (^◡𝑁‘(𝑘 + 1)))))
144	143	expcom 115	. . . 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 9305	. 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 103 ↔ wb 104 ∨ wo 698 DECID wdc 824 = wceq 1343 ⊤wtru 1344 ∈ wcel 2136 ≠ wne 2336 ∀wral 2444 ∃wrex 2445 ∪ cun 3114 ∩ cin 3115 ⊆ wss 3116 ∅c0 3409 ifcif 3520 {csn 3576 ⟨cop 3579 ↦ cmpt 4043 Ord word 4340 suc csuc 4343 ωcom 4567 ^◡ccnv 4603 dom cdm 4604 “ cima 4607 Fn wfn 5183 ⟶wf 5184 –onto→wfo 5186 –1-1-onto→wf1o 5187 ‘cfv 5188 (class class class)co 5842 ∈ cmpo 5844 freccfrec 6358 ↑_pm cpm 6615 0cc0 7753 1c1 7754 + caddc 7756 − cmin 8069 ℕ₀cn0 9114 ℤcz 9191 ℤ_≥cuz 9466 seqcseq 10380

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-addcom 7853 ax-addass 7855 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-0id 7861 ax-rnegex 7862 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-ltadd 7869

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-frec 6359 df-pm 6617 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-inn 8858 df-n0 9115 df-z 9192 df-uz 9467 df-seqfrec 10381

This theorem is referenced by: ennnfonelemex 12347 ennnfonelemf1 12351 ennnfonelemrn 12352

W3C validator