Theorem sspwimpVD 44135

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 43785) 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 44134 is sspwimpVD 44135 without virtual deductions and was derived from sspwimpVD 44135. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
2::	⊢ (   .............. 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ∈ 𝒫 𝐴   )
3:2:	⊢ (   .............. 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ⊆ 𝐴   )
4:3,1:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
5::	⊢ 𝑥 ∈ V
6:4,5:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵    )
7:6:	⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)    )
8:7:	⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
9:8:	⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
qed:9:	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Assertion

Ref	Expression
sspwimpVD	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Proof of Theorem sspwimpVD

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3470	. . . . . . 7 ⊢ 𝑥 ∈ V
2	1	vd01 43813	. . . . . 6 ⊢ (   ⊤   ▶   𝑥 ∈ V   )
3		idn1 43790	. . . . . . 7 ⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
4		idn1 43790	. . . . . . . 8 ⊢ (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ∈ 𝒫 𝐴   )
5		elpwi 4601	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
6	4, 5	el1 43844	. . . . . . 7 ⊢ (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ⊆ 𝐴   )
7		sstr 3982	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 𝑥 ⊆ 𝐵)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → 𝑥 ⊆ 𝐵)
9	3, 6, 8	el12 43942	. . . . . 6 ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
10	2, 9	elpwgdedVD 44133	. . . . . 6 ⊢ (   (   ⊤   ,   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   )   ▶   𝑥 ∈ 𝒫 𝐵   )
11	2, 9, 10	un0.1 43995	. . . . 5 ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵   )
12	11	int2 43822	. . . 4 ⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
13	12	gen11 43832	. . 3 ⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
14		dfss2 3960	. . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵))
15	14	biimpri 227	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵)
16	13, 15	el1 43844	. 2 ⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
17	16	in1 43787	1 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Syntax hints:   → wi 4  ∀wal 1531  ⊤wtru 1534   ∈ wcel 2098  Vcvv 3466   ⊆ wss 3940  𝒫 cpw 4594  (   wvhc2 43796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957  df-pw 4596  df-vd1 43786  df-vhc2 43797

This theorem is referenced by: (None)