Description: The powerclass construction preserves and reflects inclusion. Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of TakeutiZaring p. 18. (Contributed by NM, 13-Oct-1996)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sspwb | ⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sspw | ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 ) | |
| 2 | ssel | ⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 → ( { 𝑥 } ∈ 𝒫 𝐴 → { 𝑥 } ∈ 𝒫 𝐵 ) ) | |
| 3 | vsnex | ⊢ { 𝑥 } ∈ V | |
| 4 | 3 | elpw | ⊢ ( { 𝑥 } ∈ 𝒫 𝐴 ↔ { 𝑥 } ⊆ 𝐴 ) |
| 5 | vex | ⊢ 𝑥 ∈ V | |
| 6 | 5 | snss | ⊢ ( 𝑥 ∈ 𝐴 ↔ { 𝑥 } ⊆ 𝐴 ) |
| 7 | 4 6 | bitr4i | ⊢ ( { 𝑥 } ∈ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴 ) |
| 8 | 3 | elpw | ⊢ ( { 𝑥 } ∈ 𝒫 𝐵 ↔ { 𝑥 } ⊆ 𝐵 ) |
| 9 | 5 | snss | ⊢ ( 𝑥 ∈ 𝐵 ↔ { 𝑥 } ⊆ 𝐵 ) |
| 10 | 8 9 | bitr4i | ⊢ ( { 𝑥 } ∈ 𝒫 𝐵 ↔ 𝑥 ∈ 𝐵 ) |
| 11 | 2 7 10 | 3imtr3g | ⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) |
| 12 | 11 | ssrdv | ⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 → 𝐴 ⊆ 𝐵 ) |
| 13 | 1 12 | impbii | ⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |