Metamath Proof Explorer

Theorem submre

Description: The subcollection of a closed set system below a given closed set is itself a closed set system. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Assertion submre 
|- ( ( C e. ( Moore ` X ) /\ A e. C ) -> ( C i^i ~P A ) e. ( Moore ` A ) )

Proof

Step Hyp Ref Expression
1 inss2 
 |-  ( C i^i ~P A ) C_ ~P A
2 1 a1i 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C ) -> ( C i^i ~P A ) C_ ~P A )
3 simpr 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C ) -> A e. C )
4 pwidg 
 |-  ( A e. C -> A e. ~P A )
5 4 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C ) -> A e. ~P A )
6 3 5 elind 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C ) -> A e. ( C i^i ~P A ) )
7 simp1l 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> C e. ( Moore ` X ) )
8 inss1 
 |-  ( C i^i ~P A ) C_ C
9 sstr 
 |-  ( ( x C_ ( C i^i ~P A ) /\ ( C i^i ~P A ) C_ C ) -> x C_ C )
10 8 9 mpan2 
 |-  ( x C_ ( C i^i ~P A ) -> x C_ C )
11 10 3ad2ant2 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> x C_ C )
12 simp3 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> x =/= (/) )
13 mreintcl 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C /\ x =/= (/) ) -> |^| x e. C )
14 7 11 12 13 syl3anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> |^| x e. C )
15 sstr 
 |-  ( ( x C_ ( C i^i ~P A ) /\ ( C i^i ~P A ) C_ ~P A ) -> x C_ ~P A )
16 1 15 mpan2 
 |-  ( x C_ ( C i^i ~P A ) -> x C_ ~P A )
17 16 3ad2ant2 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> x C_ ~P A )
18 intssuni2 
 |-  ( ( x C_ ~P A /\ x =/= (/) ) -> |^| x C_ U. ~P A )
19 17 12 18 syl2anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> |^| x C_ U. ~P A )
20 unipw 
 |-  U. ~P A = A
21 19 20 sseqtrdi 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> |^| x C_ A )
22 elpw2g 
 |-  ( A e. C -> ( |^| x e. ~P A <-> |^| x C_ A ) )
23 22 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C ) -> ( |^| x e. ~P A <-> |^| x C_ A ) )
24 23 3ad2ant1 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> ( |^| x e. ~P A <-> |^| x C_ A ) )
25 21 24 mpbird 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> |^| x e. ~P A )
26 14 25 elind 
 |-  ( ( ( C e. ( Moore ` X ) /\ A e. C ) /\ x C_ ( C i^i ~P A ) /\ x =/= (/) ) -> |^| x e. ( C i^i ~P A ) )
27 2 6 26 ismred 
 |-  ( ( C e. ( Moore ` X ) /\ A e. C ) -> ( C i^i ~P A ) e. ( Moore ` A ) )