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 → U V ⊆ 𝒫 X
13 1 mrcuni ⊢ C ∈ Moore ⁡ X ∧ U V ⊆ 𝒫 X → F ⁡ ⋃ U V = F ⁡ ⋃ F U V
14 2 12 13 syl2anc ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X ∧ V ⊆ X → F ⁡ ⋃ U V = F ⁡ ⋃ F U V
15 uniprg ⊢ U ∈ 𝒫 X ∧ V ∈ 𝒫 X → ⋃ U V = U ∪ V
16 7 11 15 syl2anc ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X ∧ V ⊆ X → ⋃ U V = U ∪ V
17 16 fveq2d ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X ∧ V ⊆ X → F ⁡ ⋃ U V = F ⁡ U ∪ V
18 1 mrcf ⊢ C ∈ Moore ⁡ X → F : 𝒫 X ⟶ C
19 18 ffnd ⊢ C ∈ Moore ⁡ X → F Fn 𝒫 X
20 19 3ad2ant1 ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X ∧ V ⊆ X → F Fn 𝒫 X
21 fnimapr ⊢ F Fn 𝒫 X ∧ U ∈ 𝒫 X ∧ V ∈ 𝒫 X → F U V = F ⁡ U F ⁡ V
22 20 7 11 21 syl3anc ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X ∧ V ⊆ X → F U V = F ⁡ U F ⁡ V
23 22 unieqd ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X ∧ V ⊆ X → ⋃ F U V = ⋃ F ⁡ U F ⁡ V
24 fvex ⊢ F ⁡ U ∈ V
25 fvex ⊢ F ⁡ V ∈ V
26 24 25 unipr ⊢ ⋃ F ⁡ U F ⁡ V = F ⁡ U ∪ F ⁡ V
27 23 26 eqtrdi ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X ∧ V ⊆ X → ⋃ F U V = F ⁡ U ∪ F ⁡ V
28 27 fveq2d ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X ∧ V ⊆ X → F ⁡ ⋃ F U V = 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