This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion mrcun ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ ( 𝑈 ∪ 𝑉 ) ) = ( 𝐹 ‘ ( ( 𝐹 ‘ 𝑈 ) ∪ ( 𝐹 ‘ 𝑉 ) ) ) )

Proof

Step Hyp Ref Expression
1 mrcfval.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 simp1 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
3 mre1cl ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
4 elpw2g ⊢ ( 𝑋 ∈ 𝐶 → ( 𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋 ) )
5 3 4 syl ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑈 ∈ 𝒫 𝑋 ↔ 𝑈 ⊆ 𝑋 ) )
6 5 biimpar ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑈 ∈ 𝒫 𝑋 )
7 6 3adant3 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → 𝑈 ∈ 𝒫 𝑋 )
8 elpw2g ⊢ ( 𝑋 ∈ 𝐶 → ( 𝑉 ∈ 𝒫 𝑋 ↔ 𝑉 ⊆ 𝑋 ) )
9 3 8 syl ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑉 ∈ 𝒫 𝑋 ↔ 𝑉 ⊆ 𝑋 ) )
10 9 biimpar ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑉 ⊆ 𝑋 ) → 𝑉 ∈ 𝒫 𝑋 )
11 10 3adant2 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → 𝑉 ∈ 𝒫 𝑋 )
12 7 11 prssd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → { 𝑈 , 𝑉 } ⊆ 𝒫 𝑋 )
13 1 mrcuni ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ { 𝑈 , 𝑉 } ⊆ 𝒫 𝑋 ) → ( 𝐹 ‘ ∪ { 𝑈 , 𝑉 } ) = ( 𝐹 ‘ ∪ ( 𝐹 “ { 𝑈 , 𝑉 } ) ) )
14 2 12 13 syl2anc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ ∪ { 𝑈 , 𝑉 } ) = ( 𝐹 ‘ ∪ ( 𝐹 “ { 𝑈 , 𝑉 } ) ) )
15 uniprg ⊢ ( ( 𝑈 ∈ 𝒫 𝑋 ∧ 𝑉 ∈ 𝒫 𝑋 ) → ∪ { 𝑈 , 𝑉 } = ( 𝑈 ∪ 𝑉 ) )
16 7 11 15 syl2anc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → ∪ { 𝑈 , 𝑉 } = ( 𝑈 ∪ 𝑉 ) )
17 16 fveq2d ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ ∪ { 𝑈 , 𝑉 } ) = ( 𝐹 ‘ ( 𝑈 ∪ 𝑉 ) ) )
18 1 mrcf ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝐶 )
19 18 ffnd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 Fn 𝒫 𝑋 )
20 19 3ad2ant1 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → 𝐹 Fn 𝒫 𝑋 )
21 fnimapr ⊢ ( ( 𝐹 Fn 𝒫 𝑋 ∧ 𝑈 ∈ 𝒫 𝑋 ∧ 𝑉 ∈ 𝒫 𝑋 ) → ( 𝐹 “ { 𝑈 , 𝑉 } ) = { ( 𝐹 ‘ 𝑈 ) , ( 𝐹 ‘ 𝑉 ) } )
22 20 7 11 21 syl3anc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 “ { 𝑈 , 𝑉 } ) = { ( 𝐹 ‘ 𝑈 ) , ( 𝐹 ‘ 𝑉 ) } )
23 22 unieqd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → ∪ ( 𝐹 “ { 𝑈 , 𝑉 } ) = ∪ { ( 𝐹 ‘ 𝑈 ) , ( 𝐹 ‘ 𝑉 ) } )
24 fvex ⊢ ( 𝐹 ‘ 𝑈 ) ∈ V
25 fvex ⊢ ( 𝐹 ‘ 𝑉 ) ∈ V
26 24 25 unipr ⊢ ∪ { ( 𝐹 ‘ 𝑈 ) , ( 𝐹 ‘ 𝑉 ) } = ( ( 𝐹 ‘ 𝑈 ) ∪ ( 𝐹 ‘ 𝑉 ) )
27 23 26 eqtrdi ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → ∪ ( 𝐹 “ { 𝑈 , 𝑉 } ) = ( ( 𝐹 ‘ 𝑈 ) ∪ ( 𝐹 ‘ 𝑉 ) ) )
28 27 fveq2d ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ ∪ ( 𝐹 “ { 𝑈 , 𝑉 } ) ) = ( 𝐹 ‘ ( ( 𝐹 ‘ 𝑈 ) ∪ ( 𝐹 ‘ 𝑉 ) ) ) )
29 14 17 28 3eqtr3d ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ∧ 𝑉 ⊆ 𝑋 ) → ( 𝐹 ‘ ( 𝑈 ∪ 𝑉 ) ) = ( 𝐹 ‘ ( ( 𝐹 ‘ 𝑈 ) ∪ ( 𝐹 ‘ 𝑉 ) ) ) )