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 https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sspwimpALT2 | ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | ⊢ 𝑥 ∈ V | |
| 2 | elpwi | ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 ) | |
| 3 | id | ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ 𝐵 ) | |
| 4 | 2 3 | sylan9ssr | ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ⊆ 𝐵 ) |
| 5 | elpwg | ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 ) ) | |
| 6 | 5 | biimpar | ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ∈ 𝒫 𝐵 ) |
| 7 | 1 4 6 | sylancr | ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ∈ 𝒫 𝐵 ) |
| 8 | 7 | ex | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) ) |
| 9 | 8 | ssrdv | ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |