![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cc4n | GIF version |
Description: Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7169, the hypotheses only require an A(n) for each value of 𝑛, not a single set 𝐴 which suffices for every 𝑛 ∈ ω. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.) |
Ref | Expression |
---|---|
cc4n.cc | ⊢ (𝜑 → CCHOICE) |
cc4n.1 | ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ 𝑉) |
cc4n.2 | ⊢ (𝜑 → 𝑁 ≈ ω) |
cc4n.3 | ⊢ (𝑥 = (𝑓‘𝑛) → (𝜓 ↔ 𝜒)) |
cc4n.m | ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑥 ∈ 𝐴 𝜓) |
Ref | Expression |
---|---|
cc4n | ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cc4n.cc | . . 3 ⊢ (𝜑 → CCHOICE) | |
2 | cc4n.1 | . . . 4 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ 𝑉) | |
3 | elex 2720 | . . . . 5 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V) | |
4 | 3 | ralimi 2517 | . . . 4 ⊢ (∀𝑛 ∈ 𝑁 {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ 𝑉 → ∀𝑛 ∈ 𝑁 {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V) |
5 | 2, 4 | syl 14 | . . 3 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V) |
6 | cc4n.m | . . . 4 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑥 ∈ 𝐴 𝜓) | |
7 | rabn0m 3417 | . . . . 5 ⊢ (∃𝑤 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∃𝑥 ∈ 𝐴 𝜓) | |
8 | 7 | ralbii 2460 | . . . 4 ⊢ (∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ∀𝑛 ∈ 𝑁 ∃𝑥 ∈ 𝐴 𝜓) |
9 | 6, 8 | sylibr 133 | . . 3 ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∃𝑤 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) |
10 | cc4n.2 | . . 3 ⊢ (𝜑 → 𝑁 ≈ ω) | |
11 | 1, 5, 9, 10 | cc3 7167 | . 2 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜓})) |
12 | simprl 521 | . . . . 5 ⊢ ((𝜑 ∧ (𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜓})) → 𝑓 Fn 𝑁) | |
13 | cc4n.3 | . . . . . . . . 9 ⊢ (𝑥 = (𝑓‘𝑛) → (𝜓 ↔ 𝜒)) | |
14 | 13 | elrab 2864 | . . . . . . . 8 ⊢ ((𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} ↔ ((𝑓‘𝑛) ∈ 𝐴 ∧ 𝜒)) |
15 | 14 | simprbi 273 | . . . . . . 7 ⊢ ((𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} → 𝜒) |
16 | 15 | ralimi 2517 | . . . . . 6 ⊢ (∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜓} → ∀𝑛 ∈ 𝑁 𝜒) |
17 | 16 | ad2antll 483 | . . . . 5 ⊢ ((𝜑 ∧ (𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜓})) → ∀𝑛 ∈ 𝑁 𝜒) |
18 | 12, 17 | jca 304 | . . . 4 ⊢ ((𝜑 ∧ (𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜓})) → (𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 𝜒)) |
19 | 18 | ex 114 | . . 3 ⊢ (𝜑 → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) → (𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 𝜒))) |
20 | 19 | eximdv 1857 | . 2 ⊢ (𝜑 → (∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜓}) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 𝜒))) |
21 | 11, 20 | mpd 13 | 1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1332 ∃wex 1469 ∈ wcel 2125 ∀wral 2432 ∃wrex 2433 {crab 2436 Vcvv 2709 class class class wbr 3961 ωcom 4543 Fn wfn 5158 ‘cfv 5163 ≈ cen 6672 CCHOICEwacc 7161 |
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-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-coll 4075 ax-sep 4078 ax-pow 4130 ax-pr 4164 ax-un 4388 ax-iinf 4541 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1335 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ral 2437 df-rex 2438 df-reu 2439 df-rab 2441 df-v 2711 df-sbc 2934 df-csb 3028 df-un 3102 df-in 3104 df-ss 3111 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-int 3804 df-iun 3847 df-br 3962 df-opab 4022 df-mpt 4023 df-id 4248 df-iom 4544 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-rn 4590 df-res 4591 df-ima 4592 df-iota 5128 df-fun 5165 df-fn 5166 df-f 5167 df-f1 5168 df-fo 5169 df-f1o 5170 df-fv 5171 df-2nd 6079 df-er 6469 df-en 6675 df-cc 7162 |
This theorem is referenced by: omctfn 12123 |
Copyright terms: Public domain | W3C validator |