pwexg - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > pwexg		GIF version

Theorem pwexg 4328

Description: The power class of a set is a set. (Contributed by SF, 21-Jan-2015.)

**Assertion**
Ref	Expression
pwexg	⊢ (A ∈ V → ℘A ∈ V)

**Proof of Theorem pwexg**
Step	Hyp	Ref	Expression
1		dfpw2 4327	. 2 ⊢ ℘A = ∼ (( S_k ∖ (℘₁A ×_k V)) “_k 1_c)
2		ssetkex 4294	. . . . 5 ⊢ S_k ∈ V
3		pw1exg 4302	. . . . . 6 ⊢ (A ∈ V → ℘₁A ∈ V)
4		vvex 4109	. . . . . 6 ⊢ V ∈ V
5		xpkexg 4288	. . . . . 6 ⊢ ((℘₁A ∈ V ∧ V ∈ V) → (℘₁A ×_k V) ∈ V)
6	3, 4, 5	sylancl 643	. . . . 5 ⊢ (A ∈ V → (℘₁A ×_k V) ∈ V)
7		difexg 4102	. . . . 5 ⊢ (( S_k ∈ V ∧ (℘₁A ×_k V) ∈ V) → ( S_k ∖ (℘₁A ×_k V)) ∈ V)
8	2, 6, 7	sylancr 644	. . . 4 ⊢ (A ∈ V → ( S_k ∖ (℘₁A ×_k V)) ∈ V)
9		1cex 4142	. . . 4 ⊢ 1_c ∈ V
10		imakexg 4299	. . . 4 ⊢ ((( S_k ∖ (℘₁A ×_k V)) ∈ V ∧ 1_c ∈ V) → (( S_k ∖ (℘₁A ×_k V)) “_k 1_c) ∈ V)
11	8, 9, 10	sylancl 643	. . 3 ⊢ (A ∈ V → (( S_k ∖ (℘₁A ×_k V)) “_k 1_c) ∈ V)
12		complexg 4099	. . 3 ⊢ ((( S_k ∖ (℘₁A ×_k V)) “_k 1_c) ∈ V → ∼ (( S_k ∖ (℘₁A ×_k V)) “_k 1_c) ∈ V)
13	11, 12	syl 15	. 2 ⊢ (A ∈ V → ∼ (( S_k ∖ (℘₁A ×_k V)) “_k 1_c) ∈ V)
14	1, 13	syl5eqel 2437	1 ⊢ (A ∈ V → ℘A ∈ V)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 1710 Vcvv 2859 ∼ ccompl 3205 ∖ cdif 3206 ℘cpw 3722 1_cc1c 4134 ℘₁cpw1 4135 ×_k cxpk 4174 “_k cimak 4179 S_k cssetk 4183

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4078 ax-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-typlower 4086 ax-sn 4087

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-ss 3259 df-nul 3551 df-pw 3724 df-sn 3741 df-pr 3742 df-opk 4058 df-1c 4136 df-pw1 4137 df-xpk 4185 df-cnvk 4186 df-imak 4189 df-p6 4191 df-sik 4192 df-ssetk 4193

This theorem is referenced by: pwex 4329 pmex 6005 ltcpw1pwg 6202

W3C validator