Metamath Proof Explorer

Theorem mrcun

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

Ref Expression
Hypothesis mrcfval.f 
|- F = ( mrCls ` C )
Assertion mrcun 
|- ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> ( F ` ( U u. V ) ) = ( F ` ( ( F ` U ) u. ( F ` V ) ) ) )

Proof

Step Hyp Ref Expression
1 mrcfval.f 
 |-  F = ( mrCls ` C )
2 simp1 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> C e. ( Moore ` X ) )
3 mre1cl 
 |-  ( C e. ( Moore ` X ) -> X e. C )
4 elpw2g 
 |-  ( X e. C -> ( U e. ~P X <-> U C_ X ) )
5 3 4 syl 
 |-  ( C e. ( Moore ` X ) -> ( U e. ~P X <-> U C_ X ) )
6 5 biimpar 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X ) -> U e. ~P X )
7 6 3adant3 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> U e. ~P X )
8 elpw2g 
 |-  ( X e. C -> ( V e. ~P X <-> V C_ X ) )
9 3 8 syl 
 |-  ( C e. ( Moore ` X ) -> ( V e. ~P X <-> V C_ X ) )
10 9 biimpar 
 |-  ( ( C e. ( Moore ` X ) /\ V C_ X ) -> V e. ~P X )
11 10 3adant2 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> V e. ~P X )
12 7 11 prssd 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> { U , V } C_ ~P X )
13 1 mrcuni 
 |-  ( ( C e. ( Moore ` X ) /\ { U , V } C_ ~P X ) -> ( F ` U. { U , V } ) = ( F ` U. ( F " { U , V } ) ) )
14 2 12 13 syl2anc 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> ( F ` U. { U , V } ) = ( F ` U. ( F " { U , V } ) ) )
15 uniprg 
 |-  ( ( U e. ~P X /\ V e. ~P X ) -> U. { U , V } = ( U u. V ) )
16 7 11 15 syl2anc 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> U. { U , V } = ( U u. V ) )
17 16 fveq2d 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> ( F ` U. { U , V } ) = ( F ` ( U u. V ) ) )
18 1 mrcf 
 |-  ( C e. ( Moore ` X ) -> F : ~P X --> C )
19 18 ffnd 
 |-  ( C e. ( Moore ` X ) -> F Fn ~P X )
20 19 3ad2ant1 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> F Fn ~P X )
21 fnimapr 
 |-  ( ( F Fn ~P X /\ U e. ~P X /\ V e. ~P X ) -> ( F " { U , V } ) = { ( F ` U ) , ( F ` V ) } )
22 20 7 11 21 syl3anc 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> ( F " { U , V } ) = { ( F ` U ) , ( F ` V ) } )
23 22 unieqd 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> U. ( F " { U , V } ) = U. { ( F ` U ) , ( F ` V ) } )
24 fvex 
 |-  ( F ` U ) e. _V
25 fvex 
 |-  ( F ` V ) e. _V
26 24 25 unipr 
 |-  U. { ( F ` U ) , ( F ` V ) } = ( ( F ` U ) u. ( F ` V ) )
27 23 26 eqtrdi 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> U. ( F " { U , V } ) = ( ( F ` U ) u. ( F ` V ) ) )
28 27 fveq2d 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> ( F ` U. ( F " { U , V } ) ) = ( F ` ( ( F ` U ) u. ( F ` V ) ) ) )
29 14 17 28 3eqtr3d 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X /\ V C_ X ) -> ( F ` ( U u. V ) ) = ( F ` ( ( F ` U ) u. ( F ` V ) ) ) )