![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fival | Structured version Visualization version GIF version |
Description: The set of all the finite intersections of the elements of 𝐴. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
Ref | Expression |
---|---|
fival | ⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fi 8726 | . 2 ⊢ fi = (𝑧 ∈ V ↦ {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑦 = ∩ 𝑥}) | |
2 | pweq 4460 | . . . . 5 ⊢ (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴) | |
3 | 2 | ineq1d 4112 | . . . 4 ⊢ (𝑧 = 𝐴 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝐴 ∩ Fin)) |
4 | 3 | rexeqdv 3376 | . . 3 ⊢ (𝑧 = 𝐴 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑦 = ∩ 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥)) |
5 | 4 | abbidv 2860 | . 2 ⊢ (𝑧 = 𝐴 → {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑦 = ∩ 𝑥} = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) |
6 | elex 3455 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
7 | simpr 485 | . . . . . . 7 ⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩ 𝑥) → 𝑦 = ∩ 𝑥) | |
8 | elinel1 4097 | . . . . . . . . 9 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) | |
9 | 8 | elpwid 4469 | . . . . . . . 8 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴) |
10 | eqvisset 3454 | . . . . . . . . 9 ⊢ (𝑦 = ∩ 𝑥 → ∩ 𝑥 ∈ V) | |
11 | intex 5136 | . . . . . . . . 9 ⊢ (𝑥 ≠ ∅ ↔ ∩ 𝑥 ∈ V) | |
12 | 10, 11 | sylibr 235 | . . . . . . . 8 ⊢ (𝑦 = ∩ 𝑥 → 𝑥 ≠ ∅) |
13 | intssuni2 4811 | . . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∩ 𝑥 ⊆ ∪ 𝐴) | |
14 | 9, 12, 13 | syl2an 595 | . . . . . . 7 ⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩ 𝑥) → ∩ 𝑥 ⊆ ∪ 𝐴) |
15 | 7, 14 | eqsstrd 3930 | . . . . . 6 ⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩ 𝑥) → 𝑦 ⊆ ∪ 𝐴) |
16 | selpw 4464 | . . . . . 6 ⊢ (𝑦 ∈ 𝒫 ∪ 𝐴 ↔ 𝑦 ⊆ ∪ 𝐴) | |
17 | 15, 16 | sylibr 235 | . . . . 5 ⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩ 𝑥) → 𝑦 ∈ 𝒫 ∪ 𝐴) |
18 | 17 | rexlimiva 3244 | . . . 4 ⊢ (∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥 → 𝑦 ∈ 𝒫 ∪ 𝐴) |
19 | 18 | abssi 3971 | . . 3 ⊢ {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ⊆ 𝒫 ∪ 𝐴 |
20 | uniexg 7330 | . . . 4 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
21 | 20 | pwexd 5176 | . . 3 ⊢ (𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴 ∈ V) |
22 | ssexg 5123 | . . 3 ⊢ (({𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ⊆ 𝒫 ∪ 𝐴 ∧ 𝒫 ∪ 𝐴 ∈ V) → {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ∈ V) | |
23 | 19, 21, 22 | sylancr 587 | . 2 ⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ∈ V) |
24 | 1, 5, 6, 23 | fvmptd3 6662 | 1 ⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2081 {cab 2775 ≠ wne 2984 ∃wrex 3106 Vcvv 3437 ∩ cin 3862 ⊆ wss 3863 ∅c0 4215 𝒫 cpw 4457 ∪ cuni 4749 ∩ cint 4786 ‘cfv 6230 Fincfn 8362 ficfi 8725 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3710 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-int 4787 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-iota 6194 df-fun 6232 df-fv 6238 df-fi 8726 |
This theorem is referenced by: elfi 8728 fi0 8735 |
Copyright terms: Public domain | W3C validator |