Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) using conjunction-form virtual hypothesis collections. It was completed automatically by a tools program which would invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimpcf is sspwimpcfVD without virtual deductions and was derived from sspwimpcfVD . The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)
1:: | |- (. A C_ B ->. A C_ B ). |
2:: | |- (. ........... x e. ~P A ->. x e. ~P A ). |
3:2: | |- (. ........... x e. ~P A ->. x C_ A ). |
4:3,1: | |- (. (. A C_ B ,. x e. ~P A ). ->. x C_ B ). |
5:: | |- x e.V |
6:4,5: | |- (. (. A C B ,. x e. ~P A ). ->. x e. ~P B ). |
7:6: | |- (. A C_ B ->. ( x e. ~P A -> x e. ~P B ) ). |
8:7: | |- (. A C_ B ->. A. x ( x e. ~P A -> x e. ~P B ) ). |
9:8: | |- (. A C_ B ->. ~P A C_ ~P B ). |
qed:9: | |- ( A C_ B -> ~P A C_ ~P B ) |
Ref | Expression | ||
---|---|---|---|
Assertion | sspwimpcfVD | ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | ⊢ 𝑥 ∈ V | |
2 | idn1 | ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝐴 ⊆ 𝐵 ) | |
3 | idn1 | ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ∈ 𝒫 𝐴 ) | |
4 | elpwi | ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 ) | |
5 | 3 4 | el1 | ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ⊆ 𝐴 ) |
6 | sstr2 | ⊢ ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵 ) ) | |
7 | 6 | impcom | ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ⊆ 𝐵 ) |
8 | 2 5 7 | el12 | ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ⊆ 𝐵 ) |
9 | elpwg | ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 ) ) | |
10 | 9 | biimpar | ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ⊆ 𝐵 ) → 𝑥 ∈ 𝒫 𝐵 ) |
11 | 1 8 10 | el021old | ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ∈ 𝒫 𝐵 ) |
12 | 11 | int2 | ⊢ ( 𝐴 ⊆ 𝐵 ▶ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) ) |
13 | 12 | gen11 | ⊢ ( 𝐴 ⊆ 𝐵 ▶ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) ) |
14 | dfss2 | ⊢ ( 𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) ) | |
15 | 14 | biimpri | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵 ) → 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |
16 | 13 15 | el1 | ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |
17 | 16 | in1 | ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |