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∈Moore⁡X∧U⊆X∧V⊆X→F⁡U∪V=F⁡F⁡U∪F⁡V

Proof

Step Hyp Ref Expression
1 mrcfval.f ⊢F=mrCls⁡C
2 simp1 ⊢C∈Moore⁡X∧U⊆X∧V⊆X→C∈Moore⁡X
3 mre1cl ⊢C∈Moore⁡X→X∈C
4 elpw2g ⊢X∈C→U∈𝒫X↔U⊆X
5 3 4 syl ⊢C∈Moore⁡X→U∈𝒫X↔U⊆X
6 5 biimpar ⊢C∈Moore⁡X∧U⊆X→U∈𝒫X
7 6 3adant3 ⊢C∈Moore⁡X∧U⊆X∧V⊆X→U∈𝒫X
8 elpw2g ⊢X∈C→V∈𝒫X↔V⊆X
9 3 8 syl ⊢C∈Moore⁡X→V∈𝒫X↔V⊆X
10 9 biimpar ⊢C∈Moore⁡X∧V⊆X→V∈𝒫X
11 10 3adant2 ⊢C∈Moore⁡X∧U⊆X∧V⊆X→V∈𝒫X
12 7 11 prssd ⊢C∈Moore⁡X∧U⊆X∧V⊆X→UV⊆𝒫X
13 1 mrcuni ⊢C∈Moore⁡X∧UV⊆𝒫X→F⁡⋃UV=F⁡⋃FUV
14 2 12 13 syl2anc ⊢C∈Moore⁡X∧U⊆X∧V⊆X→F⁡⋃UV=F⁡⋃FUV
15 uniprg ⊢U∈𝒫X∧V∈𝒫X→⋃UV=U∪V
16 7 11 15 syl2anc ⊢C∈Moore⁡X∧U⊆X∧V⊆X→⋃UV=U∪V
17 16 fveq2d ⊢C∈Moore⁡X∧U⊆X∧V⊆X→F⁡⋃UV=F⁡U∪V
18 1 mrcf ⊢C∈Moore⁡X→F:𝒫X⟶C
19 18 ffnd ⊢C∈Moore⁡X→FFn𝒫X
20 19 3ad2ant1 ⊢C∈Moore⁡X∧U⊆X∧V⊆X→FFn𝒫X
21 fnimapr ⊢FFn𝒫X∧U∈𝒫X∧V∈𝒫X→FUV=F⁡UF⁡V
22 20 7 11 21 syl3anc ⊢C∈Moore⁡X∧U⊆X∧V⊆X→FUV=F⁡UF⁡V
23 22 unieqd ⊢C∈Moore⁡X∧U⊆X∧V⊆X→⋃FUV=⋃F⁡UF⁡V
24 fvex ⊢F⁡U∈V
25 fvex ⊢F⁡V∈V
26 24 25 unipr ⊢⋃F⁡UF⁡V=F⁡U∪F⁡V
27 23 26 eqtrdi ⊢C∈Moore⁡X∧U⊆X∧V⊆X→⋃FUV=F⁡U∪F⁡V
28 27 fveq2d ⊢C∈Moore⁡X∧U⊆X∧V⊆X→F⁡⋃FUV=F⁡F⁡U∪F⁡V
29 14 17 28 3eqtr3d ⊢C∈Moore⁡X∧U⊆X∧V⊆X→F⁡U∪V=F⁡F⁡U∪F⁡V