Metamath Proof Explorer

Theorem mremre

Description: The Moore collections of subsets of a space, viewed as a kind of subset of the power set, form a Moore collection in their own right on the power set. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion mremre 
|- ( X e. V -> ( Moore ` X ) e. ( Moore ` ~P X ) )

Proof

Step Hyp Ref Expression
1 mresspw 
 |-  ( a e. ( Moore ` X ) -> a C_ ~P X )
2 velpw 
 |-  ( a e. ~P ~P X <-> a C_ ~P X )
3 1 2 sylibr 
 |-  ( a e. ( Moore ` X ) -> a e. ~P ~P X )
4 3 ssriv 
 |-  ( Moore ` X ) C_ ~P ~P X
5 4 a1i 
 |-  ( X e. V -> ( Moore ` X ) C_ ~P ~P X )
6 ssidd 
 |-  ( X e. V -> ~P X C_ ~P X )
7 pwidg 
 |-  ( X e. V -> X e. ~P X )
8 intssuni2 
 |-  ( ( a C_ ~P X /\ a =/= (/) ) -> |^| a C_ U. ~P X )
9 8 3adant1 
 |-  ( ( X e. V /\ a C_ ~P X /\ a =/= (/) ) -> |^| a C_ U. ~P X )
10 unipw 
 |-  U. ~P X = X
11 9 10 sseqtrdi 
 |-  ( ( X e. V /\ a C_ ~P X /\ a =/= (/) ) -> |^| a C_ X )
12 elpw2g 
 |-  ( X e. V -> ( |^| a e. ~P X <-> |^| a C_ X ) )
13 12 3ad2ant1 
 |-  ( ( X e. V /\ a C_ ~P X /\ a =/= (/) ) -> ( |^| a e. ~P X <-> |^| a C_ X ) )
14 11 13 mpbird 
 |-  ( ( X e. V /\ a C_ ~P X /\ a =/= (/) ) -> |^| a e. ~P X )
15 6 7 14 ismred 
 |-  ( X e. V -> ~P X e. ( Moore ` X ) )
16 n0 
 |-  ( a =/= (/) <-> E. b b e. a )
17 intss1 
 |-  ( b e. a -> |^| a C_ b )
18 17 adantl 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) ) /\ b e. a ) -> |^| a C_ b )
19 simpr 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) ) -> a C_ ( Moore ` X ) )
20 19 sselda 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) ) /\ b e. a ) -> b e. ( Moore ` X ) )
21 mresspw 
 |-  ( b e. ( Moore ` X ) -> b C_ ~P X )
22 20 21 syl 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) ) /\ b e. a ) -> b C_ ~P X )
23 18 22 sstrd 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) ) /\ b e. a ) -> |^| a C_ ~P X )
24 23 ex 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) ) -> ( b e. a -> |^| a C_ ~P X ) )
25 24 exlimdv 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) ) -> ( E. b b e. a -> |^| a C_ ~P X ) )
26 16 25 biimtrid 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) ) -> ( a =/= (/) -> |^| a C_ ~P X ) )
27 26 3impia 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) -> |^| a C_ ~P X )
28 simp2 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) -> a C_ ( Moore ` X ) )
29 28 sselda 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b e. a ) -> b e. ( Moore ` X ) )
30 mre1cl 
 |-  ( b e. ( Moore ` X ) -> X e. b )
31 29 30 syl 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b e. a ) -> X e. b )
32 31 ralrimiva 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) -> A. b e. a X e. b )
33 elintg 
 |-  ( X e. V -> ( X e. |^| a <-> A. b e. a X e. b ) )
34 33 3ad2ant1 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) -> ( X e. |^| a <-> A. b e. a X e. b ) )
35 32 34 mpbird 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) -> X e. |^| a )
36 simp12 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) -> a C_ ( Moore ` X ) )
37 36 sselda 
 |-  ( ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) /\ c e. a ) -> c e. ( Moore ` X ) )
38 simpl2 
 |-  ( ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) /\ c e. a ) -> b C_ |^| a )
39 intss1 
 |-  ( c e. a -> |^| a C_ c )
40 39 adantl 
 |-  ( ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) /\ c e. a ) -> |^| a C_ c )
41 38 40 sstrd 
 |-  ( ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) /\ c e. a ) -> b C_ c )
42 simpl3 
 |-  ( ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) /\ c e. a ) -> b =/= (/) )
43 mreintcl 
 |-  ( ( c e. ( Moore ` X ) /\ b C_ c /\ b =/= (/) ) -> |^| b e. c )
44 37 41 42 43 syl3anc 
 |-  ( ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) /\ c e. a ) -> |^| b e. c )
45 44 ralrimiva 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) -> A. c e. a |^| b e. c )
46 intex 
 |-  ( b =/= (/) <-> |^| b e. _V )
47 elintg 
 |-  ( |^| b e. _V -> ( |^| b e. |^| a <-> A. c e. a |^| b e. c ) )
48 46 47 sylbi 
 |-  ( b =/= (/) -> ( |^| b e. |^| a <-> A. c e. a |^| b e. c ) )
49 48 3ad2ant3 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) -> ( |^| b e. |^| a <-> A. c e. a |^| b e. c ) )
50 45 49 mpbird 
 |-  ( ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) /\ b C_ |^| a /\ b =/= (/) ) -> |^| b e. |^| a )
51 27 35 50 ismred 
 |-  ( ( X e. V /\ a C_ ( Moore ` X ) /\ a =/= (/) ) -> |^| a e. ( Moore ` X ) )
52 5 15 51 ismred 
 |-  ( X e. V -> ( Moore ` X ) e. ( Moore ` ~P X ) )