| Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > sspwimpVD | Structured version Visualization version GIF version | ||
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 44589)
using conjunction-form virtual hypothesis collections. It was completed
manually, but has the potential to be completed automatically by a tools
program which would invoke Mel L. O'Cat's mmj2 and Norm Megill's
Metamath Proof Assistant.
sspwimp 44938 is sspwimpVD 44939 without virtual deductions and was derived
from sspwimpVD 44939. (Contributed by Alan Sare, 23-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
| Ref | Expression |
|---|---|
| sspwimpVD | ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex 3484 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
| 2 | 1 | vd01 44617 | . . . . . 6 ⊢ ( ⊤ ▶ 𝑥 ∈ V ) |
| 3 | idn1 44594 | . . . . . . 7 ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝐴 ⊆ 𝐵 ) | |
| 4 | idn1 44594 | . . . . . . . 8 ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ∈ 𝒫 𝐴 ) | |
| 5 | elpwi 4607 | . . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) | |
| 6 | 4, 5 | el1 44648 | . . . . . . 7 ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ⊆ 𝐴 ) |
| 7 | sstr 3992 | . . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 𝑥 ⊆ 𝐵) | |
| 8 | 7 | ancoms 458 | . . . . . . 7 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → 𝑥 ⊆ 𝐵) |
| 9 | 3, 6, 8 | el12 44746 | . . . . . 6 ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ⊆ 𝐵 ) |
| 10 | 2, 9 | elpwgdedVD 44937 | . . . . . 6 ⊢ ( ( ⊤ , ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ) ▶ 𝑥 ∈ 𝒫 𝐵 ) |
| 11 | 2, 9, 10 | un0.1 44799 | . . . . 5 ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ∈ 𝒫 𝐵 ) |
| 12 | 11 | int2 44626 | . . . 4 ⊢ ( 𝐴 ⊆ 𝐵 ▶ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) ) |
| 13 | 12 | gen11 44636 | . . 3 ⊢ ( 𝐴 ⊆ 𝐵 ▶ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) ) |
| 14 | df-ss 3968 | . . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)) | |
| 15 | 14 | biimpri 228 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
| 16 | 13, 15 | el1 44648 | . 2 ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |
| 17 | 16 | in1 44591 | 1 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ⊤wtru 1541 ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 𝒫 cpw 4600 ( wvhc2 44600 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-pw 4602 df-vd1 44590 df-vhc2 44601 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |