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

Theorem ennnfonelemhf1o 12384
Description: Lemma for ennnfone 12396. 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 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))
ennnfonelemh.h 𝐻 = seq0(𝐺, 𝐽)
ennnfonelemhf1o.p (𝜑𝑃 ∈ ℕ0)
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.
StepHypRef Expression
1 ennnfonelemhf1o.p . 2 (𝜑𝑃 ∈ ℕ0)
2 fveq2 5510 . . . . 5 (𝑤 = 0 → (𝐻𝑤) = (𝐻‘0))
32dmeqd 4824 . . . . 5 (𝑤 = 0 → dom (𝐻𝑤) = dom (𝐻‘0))
4 fveq2 5510 . . . . . 6 (𝑤 = 0 → (𝑁𝑤) = (𝑁‘0))
54imaeq2d 4965 . . . . 5 (𝑤 = 0 → (𝐹 “ (𝑁𝑤)) = (𝐹 “ (𝑁‘0)))
62, 3, 5f1oeq123d 5450 . . . 4 (𝑤 = 0 → ((𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤)) ↔ (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (𝑁‘0))))
76imbi2d 230 . . 3 (𝑤 = 0 → ((𝜑 → (𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤))) ↔ (𝜑 → (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (𝑁‘0)))))
8 fveq2 5510 . . . . 5 (𝑤 = 𝑘 → (𝐻𝑤) = (𝐻𝑘))
98dmeqd 4824 . . . . 5 (𝑤 = 𝑘 → dom (𝐻𝑤) = dom (𝐻𝑘))
10 fveq2 5510 . . . . . 6 (𝑤 = 𝑘 → (𝑁𝑤) = (𝑁𝑘))
1110imaeq2d 4965 . . . . 5 (𝑤 = 𝑘 → (𝐹 “ (𝑁𝑤)) = (𝐹 “ (𝑁𝑘)))
128, 9, 11f1oeq123d 5450 . . . 4 (𝑤 = 𝑘 → ((𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤)) ↔ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))))
1312imbi2d 230 . . 3 (𝑤 = 𝑘 → ((𝜑 → (𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤))) ↔ (𝜑 → (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)))))
14 fveq2 5510 . . . . 5 (𝑤 = (𝑘 + 1) → (𝐻𝑤) = (𝐻‘(𝑘 + 1)))
1514dmeqd 4824 . . . . 5 (𝑤 = (𝑘 + 1) → dom (𝐻𝑤) = dom (𝐻‘(𝑘 + 1)))
16 fveq2 5510 . . . . . 6 (𝑤 = (𝑘 + 1) → (𝑁𝑤) = (𝑁‘(𝑘 + 1)))
1716imaeq2d 4965 . . . . 5 (𝑤 = (𝑘 + 1) → (𝐹 “ (𝑁𝑤)) = (𝐹 “ (𝑁‘(𝑘 + 1))))
1814, 15, 17f1oeq123d 5450 . . . 4 (𝑤 = (𝑘 + 1) → ((𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤)) ↔ (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1)))))
1918imbi2d 230 . . 3 (𝑤 = (𝑘 + 1) → ((𝜑 → (𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤))) ↔ (𝜑 → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))))
20 fveq2 5510 . . . . 5 (𝑤 = 𝑃 → (𝐻𝑤) = (𝐻𝑃))
2120dmeqd 4824 . . . . 5 (𝑤 = 𝑃 → dom (𝐻𝑤) = dom (𝐻𝑃))
22 fveq2 5510 . . . . . 6 (𝑤 = 𝑃 → (𝑁𝑤) = (𝑁𝑃))
2322imaeq2d 4965 . . . . 5 (𝑤 = 𝑃 → (𝐹 “ (𝑁𝑤)) = (𝐹 “ (𝑁𝑃)))
2420, 21, 23f1oeq123d 5450 . . . 4 (𝑤 = 𝑃 → ((𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤)) ↔ (𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃))))
2524imbi2d 230 . . 3 (𝑤 = 𝑃 → ((𝜑 → (𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤))) ↔ (𝜑 → (𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)))))
26 f1o0 5493 . . . 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 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))
33 ennnfonelemh.h . . . . . 6 𝐻 = seq0(𝐺, 𝐽)
3427, 28, 29, 30, 31, 32, 33ennnfonelem0 12376 . . . . 5 (𝜑 → (𝐻‘0) = ∅)
3534dmeqd 4824 . . . . . 6 (𝜑 → dom (𝐻‘0) = dom ∅)
36 dm0 4836 . . . . . 6 dom ∅ = ∅
3735, 36eqtrdi 2226 . . . . 5 (𝜑 → dom (𝐻‘0) = ∅)
38 0zd 9241 . . . . . . . . . . . 12 (⊤ → 0 ∈ ℤ)
3938, 31frec2uz0d 10372 . . . . . . . . . . 11 (⊤ → (𝑁‘∅) = 0)
4039mptru 1362 . . . . . . . . . 10 (𝑁‘∅) = 0
4140fveq2i 5513 . . . . . . . . 9 (𝑁‘(𝑁‘∅)) = (𝑁‘0)
4238, 31frec2uzf1od 10379 . . . . . . . . . . 11 (⊤ → 𝑁:ω–1-1-onto→(ℤ‘0))
4342mptru 1362 . . . . . . . . . 10 𝑁:ω–1-1-onto→(ℤ‘0)
44 peano1 4589 . . . . . . . . . 10 ∅ ∈ ω
45 f1ocnvfv1 5771 . . . . . . . . . 10 ((𝑁:ω–1-1-onto→(ℤ‘0) ∧ ∅ ∈ ω) → (𝑁‘(𝑁‘∅)) = ∅)
4643, 44, 45mp2an 426 . . . . . . . . 9 (𝑁‘(𝑁‘∅)) = ∅
4741, 46eqtr3i 2200 . . . . . . . 8 (𝑁‘0) = ∅
4847imaeq2i 4963 . . . . . . 7 (𝐹 “ (𝑁‘0)) = (𝐹 “ ∅)
49 ima0 4982 . . . . . . 7 (𝐹 “ ∅) = ∅
5048, 49eqtri 2198 . . . . . 6 (𝐹 “ (𝑁‘0)) = ∅
5150a1i 9 . . . . 5 (𝜑 → (𝐹 “ (𝑁‘0)) = ∅)
5234, 37, 51f1oeq123d 5450 . . . 4 (𝜑 → ((𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (𝑁‘0)) ↔ ∅:∅–1-1-onto→∅))
5326, 52mpbiri 168 . . 3 (𝜑 → (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (𝑁‘0)))
54 simplr 528 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)))
5527ad2antrr 488 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
5628ad2antrr 488 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝐹:ω–onto𝐴)
5729ad2antrr 488 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
58 simplr 528 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝑘 ∈ ℕ0)
5955, 56, 57, 30, 31, 32, 33, 58ennnfonelemp1 12377 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})))
6059adantr 276 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})))
61 simpr 110 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)))
6261iftrued 3541 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})) = (𝐻𝑘))
6360, 62eqtrd 2210 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = (𝐻𝑘))
6463dmeqd 4824 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → dom (𝐻‘(𝑘 + 1)) = dom (𝐻𝑘))
65 0zd 9241 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 0 ∈ ℤ)
6631frechashgf1o 10401 . . . . . . . . . . . . . . . . . . . . 21 𝑁:ω–1-1-onto→ℕ0
6766a1i 9 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝑁:ω–1-1-onto→ℕ0)
68 f1ocnv 5469 . . . . . . . . . . . . . . . . . . . 20 (𝑁:ω–1-1-onto→ℕ0𝑁:ℕ01-1-onto→ω)
69 f1of 5456 . . . . . . . . . . . . . . . . . . . 20 (𝑁:ℕ01-1-onto→ω → 𝑁:ℕ0⟶ω)
7067, 68, 693syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝑁:ℕ0⟶ω)
7170, 58ffvelcdmd 5647 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁𝑘) ∈ ω)
7265, 31, 71frec2uzsucd 10374 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘suc (𝑁𝑘)) = ((𝑁‘(𝑁𝑘)) + 1))
73 f1ocnvfv2 5772 . . . . . . . . . . . . . . . . . . 19 ((𝑁:ω–1-1-onto→ℕ0𝑘 ∈ ℕ0) → (𝑁‘(𝑁𝑘)) = 𝑘)
7466, 58, 73sylancr 414 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑁𝑘)) = 𝑘)
7574oveq1d 5883 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ((𝑁‘(𝑁𝑘)) + 1) = (𝑘 + 1))
7672, 75eqtrd 2210 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘suc (𝑁𝑘)) = (𝑘 + 1))
7776fveq2d 5514 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑁‘suc (𝑁𝑘))) = (𝑁‘(𝑘 + 1)))
78 peano2 4590 . . . . . . . . . . . . . . . . 17 ((𝑁𝑘) ∈ ω → suc (𝑁𝑘) ∈ ω)
7971, 78syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → suc (𝑁𝑘) ∈ ω)
80 f1ocnvfv1 5771 . . . . . . . . . . . . . . . 16 ((𝑁:ω–1-1-onto→ℕ0 ∧ suc (𝑁𝑘) ∈ ω) → (𝑁‘(𝑁‘suc (𝑁𝑘))) = suc (𝑁𝑘))
8166, 79, 80sylancr 414 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑁‘suc (𝑁𝑘))) = suc (𝑁𝑘))
8277, 81eqtr3d 2212 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑘 + 1)) = suc (𝑁𝑘))
83 df-suc 4367 . . . . . . . . . . . . . 14 suc (𝑁𝑘) = ((𝑁𝑘) ∪ {(𝑁𝑘)})
8482, 83eqtrdi 2226 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑘 + 1)) = ((𝑁𝑘) ∪ {(𝑁𝑘)}))
8584imaeq2d 4965 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = (𝐹 “ ((𝑁𝑘) ∪ {(𝑁𝑘)})))
86 imaundi 5036 . . . . . . . . . . . 12 (𝐹 “ ((𝑁𝑘) ∪ {(𝑁𝑘)})) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)}))
8785, 86eqtrdi 2226 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
8887adantr 276 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
8961snssd 3736 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → {(𝐹‘(𝑁𝑘))} ⊆ (𝐹 “ (𝑁𝑘)))
90 ssequn2 3308 . . . . . . . . . . . 12 ({(𝐹‘(𝑁𝑘))} ⊆ (𝐹 “ (𝑁𝑘)) ↔ ((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = (𝐹 “ (𝑁𝑘)))
9189, 90sylib 122 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = (𝐹 “ (𝑁𝑘)))
92 fofn 5435 . . . . . . . . . . . . . . . 16 (𝐹:ω–onto𝐴𝐹 Fn ω)
9356, 92syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝐹 Fn ω)
94 fnsnfv 5570 . . . . . . . . . . . . . . 15 ((𝐹 Fn ω ∧ (𝑁𝑘) ∈ ω) → {(𝐹‘(𝑁𝑘))} = (𝐹 “ {(𝑁𝑘)}))
9593, 71, 94syl2anc 411 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → {(𝐹‘(𝑁𝑘))} = (𝐹 “ {(𝑁𝑘)}))
9695uneq2d 3289 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
9796eqeq1d 2186 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = (𝐹 “ (𝑁𝑘)) ↔ ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})) = (𝐹 “ (𝑁𝑘))))
9897adantr 276 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = (𝐹 “ (𝑁𝑘)) ↔ ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})) = (𝐹 “ (𝑁𝑘))))
9991, 98mpbid 147 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})) = (𝐹 “ (𝑁𝑘)))
10088, 99eqtrd 2210 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = (𝐹 “ (𝑁𝑘)))
10163, 64, 100f1oeq123d 5450 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))) ↔ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))))
10254, 101mpbird 167 . . . . . . 7 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))
103 simplr 528 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)))
10455, 56, 57, 30, 31, 32, 33, 58ennnfonelemom 12379 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → dom (𝐻𝑘) ∈ ω)
105104adantr 276 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → dom (𝐻𝑘) ∈ ω)
106 fof 5433 . . . . . . . . . . . . . 14 (𝐹:ω–onto𝐴𝐹:ω⟶𝐴)
10756, 106syl 14 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝐹:ω⟶𝐴)
108107, 71ffvelcdmd 5647 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐹‘(𝑁𝑘)) ∈ 𝐴)
109108adantr 276 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹‘(𝑁𝑘)) ∈ 𝐴)
110 f1osng 5497 . . . . . . . . . . 11 ((dom (𝐻𝑘) ∈ ω ∧ (𝐹‘(𝑁𝑘)) ∈ 𝐴) → {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→{(𝐹‘(𝑁𝑘))})
111105, 109, 110syl2anc 411 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→{(𝐹‘(𝑁𝑘))})
11295adantr 276 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → {(𝐹‘(𝑁𝑘))} = (𝐹 “ {(𝑁𝑘)}))
113 f1oeq3 5446 . . . . . . . . . . 11 ({(𝐹‘(𝑁𝑘))} = (𝐹 “ {(𝑁𝑘)}) → ({⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→{(𝐹‘(𝑁𝑘))} ↔ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→(𝐹 “ {(𝑁𝑘)})))
114112, 113syl 14 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ({⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→{(𝐹‘(𝑁𝑘))} ↔ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→(𝐹 “ {(𝑁𝑘)})))
115111, 114mpbid 147 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→(𝐹 “ {(𝑁𝑘)}))
116 nnord 4607 . . . . . . . . . 10 (dom (𝐻𝑘) ∈ ω → Ord dom (𝐻𝑘))
117 orddisj 4541 . . . . . . . . . 10 (Ord dom (𝐻𝑘) → (dom (𝐻𝑘) ∩ {dom (𝐻𝑘)}) = ∅)
118105, 116, 1173syl 17 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (dom (𝐻𝑘) ∩ {dom (𝐻𝑘)}) = ∅)
119112ineq2d 3336 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∩ {(𝐹‘(𝑁𝑘))}) = ((𝐹 “ (𝑁𝑘)) ∩ (𝐹 “ {(𝑁𝑘)})))
120 simpr 110 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)))
121 disjsn 3653 . . . . . . . . . . 11 (((𝐹 “ (𝑁𝑘)) ∩ {(𝐹‘(𝑁𝑘))}) = ∅ ↔ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)))
122120, 121sylibr 134 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∩ {(𝐹‘(𝑁𝑘))}) = ∅)
123119, 122eqtr3d 2212 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∩ (𝐹 “ {(𝑁𝑘)})) = ∅)
124 f1oun 5476 . . . . . . . . 9 ((((𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)) ∧ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→(𝐹 “ {(𝑁𝑘)})) ∧ ((dom (𝐻𝑘) ∩ {dom (𝐻𝑘)}) = ∅ ∧ ((𝐹 “ (𝑁𝑘)) ∩ (𝐹 “ {(𝑁𝑘)})) = ∅)) → ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}):(dom (𝐻𝑘) ∪ {dom (𝐻𝑘)})–1-1-onto→((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
125103, 115, 118, 123, 124syl22anc 1239 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}):(dom (𝐻𝑘) ∪ {dom (𝐻𝑘)})–1-1-onto→((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
12659adantr 276 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})))
127120iffalsed 3544 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})) = ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}))
128126, 127eqtrd 2210 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}))
12955adantr 276 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
13056adantr 276 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → 𝐹:ω–onto𝐴)
13157adantr 276 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
13258adantr 276 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → 𝑘 ∈ ℕ0)
133129, 130, 131, 30, 31, 32, 33, 132, 120ennnfonelemhdmp1 12380 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → dom (𝐻‘(𝑘 + 1)) = suc dom (𝐻𝑘))
134 df-suc 4367 . . . . . . . . . 10 suc dom (𝐻𝑘) = (dom (𝐻𝑘) ∪ {dom (𝐻𝑘)})
135133, 134eqtrdi 2226 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → dom (𝐻‘(𝑘 + 1)) = (dom (𝐻𝑘) ∪ {dom (𝐻𝑘)}))
13687adantr 276 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
137128, 135, 136f1oeq123d 5450 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))) ↔ ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}):(dom (𝐻𝑘) ∪ {dom (𝐻𝑘)})–1-1-onto→((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)}))))
138125, 137mpbird 167 . . . . . . 7 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))
13955, 56, 71ennnfonelemdc 12370 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → DECID (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)))
140 exmiddc 836 . . . . . . . 8 (DECID (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)) → ((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)) ∨ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))))
141139, 140syl 14 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)) ∨ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))))
142102, 138, 141mpjaodan 798 . . . . . 6 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))
143142ex 115 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1)))))
144143expcom 116 . . . 4 (𝑘 ∈ ℕ0 → (𝜑 → ((𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))))
145144a2d 26 . . 3 (𝑘 ∈ ℕ0 → ((𝜑 → (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝜑 → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))))
1467, 13, 19, 25, 53, 145nn0ind 9343 . 2 (𝑃 ∈ ℕ0 → (𝜑 → (𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃))))
1471, 146mpcom 36 1 (𝜑 → (𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834   = wceq 1353  wtru 1354  wcel 2148  wne 2347  wral 2455  wrex 2456  cun 3127  cin 3128  wss 3129  c0 3422  ifcif 3534  {csn 3591  cop 3594  cmpt 4061  Ord word 4358  suc csuc 4361  ωcom 4585  ccnv 4621  dom cdm 4622  cima 4625   Fn wfn 5206  wf 5207  ontowfo 5209  1-1-ontowf1o 5210  cfv 5211  (class class class)co 5868  cmpo 5870  freccfrec 6384  pm cpm 6642  0cc0 7789  1c1 7790   + caddc 7792  cmin 8105  0cn0 9152  cz 9229  cuz 9504  seqcseq 10418
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4205  ax-un 4429  ax-setind 4532  ax-iinf 4583  ax-cnex 7880  ax-resscn 7881  ax-1cn 7882  ax-1re 7883  ax-icn 7884  ax-addcl 7885  ax-addrcl 7886  ax-mulcl 7887  ax-addcom 7889  ax-addass 7891  ax-distr 7893  ax-i2m1 7894  ax-0lt1 7895  ax-0id 7897  ax-rnegex 7898  ax-cnre 7900  ax-pre-ltirr 7901  ax-pre-ltwlin 7902  ax-pre-lttrn 7903  ax-pre-ltadd 7905
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4289  df-iord 4362  df-on 4364  df-ilim 4365  df-suc 4367  df-iom 4586  df-xp 4628  df-rel 4629  df-cnv 4630  df-co 4631  df-dm 4632  df-rn 4633  df-res 4634  df-ima 4635  df-iota 5173  df-fun 5213  df-fn 5214  df-f 5215  df-f1 5216  df-fo 5217  df-f1o 5218  df-fv 5219  df-riota 5824  df-ov 5871  df-oprab 5872  df-mpo 5873  df-1st 6134  df-2nd 6135  df-recs 6299  df-frec 6385  df-pm 6644  df-pnf 7971  df-mnf 7972  df-xr 7973  df-ltxr 7974  df-le 7975  df-sub 8107  df-neg 8108  df-inn 8896  df-n0 9153  df-z 9230  df-uz 9505  df-seqfrec 10419
This theorem is referenced by:  ennnfonelemex  12385  ennnfonelemf1  12389  ennnfonelemrn  12390
  Copyright terms: Public domain W3C validator