| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > infcvgaux1i | Structured version Visualization version GIF version | ||
| Description: Auxiliary theorem for applications of supcvg 15933. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.) |
| Ref | Expression |
|---|---|
| infcvg.1 | ⊢ 𝑅 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} |
| infcvg.2 | ⊢ (𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ) |
| infcvg.3 | ⊢ 𝑍 ∈ 𝑋 |
| infcvg.4 | ⊢ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 |
| Ref | Expression |
|---|---|
| infcvgaux1i | ⊢ (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | infcvg.1 | . . 3 ⊢ 𝑅 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} | |
| 2 | infcvg.2 | . . . . . . 7 ⊢ (𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ) | |
| 3 | 2 | renegcld 11656 | . . . . . 6 ⊢ (𝑦 ∈ 𝑋 → -𝐴 ∈ ℝ) |
| 4 | eleq1 2853 | . . . . . 6 ⊢ (𝑥 = -𝐴 → (𝑥 ∈ ℝ ↔ -𝐴 ∈ ℝ)) | |
| 5 | 3, 4 | syl5ibrcom 250 | . . . . 5 ⊢ (𝑦 ∈ 𝑋 → (𝑥 = -𝐴 → 𝑥 ∈ ℝ)) |
| 6 | 5 | rexlimiv 3161 | . . . 4 ⊢ (∃𝑦 ∈ 𝑋 𝑥 = -𝐴 → 𝑥 ∈ ℝ) |
| 7 | 6 | abssi 4023 | . . 3 ⊢ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} ⊆ ℝ |
| 8 | 1, 7 | eqsstri 3984 | . 2 ⊢ 𝑅 ⊆ ℝ |
| 9 | infcvg.3 | . . . . . 6 ⊢ 𝑍 ∈ 𝑋 | |
| 10 | eqid 2765 | . . . . . 6 ⊢ -⦋𝑍 / 𝑦⦌𝐴 = -⦋𝑍 / 𝑦⦌𝐴 | |
| 11 | 10 | nfth 1834 | . . . . . . 7 ⊢ Ⅎ𝑦-⦋𝑍 / 𝑦⦌𝐴 = -⦋𝑍 / 𝑦⦌𝐴 |
| 12 | csbeq1a 3868 | . . . . . . . . 9 ⊢ (𝑦 = 𝑍 → 𝐴 = ⦋𝑍 / 𝑦⦌𝐴) | |
| 13 | 12 | negeqd 11466 | . . . . . . . 8 ⊢ (𝑦 = 𝑍 → -𝐴 = -⦋𝑍 / 𝑦⦌𝐴) |
| 14 | 13 | eqeq2d 2776 | . . . . . . 7 ⊢ (𝑦 = 𝑍 → (-⦋𝑍 / 𝑦⦌𝐴 = -𝐴 ↔ -⦋𝑍 / 𝑦⦌𝐴 = -⦋𝑍 / 𝑦⦌𝐴)) |
| 15 | 11, 14 | rspce 3572 | . . . . . 6 ⊢ ((𝑍 ∈ 𝑋 ∧ -⦋𝑍 / 𝑦⦌𝐴 = -⦋𝑍 / 𝑦⦌𝐴) → ∃𝑦 ∈ 𝑋 -⦋𝑍 / 𝑦⦌𝐴 = -𝐴) |
| 16 | 9, 10, 15 | mp2an 705 | . . . . 5 ⊢ ∃𝑦 ∈ 𝑋 -⦋𝑍 / 𝑦⦌𝐴 = -𝐴 |
| 17 | negex 11470 | . . . . . 6 ⊢ -⦋𝑍 / 𝑦⦌𝐴 ∈ V | |
| 18 | nfcsb1v 3878 | . . . . . . . . 9 ⊢ Ⅎ𝑦⦋𝑍 / 𝑦⦌𝐴 | |
| 19 | 18 | nfneg 11468 | . . . . . . . 8 ⊢ Ⅎ𝑦-⦋𝑍 / 𝑦⦌𝐴 |
| 20 | 19 | nfeq2 2944 | . . . . . . 7 ⊢ Ⅎ𝑦 𝑥 = -⦋𝑍 / 𝑦⦌𝐴 |
| 21 | eqeq1 2769 | . . . . . . 7 ⊢ (𝑥 = -⦋𝑍 / 𝑦⦌𝐴 → (𝑥 = -𝐴 ↔ -⦋𝑍 / 𝑦⦌𝐴 = -𝐴)) | |
| 22 | 20, 21 | rexbid 3281 | . . . . . 6 ⊢ (𝑥 = -⦋𝑍 / 𝑦⦌𝐴 → (∃𝑦 ∈ 𝑋 𝑥 = -𝐴 ↔ ∃𝑦 ∈ 𝑋 -⦋𝑍 / 𝑦⦌𝐴 = -𝐴)) |
| 23 | 17, 22 | elab 3640 | . . . . 5 ⊢ (-⦋𝑍 / 𝑦⦌𝐴 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} ↔ ∃𝑦 ∈ 𝑋 -⦋𝑍 / 𝑦⦌𝐴 = -𝐴) |
| 24 | 16, 23 | mpbir 234 | . . . 4 ⊢ -⦋𝑍 / 𝑦⦌𝐴 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = -𝐴} |
| 25 | 24, 1 | eleqtrri 2864 | . . 3 ⊢ -⦋𝑍 / 𝑦⦌𝐴 ∈ 𝑅 |
| 26 | 25 | ne0ii 4297 | . 2 ⊢ 𝑅 ≠ ∅ |
| 27 | infcvg.4 | . 2 ⊢ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 | |
| 28 | 8, 26, 27 | 3pm3.2i 1358 | 1 ⊢ (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑤 ≤ 𝑧) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 {cab 2743 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 ⦋csb 3854 ⊆ wss 3906 ∅c0 4286 class class class wbr 5111 ℝcr 11114 ≤ cle 11259 -cneg 11457 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-po 5571 df-so 5572 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-pnf 11260 df-mnf 11261 df-ltxr 11263 df-sub 11458 df-neg 11459 |
| This theorem is used by: infcvgaux2i 15935 |
| Copyright terms: Public domain | W3C validator |