![]() |
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 43101)
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 43450 is sspwimpVD 43451 without virtual deductions and was derived
from sspwimpVD 43451. (Contributed by Alan Sare, 23-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
Ref | Expression |
---|---|
sspwimpVD | ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3477 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
2 | 1 | vd01 43129 | . . . . . 6 ⊢ ( ⊤ ▶ 𝑥 ∈ V ) |
3 | idn1 43106 | . . . . . . 7 ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝐴 ⊆ 𝐵 ) | |
4 | idn1 43106 | . . . . . . . 8 ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ∈ 𝒫 𝐴 ) | |
5 | elpwi 4603 | . . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) | |
6 | 4, 5 | el1 43160 | . . . . . . 7 ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ⊆ 𝐴 ) |
7 | sstr 3986 | . . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 𝑥 ⊆ 𝐵) | |
8 | 7 | ancoms 459 | . . . . . . 7 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → 𝑥 ⊆ 𝐵) |
9 | 3, 6, 8 | el12 43258 | . . . . . 6 ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ⊆ 𝐵 ) |
10 | 2, 9 | elpwgdedVD 43449 | . . . . . 6 ⊢ ( ( ⊤ , ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ) ▶ 𝑥 ∈ 𝒫 𝐵 ) |
11 | 2, 9, 10 | un0.1 43311 | . . . . 5 ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ∈ 𝒫 𝐵 ) |
12 | 11 | int2 43138 | . . . 4 ⊢ ( 𝐴 ⊆ 𝐵 ▶ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) ) |
13 | 12 | gen11 43148 | . . 3 ⊢ ( 𝐴 ⊆ 𝐵 ▶ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) ) |
14 | dfss2 3964 | . . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)) | |
15 | 14 | biimpri 227 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
16 | 13, 15 | el1 43160 | . 2 ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |
17 | 16 | in1 43103 | 1 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 ⊤wtru 1542 ∈ wcel 2106 Vcvv 3473 ⊆ wss 3944 𝒫 cpw 4596 ( wvhc2 43112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3951 df-ss 3961 df-pw 4598 df-vd1 43102 df-vhc2 43113 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |