pwexg - New Foundations Explorer

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

Theorem pwexg 4329

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 4328	. 2 ⊢ ℘A = ∼ (( S_k ∖ (℘₁A ×_k V)) “_k 1_c)
2		ssetkex 4295	. . . . 5 ⊢ S_k ∈ V
3		pw1exg 4303	. . . . . 6 ⊢ (A ∈ V → ℘₁A ∈ V)
4		vvex 4110	. . . . . 6 ⊢ V ∈ V
5		xpkexg 4289	. . . . . 6 ⊢ ((℘₁A ∈ V ∧ V ∈ V) → (℘₁A ×_k V) ∈ V)
6	3, 4, 5	sylancl 643	. . . . 5 ⊢ (A ∈ V → (℘₁A ×_k V) ∈ V)
7		difexg 4103	. . . . 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 4143	. . . 4 ⊢ 1_c ∈ V
10		imakexg 4300	. . . 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 4100	. . 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

This proof depends on syntax axioms: → wi 4 ∈ wcel 1710 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ℘cpw 3723 1_cc1c 4135 ℘₁cpw1 4136 ×_k cxpk 4175 “_k cimak 4180 S_k cssetk 4184

This proof depends on 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 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-typlower 4087 ax-sn 4088

This proof 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 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-v 2862 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-ss 3260 df-nul 3552 df-pw 3725 df-sn 3742 df-pr 3743 df-opk 4059 df-1c 4137 df-pw1 4138 df-xpk 4186 df-cnvk 4187 df-imak 4190 df-p6 4192 df-sik 4193 df-ssetk 4194

This theorem is used by: pwex 4330 pmex 6006 ltcpw1pwg 6203

W3C validator