Description: If a class is a subclass of another class, then its power class is a
subclass of that other class's power class. Left-to-right implication
of Exercise 18 of [TakeutiZaring] p. 18. Proof derived by
completeusersproof.c from User's Proof in VirtualDeductionProofs.txt.
The User's Proof in html format is displayed in
http://www.virtualdeduction.com/sspwimpaltvd.html. (Contributed by
Alan Sare, 11-Sep-2016.)
Assertion
| Ref
| Expression |
|---|
| sspwimpALT2VD |
⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
Proof of Theorem sspwimpALT2VD
| Step | Hyp | Expression |
|---|
| 1 | | ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝐴 ⊆ 𝐵 )
| | 2 | | ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ∈ 𝒫 𝐴 )
| | 3 | 2 | ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ⊆ 𝐴 )
| | 4 | 3,1 | ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ⊆ 𝐵 )
| | 5 | | ⊢ 𝑥 ∈ V
| | 6 | 4,5 | ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ∈ 𝒫 𝐵 )
| | 7 | 6 | ⊢ ( 𝐴 ⊆ 𝐵 ▶ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) )
| | 8 | 7 | ⊢ ( 𝐴 ⊆ 𝐵 ▶ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) )
| | 9 | 8 | ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝒫 𝐴 ⊆ 𝒫 𝐵 )
| | qed | 9 | ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
| |