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 41814)
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 42163 is sspwimpVD 42164 without virtual deductions and was derived
from sspwimpVD 42164. (Contributed by Alan Sare, 23-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
Ref | Expression |
---|---|
sspwimpVD | ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3405 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
2 | 1 | vd01 41842 | . . . . . 6 ⊢ ( ⊤ ▶ 𝑥 ∈ V ) |
3 | idn1 41819 | . . . . . . 7 ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝐴 ⊆ 𝐵 ) | |
4 | idn1 41819 | . . . . . . . 8 ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ∈ 𝒫 𝐴 ) | |
5 | elpwi 4512 | . . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) | |
6 | 4, 5 | el1 41873 | . . . . . . 7 ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ⊆ 𝐴 ) |
7 | sstr 3899 | . . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 𝑥 ⊆ 𝐵) | |
8 | 7 | ancoms 462 | . . . . . . 7 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → 𝑥 ⊆ 𝐵) |
9 | 3, 6, 8 | el12 41971 | . . . . . 6 ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ⊆ 𝐵 ) |
10 | 2, 9 | elpwgdedVD 42162 | . . . . . 6 ⊢ ( ( ⊤ , ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ) ▶ 𝑥 ∈ 𝒫 𝐵 ) |
11 | 2, 9, 10 | un0.1 42024 | . . . . 5 ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ∈ 𝒫 𝐵 ) |
12 | 11 | int2 41851 | . . . 4 ⊢ ( 𝐴 ⊆ 𝐵 ▶ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) ) |
13 | 12 | gen11 41861 | . . 3 ⊢ ( 𝐴 ⊆ 𝐵 ▶ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) ) |
14 | dfss2 3877 | . . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)) | |
15 | 14 | biimpri 231 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
16 | 13, 15 | el1 41873 | . 2 ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |
17 | 16 | in1 41816 | 1 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1541 ⊤wtru 1544 ∈ wcel 2110 Vcvv 3401 ⊆ wss 3857 𝒫 cpw 4503 ( wvhc2 41825 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2706 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2713 df-cleq 2726 df-clel 2812 df-v 3403 df-in 3864 df-ss 3874 df-pw 4505 df-vd1 41815 df-vhc2 41826 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |