Theorem mresspw 14653

Description: A Moore collection is a subset of the power of the base set; each closed subset of the system is actually a subset of the base. (Contributed by Stefan O'Rear, 30-Jan-2015.)

Assertion

Ref	Expression
mresspw	|- ( C e. (Moore ` X ) -> C C_ ~P X )

Proof of Theorem mresspw

Dummy variable s is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ismre 14651	. 2 |- ( C e. (Moore ` X ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) )
2	1	simp1bi 1003	1 |- ( C e. (Moore ` X ) -> C C_ ~P X )

Syntax hints:   -> wi 4   e. wcel 1758   =/= wne 2648   A.wral 2799   C_ wss 3439   (/)c0 3748   ~Pcpw 3971   |^|cint 4239   ` cfv 5529  Moorecmre 14643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-iota 5492  df-fun 5531  df-fv 5537  df-mre 14647

This theorem is referenced by:  mress  14654  mrerintcl  14658  mreuni  14661  mremre  14665  isacs2  14714  mreacs  14719  isacs3lem  15459  dmdprdd  16613  dprdfeq0  16644  dprdfeq0OLD  16651  dprdss  16658  dprdz  16659  subgdmdprd  16663  subgdprd  16664  dprd2dlem1  16672  dprd2da  16673  dmdprdsplit2lem  16676  mretopd  18838  ismrc  29208