![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ennnfonelemr | GIF version |
Description: Lemma for ennnfone 12451. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.) |
Ref | Expression |
---|---|
ennnfonelemr.dceq | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
ennnfonelemr.f | ⊢ (𝜑 → 𝐹:ℕ0–onto→𝐴) |
ennnfonelemr.n | ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗)) |
Ref | Expression |
---|---|
ennnfonelemr | ⊢ (𝜑 → 𝐴 ≈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ennnfonelemr.dceq | . . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) | |
2 | equequ1 1723 | . . . . 5 ⊢ (𝑥 = 𝑎 → (𝑥 = 𝑦 ↔ 𝑎 = 𝑦)) | |
3 | 2 | dcbid 839 | . . . 4 ⊢ (𝑥 = 𝑎 → (DECID 𝑥 = 𝑦 ↔ DECID 𝑎 = 𝑦)) |
4 | equequ2 1724 | . . . . 5 ⊢ (𝑦 = 𝑏 → (𝑎 = 𝑦 ↔ 𝑎 = 𝑏)) | |
5 | 4 | dcbid 839 | . . . 4 ⊢ (𝑦 = 𝑏 → (DECID 𝑎 = 𝑦 ↔ DECID 𝑎 = 𝑏)) |
6 | 3, 5 | cbvral2v 2731 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 DECID 𝑎 = 𝑏) |
7 | 1, 6 | sylib 122 | . 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 DECID 𝑎 = 𝑏) |
8 | ennnfonelemr.f | . 2 ⊢ (𝜑 → 𝐹:ℕ0–onto→𝐴) | |
9 | ennnfonelemr.n | . . 3 ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗)) | |
10 | fveq2 5531 | . . . . . . . . 9 ⊢ (𝑗 = 𝑓 → (𝐹‘𝑗) = (𝐹‘𝑓)) | |
11 | 10 | neeq2d 2379 | . . . . . . . 8 ⊢ (𝑗 = 𝑓 → ((𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ (𝐹‘𝑘) ≠ (𝐹‘𝑓))) |
12 | 11 | cbvralv 2718 | . . . . . . 7 ⊢ (∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∀𝑓 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑓)) |
13 | 12 | rexbii 2497 | . . . . . 6 ⊢ (∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∃𝑘 ∈ ℕ0 ∀𝑓 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑓)) |
14 | fveq2 5531 | . . . . . . . . 9 ⊢ (𝑘 = 𝑒 → (𝐹‘𝑘) = (𝐹‘𝑒)) | |
15 | 14 | neeq1d 2378 | . . . . . . . 8 ⊢ (𝑘 = 𝑒 → ((𝐹‘𝑘) ≠ (𝐹‘𝑓) ↔ (𝐹‘𝑒) ≠ (𝐹‘𝑓))) |
16 | 15 | ralbidv 2490 | . . . . . . 7 ⊢ (𝑘 = 𝑒 → (∀𝑓 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑓) ↔ ∀𝑓 ∈ (0...𝑛)(𝐹‘𝑒) ≠ (𝐹‘𝑓))) |
17 | 16 | cbvrexv 2719 | . . . . . 6 ⊢ (∃𝑘 ∈ ℕ0 ∀𝑓 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑓) ↔ ∃𝑒 ∈ ℕ0 ∀𝑓 ∈ (0...𝑛)(𝐹‘𝑒) ≠ (𝐹‘𝑓)) |
18 | 13, 17 | bitri 184 | . . . . 5 ⊢ (∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∃𝑒 ∈ ℕ0 ∀𝑓 ∈ (0...𝑛)(𝐹‘𝑒) ≠ (𝐹‘𝑓)) |
19 | 18 | ralbii 2496 | . . . 4 ⊢ (∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∀𝑛 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∀𝑓 ∈ (0...𝑛)(𝐹‘𝑒) ≠ (𝐹‘𝑓)) |
20 | oveq2 5900 | . . . . . . 7 ⊢ (𝑛 = 𝑑 → (0...𝑛) = (0...𝑑)) | |
21 | 20 | raleqdv 2692 | . . . . . 6 ⊢ (𝑛 = 𝑑 → (∀𝑓 ∈ (0...𝑛)(𝐹‘𝑒) ≠ (𝐹‘𝑓) ↔ ∀𝑓 ∈ (0...𝑑)(𝐹‘𝑒) ≠ (𝐹‘𝑓))) |
22 | 21 | rexbidv 2491 | . . . . 5 ⊢ (𝑛 = 𝑑 → (∃𝑒 ∈ ℕ0 ∀𝑓 ∈ (0...𝑛)(𝐹‘𝑒) ≠ (𝐹‘𝑓) ↔ ∃𝑒 ∈ ℕ0 ∀𝑓 ∈ (0...𝑑)(𝐹‘𝑒) ≠ (𝐹‘𝑓))) |
23 | 22 | cbvralv 2718 | . . . 4 ⊢ (∀𝑛 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∀𝑓 ∈ (0...𝑛)(𝐹‘𝑒) ≠ (𝐹‘𝑓) ↔ ∀𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∀𝑓 ∈ (0...𝑑)(𝐹‘𝑒) ≠ (𝐹‘𝑓)) |
24 | 19, 23 | bitri 184 | . . 3 ⊢ (∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0 ∀𝑗 ∈ (0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∀𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∀𝑓 ∈ (0...𝑑)(𝐹‘𝑒) ≠ (𝐹‘𝑓)) |
25 | 9, 24 | sylib 122 | . 2 ⊢ (𝜑 → ∀𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∀𝑓 ∈ (0...𝑑)(𝐹‘𝑒) ≠ (𝐹‘𝑓)) |
26 | oveq1 5899 | . . . 4 ⊢ (𝑐 = 𝑎 → (𝑐 + 1) = (𝑎 + 1)) | |
27 | 26 | cbvmptv 4114 | . . 3 ⊢ (𝑐 ∈ ℤ ↦ (𝑐 + 1)) = (𝑎 ∈ ℤ ↦ (𝑎 + 1)) |
28 | freceq1 6412 | . . 3 ⊢ ((𝑐 ∈ ℤ ↦ (𝑐 + 1)) = (𝑎 ∈ ℤ ↦ (𝑎 + 1)) → frec((𝑐 ∈ ℤ ↦ (𝑐 + 1)), 0) = frec((𝑎 ∈ ℤ ↦ (𝑎 + 1)), 0)) | |
29 | 27, 28 | ax-mp 5 | . 2 ⊢ frec((𝑐 ∈ ℤ ↦ (𝑐 + 1)), 0) = frec((𝑎 ∈ ℤ ↦ (𝑎 + 1)), 0) |
30 | 7, 8, 25, 29 | ennnfonelemnn0 12448 | 1 ⊢ (𝜑 → 𝐴 ≈ ℕ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 DECID wdc 835 = wceq 1364 ≠ wne 2360 ∀wral 2468 ∃wrex 2469 class class class wbr 4018 ↦ cmpt 4079 –onto→wfo 5230 ‘cfv 5232 (class class class)co 5892 freccfrec 6410 ≈ cen 6757 0cc0 7831 1c1 7832 + caddc 7834 ℕcn 8939 ℕ0cn0 9196 ℤcz 9273 ...cfz 10028 |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-setind 4551 ax-iinf 4602 ax-cnex 7922 ax-resscn 7923 ax-1cn 7924 ax-1re 7925 ax-icn 7926 ax-addcl 7927 ax-addrcl 7928 ax-mulcl 7929 ax-addcom 7931 ax-addass 7933 ax-distr 7935 ax-i2m1 7936 ax-0lt1 7937 ax-0id 7939 ax-rnegex 7940 ax-cnre 7942 ax-pre-ltirr 7943 ax-pre-ltwlin 7944 ax-pre-lttrn 7945 ax-pre-ltadd 7947 |
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 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4308 df-iord 4381 df-on 4383 df-ilim 4384 df-suc 4386 df-iom 4605 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-rn 4652 df-res 4653 df-ima 4654 df-iota 5193 df-fun 5234 df-fn 5235 df-f 5236 df-f1 5237 df-fo 5238 df-f1o 5239 df-fv 5240 df-riota 5848 df-ov 5895 df-oprab 5896 df-mpo 5897 df-1st 6160 df-2nd 6161 df-recs 6325 df-frec 6411 df-er 6554 df-pm 6670 df-en 6760 df-pnf 8014 df-mnf 8015 df-xr 8016 df-ltxr 8017 df-le 8018 df-sub 8150 df-neg 8151 df-inn 8940 df-n0 9197 df-z 9274 df-uz 9549 df-fz 10029 df-seqfrec 10466 |
This theorem is referenced by: ennnfone 12451 |
Copyright terms: Public domain | W3C validator |