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

Theorem ennnfonelemhf1o 11937
 Description: Lemma for ennnfone 11949. 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 5421 . . . . 5 (𝑤 = 0 → (𝐻𝑤) = (𝐻‘0))
32dmeqd 4741 . . . . 5 (𝑤 = 0 → dom (𝐻𝑤) = dom (𝐻‘0))
4 fveq2 5421 . . . . . 6 (𝑤 = 0 → (𝑁𝑤) = (𝑁‘0))
54imaeq2d 4881 . . . . 5 (𝑤 = 0 → (𝐹 “ (𝑁𝑤)) = (𝐹 “ (𝑁‘0)))
62, 3, 5f1oeq123d 5362 . . . 4 (𝑤 = 0 → ((𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤)) ↔ (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (𝑁‘0))))
76imbi2d 229 . . 3 (𝑤 = 0 → ((𝜑 → (𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤))) ↔ (𝜑 → (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (𝑁‘0)))))
8 fveq2 5421 . . . . 5 (𝑤 = 𝑘 → (𝐻𝑤) = (𝐻𝑘))
98dmeqd 4741 . . . . 5 (𝑤 = 𝑘 → dom (𝐻𝑤) = dom (𝐻𝑘))
10 fveq2 5421 . . . . . 6 (𝑤 = 𝑘 → (𝑁𝑤) = (𝑁𝑘))
1110imaeq2d 4881 . . . . 5 (𝑤 = 𝑘 → (𝐹 “ (𝑁𝑤)) = (𝐹 “ (𝑁𝑘)))
128, 9, 11f1oeq123d 5362 . . . 4 (𝑤 = 𝑘 → ((𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤)) ↔ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))))
1312imbi2d 229 . . 3 (𝑤 = 𝑘 → ((𝜑 → (𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤))) ↔ (𝜑 → (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)))))
14 fveq2 5421 . . . . 5 (𝑤 = (𝑘 + 1) → (𝐻𝑤) = (𝐻‘(𝑘 + 1)))
1514dmeqd 4741 . . . . 5 (𝑤 = (𝑘 + 1) → dom (𝐻𝑤) = dom (𝐻‘(𝑘 + 1)))
16 fveq2 5421 . . . . . 6 (𝑤 = (𝑘 + 1) → (𝑁𝑤) = (𝑁‘(𝑘 + 1)))
1716imaeq2d 4881 . . . . 5 (𝑤 = (𝑘 + 1) → (𝐹 “ (𝑁𝑤)) = (𝐹 “ (𝑁‘(𝑘 + 1))))
1814, 15, 17f1oeq123d 5362 . . . 4 (𝑤 = (𝑘 + 1) → ((𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤)) ↔ (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1)))))
1918imbi2d 229 . . 3 (𝑤 = (𝑘 + 1) → ((𝜑 → (𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤))) ↔ (𝜑 → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))))
20 fveq2 5421 . . . . 5 (𝑤 = 𝑃 → (𝐻𝑤) = (𝐻𝑃))
2120dmeqd 4741 . . . . 5 (𝑤 = 𝑃 → dom (𝐻𝑤) = dom (𝐻𝑃))
22 fveq2 5421 . . . . . 6 (𝑤 = 𝑃 → (𝑁𝑤) = (𝑁𝑃))
2322imaeq2d 4881 . . . . 5 (𝑤 = 𝑃 → (𝐹 “ (𝑁𝑤)) = (𝐹 “ (𝑁𝑃)))
2420, 21, 23f1oeq123d 5362 . . . 4 (𝑤 = 𝑃 → ((𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤)) ↔ (𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃))))
2524imbi2d 229 . . 3 (𝑤 = 𝑃 → ((𝜑 → (𝐻𝑤):dom (𝐻𝑤)–1-1-onto→(𝐹 “ (𝑁𝑤))) ↔ (𝜑 → (𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)))))
26 f1o0 5404 . . . 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 11929 . . . . 5 (𝜑 → (𝐻‘0) = ∅)
3534dmeqd 4741 . . . . . 6 (𝜑 → dom (𝐻‘0) = dom ∅)
36 dm0 4753 . . . . . 6 dom ∅ = ∅
3735, 36syl6eq 2188 . . . . 5 (𝜑 → dom (𝐻‘0) = ∅)
38 0zd 9078 . . . . . . . . . . . 12 (⊤ → 0 ∈ ℤ)
3938, 31frec2uz0d 10184 . . . . . . . . . . 11 (⊤ → (𝑁‘∅) = 0)
4039mptru 1340 . . . . . . . . . 10 (𝑁‘∅) = 0
4140fveq2i 5424 . . . . . . . . 9 (𝑁‘(𝑁‘∅)) = (𝑁‘0)
4238, 31frec2uzf1od 10191 . . . . . . . . . . 11 (⊤ → 𝑁:ω–1-1-onto→(ℤ‘0))
4342mptru 1340 . . . . . . . . . 10 𝑁:ω–1-1-onto→(ℤ‘0)
44 peano1 4508 . . . . . . . . . 10 ∅ ∈ ω
45 f1ocnvfv1 5678 . . . . . . . . . 10 ((𝑁:ω–1-1-onto→(ℤ‘0) ∧ ∅ ∈ ω) → (𝑁‘(𝑁‘∅)) = ∅)
4643, 44, 45mp2an 422 . . . . . . . . 9 (𝑁‘(𝑁‘∅)) = ∅
4741, 46eqtr3i 2162 . . . . . . . 8 (𝑁‘0) = ∅
4847imaeq2i 4879 . . . . . . 7 (𝐹 “ (𝑁‘0)) = (𝐹 “ ∅)
49 ima0 4898 . . . . . . 7 (𝐹 “ ∅) = ∅
5048, 49eqtri 2160 . . . . . 6 (𝐹 “ (𝑁‘0)) = ∅
5150a1i 9 . . . . 5 (𝜑 → (𝐹 “ (𝑁‘0)) = ∅)
5234, 37, 51f1oeq123d 5362 . . . 4 (𝜑 → ((𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (𝑁‘0)) ↔ ∅:∅–1-1-onto→∅))
5326, 52mpbiri 167 . . 3 (𝜑 → (𝐻‘0):dom (𝐻‘0)–1-1-onto→(𝐹 “ (𝑁‘0)))
54 simplr 519 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)))
5527ad2antrr 479 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
5628ad2antrr 479 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝐹:ω–onto𝐴)
5729ad2antrr 479 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
58 simplr 519 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝑘 ∈ ℕ0)
5955, 56, 57, 30, 31, 32, 33, 58ennnfonelemp1 11930 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})))
6059adantr 274 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})))
61 simpr 109 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)))
6261iftrued 3481 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})) = (𝐻𝑘))
6360, 62eqtrd 2172 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = (𝐻𝑘))
6463dmeqd 4741 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → dom (𝐻‘(𝑘 + 1)) = dom (𝐻𝑘))
65 0zd 9078 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 0 ∈ ℤ)
6631frechashgf1o 10213 . . . . . . . . . . . . . . . . . . . . 21 𝑁:ω–1-1-onto→ℕ0
6766a1i 9 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝑁:ω–1-1-onto→ℕ0)
68 f1ocnv 5380 . . . . . . . . . . . . . . . . . . . 20 (𝑁:ω–1-1-onto→ℕ0𝑁:ℕ01-1-onto→ω)
69 f1of 5367 . . . . . . . . . . . . . . . . . . . 20 (𝑁:ℕ01-1-onto→ω → 𝑁:ℕ0⟶ω)
7067, 68, 693syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝑁:ℕ0⟶ω)
7170, 58ffvelrnd 5556 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁𝑘) ∈ ω)
7265, 31, 71frec2uzsucd 10186 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘suc (𝑁𝑘)) = ((𝑁‘(𝑁𝑘)) + 1))
73 f1ocnvfv2 5679 . . . . . . . . . . . . . . . . . . 19 ((𝑁:ω–1-1-onto→ℕ0𝑘 ∈ ℕ0) → (𝑁‘(𝑁𝑘)) = 𝑘)
7466, 58, 73sylancr 410 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑁𝑘)) = 𝑘)
7574oveq1d 5789 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ((𝑁‘(𝑁𝑘)) + 1) = (𝑘 + 1))
7672, 75eqtrd 2172 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘suc (𝑁𝑘)) = (𝑘 + 1))
7776fveq2d 5425 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑁‘suc (𝑁𝑘))) = (𝑁‘(𝑘 + 1)))
78 peano2 4509 . . . . . . . . . . . . . . . . 17 ((𝑁𝑘) ∈ ω → suc (𝑁𝑘) ∈ ω)
7971, 78syl 14 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → suc (𝑁𝑘) ∈ ω)
80 f1ocnvfv1 5678 . . . . . . . . . . . . . . . 16 ((𝑁:ω–1-1-onto→ℕ0 ∧ suc (𝑁𝑘) ∈ ω) → (𝑁‘(𝑁‘suc (𝑁𝑘))) = suc (𝑁𝑘))
8166, 79, 80sylancr 410 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑁‘suc (𝑁𝑘))) = suc (𝑁𝑘))
8277, 81eqtr3d 2174 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑘 + 1)) = suc (𝑁𝑘))
83 df-suc 4293 . . . . . . . . . . . . . 14 suc (𝑁𝑘) = ((𝑁𝑘) ∪ {(𝑁𝑘)})
8482, 83syl6eq 2188 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝑁‘(𝑘 + 1)) = ((𝑁𝑘) ∪ {(𝑁𝑘)}))
8584imaeq2d 4881 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = (𝐹 “ ((𝑁𝑘) ∪ {(𝑁𝑘)})))
86 imaundi 4951 . . . . . . . . . . . 12 (𝐹 “ ((𝑁𝑘) ∪ {(𝑁𝑘)})) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)}))
8785, 86syl6eq 2188 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
8887adantr 274 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
8961snssd 3665 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → {(𝐹‘(𝑁𝑘))} ⊆ (𝐹 “ (𝑁𝑘)))
90 ssequn2 3249 . . . . . . . . . . . 12 ({(𝐹‘(𝑁𝑘))} ⊆ (𝐹 “ (𝑁𝑘)) ↔ ((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = (𝐹 “ (𝑁𝑘)))
9189, 90sylib 121 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = (𝐹 “ (𝑁𝑘)))
92 fofn 5347 . . . . . . . . . . . . . . . 16 (𝐹:ω–onto𝐴𝐹 Fn ω)
9356, 92syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝐹 Fn ω)
94 fnsnfv 5480 . . . . . . . . . . . . . . 15 ((𝐹 Fn ω ∧ (𝑁𝑘) ∈ ω) → {(𝐹‘(𝑁𝑘))} = (𝐹 “ {(𝑁𝑘)}))
9593, 71, 94syl2anc 408 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → {(𝐹‘(𝑁𝑘))} = (𝐹 “ {(𝑁𝑘)}))
9695uneq2d 3230 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
9796eqeq1d 2148 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = (𝐹 “ (𝑁𝑘)) ↔ ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})) = (𝐹 “ (𝑁𝑘))))
9897adantr 274 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (((𝐹 “ (𝑁𝑘)) ∪ {(𝐹‘(𝑁𝑘))}) = (𝐹 “ (𝑁𝑘)) ↔ ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})) = (𝐹 “ (𝑁𝑘))))
9991, 98mpbid 146 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})) = (𝐹 “ (𝑁𝑘)))
10088, 99eqtrd 2172 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = (𝐹 “ (𝑁𝑘)))
10163, 64, 100f1oeq123d 5362 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))) ↔ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))))
10254, 101mpbird 166 . . . . . . 7 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))
103 simplr 519 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)))
10455, 56, 57, 30, 31, 32, 33, 58ennnfonelemom 11932 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → dom (𝐻𝑘) ∈ ω)
105104adantr 274 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → dom (𝐻𝑘) ∈ ω)
106 fof 5345 . . . . . . . . . . . . . 14 (𝐹:ω–onto𝐴𝐹:ω⟶𝐴)
10756, 106syl 14 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → 𝐹:ω⟶𝐴)
108107, 71ffvelrnd 5556 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐹‘(𝑁𝑘)) ∈ 𝐴)
109108adantr 274 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹‘(𝑁𝑘)) ∈ 𝐴)
110 f1osng 5408 . . . . . . . . . . 11 ((dom (𝐻𝑘) ∈ ω ∧ (𝐹‘(𝑁𝑘)) ∈ 𝐴) → {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→{(𝐹‘(𝑁𝑘))})
111105, 109, 110syl2anc 408 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→{(𝐹‘(𝑁𝑘))})
11295adantr 274 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → {(𝐹‘(𝑁𝑘))} = (𝐹 “ {(𝑁𝑘)}))
113 f1oeq3 5358 . . . . . . . . . . 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 146 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→(𝐹 “ {(𝑁𝑘)}))
116 nnord 4525 . . . . . . . . . 10 (dom (𝐻𝑘) ∈ ω → Ord dom (𝐻𝑘))
117 orddisj 4461 . . . . . . . . . 10 (Ord dom (𝐻𝑘) → (dom (𝐻𝑘) ∩ {dom (𝐻𝑘)}) = ∅)
118105, 116, 1173syl 17 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (dom (𝐻𝑘) ∩ {dom (𝐻𝑘)}) = ∅)
119112ineq2d 3277 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∩ {(𝐹‘(𝑁𝑘))}) = ((𝐹 “ (𝑁𝑘)) ∩ (𝐹 “ {(𝑁𝑘)})))
120 simpr 109 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)))
121 disjsn 3585 . . . . . . . . . . 11 (((𝐹 “ (𝑁𝑘)) ∩ {(𝐹‘(𝑁𝑘))}) = ∅ ↔ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)))
122120, 121sylibr 133 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∩ {(𝐹‘(𝑁𝑘))}) = ∅)
123119, 122eqtr3d 2174 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐹 “ (𝑁𝑘)) ∩ (𝐹 “ {(𝑁𝑘)})) = ∅)
124 f1oun 5387 . . . . . . . . 9 ((((𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)) ∧ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}:{dom (𝐻𝑘)}–1-1-onto→(𝐹 “ {(𝑁𝑘)})) ∧ ((dom (𝐻𝑘) ∩ {dom (𝐻𝑘)}) = ∅ ∧ ((𝐹 “ (𝑁𝑘)) ∩ (𝐹 “ {(𝑁𝑘)})) = ∅)) → ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}):(dom (𝐻𝑘) ∪ {dom (𝐻𝑘)})–1-1-onto→((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
125103, 115, 118, 123, 124syl22anc 1217 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}):(dom (𝐻𝑘) ∪ {dom (𝐻𝑘)})–1-1-onto→((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
12659adantr 274 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})))
127120iffalsed 3484 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → if((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)), (𝐻𝑘), ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩})) = ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}))
128126, 127eqtrd 2172 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)) = ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}))
12955adantr 274 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
13056adantr 274 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → 𝐹:ω–onto𝐴)
13157adantr 274 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
13258adantr 274 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → 𝑘 ∈ ℕ0)
133129, 130, 131, 30, 31, 32, 33, 132, 120ennnfonelemhdmp1 11933 . . . . . . . . . 10 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → dom (𝐻‘(𝑘 + 1)) = suc dom (𝐻𝑘))
134 df-suc 4293 . . . . . . . . . 10 suc dom (𝐻𝑘) = (dom (𝐻𝑘) ∪ {dom (𝐻𝑘)})
135133, 134syl6eq 2188 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → dom (𝐻‘(𝑘 + 1)) = (dom (𝐻𝑘) ∪ {dom (𝐻𝑘)}))
13687adantr 274 . . . . . . . . 9 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐹 “ (𝑁‘(𝑘 + 1))) = ((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)})))
137128, 135, 136f1oeq123d 5362 . . . . . . . 8 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → ((𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))) ↔ ((𝐻𝑘) ∪ {⟨dom (𝐻𝑘), (𝐹‘(𝑁𝑘))⟩}):(dom (𝐻𝑘) ∪ {dom (𝐻𝑘)})–1-1-onto→((𝐹 “ (𝑁𝑘)) ∪ (𝐹 “ {(𝑁𝑘)}))))
138125, 137mpbird 166 . . . . . . 7 ((((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) ∧ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))
13955, 56, 71ennnfonelemdc 11923 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → DECID (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)))
140 exmiddc 821 . . . . . . . 8 (DECID (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)) → ((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)) ∨ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))))
141139, 140syl 14 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → ((𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘)) ∨ ¬ (𝐹‘(𝑁𝑘)) ∈ (𝐹 “ (𝑁𝑘))))
142102, 138, 141mpjaodan 787 . . . . . 6 (((𝜑𝑘 ∈ ℕ0) ∧ (𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘))) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1))))
143142ex 114 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → ((𝐻𝑘):dom (𝐻𝑘)–1-1-onto→(𝐹 “ (𝑁𝑘)) → (𝐻‘(𝑘 + 1)):dom (𝐻‘(𝑘 + 1))–1-1-onto→(𝐹 “ (𝑁‘(𝑘 + 1)))))
144143expcom 115 . . . 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 9177 . 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 103   ↔ wb 104   ∨ wo 697  DECID wdc 819   = wceq 1331  ⊤wtru 1332   ∈ wcel 1480   ≠ wne 2308  ∀wral 2416  ∃wrex 2417   ∪ cun 3069   ∩ cin 3070   ⊆ wss 3071  ∅c0 3363  ifcif 3474  {csn 3527  ⟨cop 3530   ↦ cmpt 3989  Ord word 4284  suc csuc 4287  ωcom 4504  ◡ccnv 4538  dom cdm 4539   “ cima 4542   Fn wfn 5118  ⟶wf 5119  –onto→wfo 5121  –1-1-onto→wf1o 5122  ‘cfv 5123  (class class class)co 5774   ∈ cmpo 5776  freccfrec 6287   ↑pm cpm 6543  0cc0 7632  1c1 7633   + caddc 7635   − cmin 7945  ℕ0cn0 8989  ℤcz 9066  ℤ≥cuz 9338  seqcseq 10230 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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7723  ax-resscn 7724  ax-1cn 7725  ax-1re 7726  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-addcom 7732  ax-addass 7734  ax-distr 7736  ax-i2m1 7737  ax-0lt1 7738  ax-0id 7740  ax-rnegex 7741  ax-cnre 7743  ax-pre-ltirr 7744  ax-pre-ltwlin 7745  ax-pre-lttrn 7746  ax-pre-ltadd 7748 This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-pm 6545  df-pnf 7814  df-mnf 7815  df-xr 7816  df-ltxr 7817  df-le 7818  df-sub 7947  df-neg 7948  df-inn 8733  df-n0 8990  df-z 9067  df-uz 9339  df-seqfrec 10231 This theorem is referenced by:  ennnfonelemex  11938  ennnfonelemf1  11942  ennnfonelemrn  11943
 Copyright terms: Public domain W3C validator