Metamath Proof Explorer

Theorem mrcuni

Description: Idempotence of closure under a general union. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypothesis mrcfval.f 
|- F = ( mrCls ` C )
Assertion mrcuni 
|- ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( F ` U. U ) = ( F ` U. ( F " U ) ) )

Proof

Step Hyp Ref Expression
1 mrcfval.f 
 |-  F = ( mrCls ` C )
2 simpl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> C e. ( Moore ` X ) )
3 simpll 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ s e. U ) -> C e. ( Moore ` X ) )
4 ssel2 
 |-  ( ( U C_ ~P X /\ s e. U ) -> s e. ~P X )
5 4 elpwid 
 |-  ( ( U C_ ~P X /\ s e. U ) -> s C_ X )
6 5 adantll 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ s e. U ) -> s C_ X )
7 1 mrcssid 
 |-  ( ( C e. ( Moore ` X ) /\ s C_ X ) -> s C_ ( F ` s ) )
8 3 6 7 syl2anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ s e. U ) -> s C_ ( F ` s ) )
9 1 mrcf 
 |-  ( C e. ( Moore ` X ) -> F : ~P X --> C )
10 9 ffund 
 |-  ( C e. ( Moore ` X ) -> Fun F )
11 10 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> Fun F )
12 9 fdmd 
 |-  ( C e. ( Moore ` X ) -> dom F = ~P X )
13 12 sseq2d 
 |-  ( C e. ( Moore ` X ) -> ( U C_ dom F <-> U C_ ~P X ) )
14 13 biimpar 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> U C_ dom F )
15 funfvima2 
 |-  ( ( Fun F /\ U C_ dom F ) -> ( s e. U -> ( F ` s ) e. ( F " U ) ) )
16 11 14 15 syl2anc 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( s e. U -> ( F ` s ) e. ( F " U ) ) )
17 16 imp 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ s e. U ) -> ( F ` s ) e. ( F " U ) )
18 elssuni 
 |-  ( ( F ` s ) e. ( F " U ) -> ( F ` s ) C_ U. ( F " U ) )
19 17 18 syl 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ s e. U ) -> ( F ` s ) C_ U. ( F " U ) )
20 8 19 sstrd 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ s e. U ) -> s C_ U. ( F " U ) )
21 20 ralrimiva 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> A. s e. U s C_ U. ( F " U ) )
22 unissb 
 |-  ( U. U C_ U. ( F " U ) <-> A. s e. U s C_ U. ( F " U ) )
23 21 22 sylibr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> U. U C_ U. ( F " U ) )
24 1 mrcssv 
 |-  ( C e. ( Moore ` X ) -> ( F ` x ) C_ X )
25 24 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( F ` x ) C_ X )
26 25 ralrimivw 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> A. x e. U ( F ` x ) C_ X )
27 9 ffnd 
 |-  ( C e. ( Moore ` X ) -> F Fn ~P X )
28 sseq1 
 |-  ( s = ( F ` x ) -> ( s C_ X <-> ( F ` x ) C_ X ) )
29 28 ralima 
 |-  ( ( F Fn ~P X /\ U C_ ~P X ) -> ( A. s e. ( F " U ) s C_ X <-> A. x e. U ( F ` x ) C_ X ) )
30 27 29 sylan 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( A. s e. ( F " U ) s C_ X <-> A. x e. U ( F ` x ) C_ X ) )
31 26 30 mpbird 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> A. s e. ( F " U ) s C_ X )
32 unissb 
 |-  ( U. ( F " U ) C_ X <-> A. s e. ( F " U ) s C_ X )
33 31 32 sylibr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> U. ( F " U ) C_ X )
34 1 mrcss 
 |-  ( ( C e. ( Moore ` X ) /\ U. U C_ U. ( F " U ) /\ U. ( F " U ) C_ X ) -> ( F ` U. U ) C_ ( F ` U. ( F " U ) ) )
35 2 23 33 34 syl3anc 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( F ` U. U ) C_ ( F ` U. ( F " U ) ) )
36 simpll 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ x e. U ) -> C e. ( Moore ` X ) )
37 elssuni 
 |-  ( x e. U -> x C_ U. U )
38 37 adantl 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ x e. U ) -> x C_ U. U )
39 sspwuni 
 |-  ( U C_ ~P X <-> U. U C_ X )
40 39 biimpi 
 |-  ( U C_ ~P X -> U. U C_ X )
41 40 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> U. U C_ X )
42 41 adantr 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ x e. U ) -> U. U C_ X )
43 1 mrcss 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ U. U /\ U. U C_ X ) -> ( F ` x ) C_ ( F ` U. U ) )
44 36 38 42 43 syl3anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) /\ x e. U ) -> ( F ` x ) C_ ( F ` U. U ) )
45 44 ralrimiva 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> A. x e. U ( F ` x ) C_ ( F ` U. U ) )
46 sseq1 
 |-  ( s = ( F ` x ) -> ( s C_ ( F ` U. U ) <-> ( F ` x ) C_ ( F ` U. U ) ) )
47 46 ralima 
 |-  ( ( F Fn ~P X /\ U C_ ~P X ) -> ( A. s e. ( F " U ) s C_ ( F ` U. U ) <-> A. x e. U ( F ` x ) C_ ( F ` U. U ) ) )
48 27 47 sylan 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( A. s e. ( F " U ) s C_ ( F ` U. U ) <-> A. x e. U ( F ` x ) C_ ( F ` U. U ) ) )
49 45 48 mpbird 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> A. s e. ( F " U ) s C_ ( F ` U. U ) )
50 unissb 
 |-  ( U. ( F " U ) C_ ( F ` U. U ) <-> A. s e. ( F " U ) s C_ ( F ` U. U ) )
51 49 50 sylibr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> U. ( F " U ) C_ ( F ` U. U ) )
52 1 mrcssv 
 |-  ( C e. ( Moore ` X ) -> ( F ` U. U ) C_ X )
53 52 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( F ` U. U ) C_ X )
54 1 mrcss 
 |-  ( ( C e. ( Moore ` X ) /\ U. ( F " U ) C_ ( F ` U. U ) /\ ( F ` U. U ) C_ X ) -> ( F ` U. ( F " U ) ) C_ ( F ` ( F ` U. U ) ) )
55 2 51 53 54 syl3anc 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( F ` U. ( F " U ) ) C_ ( F ` ( F ` U. U ) ) )
56 1 mrcidm 
 |-  ( ( C e. ( Moore ` X ) /\ U. U C_ X ) -> ( F ` ( F ` U. U ) ) = ( F ` U. U ) )
57 2 41 56 syl2anc 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( F ` ( F ` U. U ) ) = ( F ` U. U ) )
58 55 57 sseqtrd 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( F ` U. ( F " U ) ) C_ ( F ` U. U ) )
59 35 58 eqssd 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ ~P X ) -> ( F ` U. U ) = ( F ` U. ( F " U ) ) )