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

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

Proof

Step Hyp Ref Expression
1 mrcfval.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 simpl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
3 simpll ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
4 ssel2 ⊢ ( ( 𝑈 ⊆ 𝒫 𝑋 ∧ 𝑠 ∈ 𝑈 ) → 𝑠 ∈ 𝒫 𝑋 )
5 4 elpwid ⊢ ( ( 𝑈 ⊆ 𝒫 𝑋 ∧ 𝑠 ∈ 𝑈 ) → 𝑠 ⊆ 𝑋 )
6 5 adantll ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) → 𝑠 ⊆ 𝑋 )
7 1 mrcssid ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑠 ⊆ 𝑋 ) → 𝑠 ⊆ ( 𝐹 ‘ 𝑠 ) )
8 3 6 7 syl2anc ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) → 𝑠 ⊆ ( 𝐹 ‘ 𝑠 ) )
9 1 mrcf ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝐶 )
10 9 ffund ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → Fun 𝐹 )
11 10 adantr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → Fun 𝐹 )
12 9 fdmd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → dom 𝐹 = 𝒫 𝑋 )
13 12 sseq2d ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑈 ⊆ dom 𝐹 ↔ 𝑈 ⊆ 𝒫 𝑋 ) )
14 13 biimpar ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → 𝑈 ⊆ dom 𝐹 )
15 funfvima2 ⊢ ( ( Fun 𝐹 ∧ 𝑈 ⊆ dom 𝐹 ) → ( 𝑠 ∈ 𝑈 → ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐹 “ 𝑈 ) ) )
16 11 14 15 syl2anc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( 𝑠 ∈ 𝑈 → ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐹 “ 𝑈 ) ) )
17 16 imp ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) → ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐹 “ 𝑈 ) )
18 elssuni ⊢ ( ( 𝐹 ‘ 𝑠 ) ∈ ( 𝐹 “ 𝑈 ) → ( 𝐹 ‘ 𝑠 ) ⊆ ∪ ( 𝐹 “ 𝑈 ) )
19 17 18 syl ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) → ( 𝐹 ‘ 𝑠 ) ⊆ ∪ ( 𝐹 “ 𝑈 ) )
20 8 19 sstrd ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑠 ∈ 𝑈 ) → 𝑠 ⊆ ∪ ( 𝐹 “ 𝑈 ) )
21 20 ralrimiva ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ∀ 𝑠 ∈ 𝑈 𝑠 ⊆ ∪ ( 𝐹 “ 𝑈 ) )
22 unissb ⊢ ( ∪ 𝑈 ⊆ ∪ ( 𝐹 “ 𝑈 ) ↔ ∀ 𝑠 ∈ 𝑈 𝑠 ⊆ ∪ ( 𝐹 “ 𝑈 ) )
23 21 22 sylibr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ∪ 𝑈 ⊆ ∪ ( 𝐹 “ 𝑈 ) )
24 1 mrcssv ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ⊆ 𝑋 )
25 24 adantr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ⊆ 𝑋 )
26 25 ralrimivw ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ∀ 𝑥 ∈ 𝑈 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑋 )
27 9 ffnd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 Fn 𝒫 𝑋 )
28 sseq1 ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑥 ) → ( 𝑠 ⊆ 𝑋 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑋 ) )
29 28 ralima ⊢ ( ( 𝐹 Fn 𝒫 𝑋 ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( ∀ 𝑠 ∈ ( 𝐹 “ 𝑈 ) 𝑠 ⊆ 𝑋 ↔ ∀ 𝑥 ∈ 𝑈 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑋 ) )
30 27 29 sylan ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( ∀ 𝑠 ∈ ( 𝐹 “ 𝑈 ) 𝑠 ⊆ 𝑋 ↔ ∀ 𝑥 ∈ 𝑈 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑋 ) )
31 26 30 mpbird ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ∀ 𝑠 ∈ ( 𝐹 “ 𝑈 ) 𝑠 ⊆ 𝑋 )
32 unissb ⊢ ( ∪ ( 𝐹 “ 𝑈 ) ⊆ 𝑋 ↔ ∀ 𝑠 ∈ ( 𝐹 “ 𝑈 ) 𝑠 ⊆ 𝑋 )
33 31 32 sylibr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ∪ ( 𝐹 “ 𝑈 ) ⊆ 𝑋 )
34 1 mrcss ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∪ 𝑈 ⊆ ∪ ( 𝐹 “ 𝑈 ) ∧ ∪ ( 𝐹 “ 𝑈 ) ⊆ 𝑋 ) → ( 𝐹 ‘ ∪ 𝑈 ) ⊆ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑈 ) ) )
35 2 23 33 34 syl3anc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( 𝐹 ‘ ∪ 𝑈 ) ⊆ ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑈 ) ) )
36 simpll ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
37 elssuni ⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ⊆ ∪ 𝑈 )
38 37 adantl ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ⊆ ∪ 𝑈 )
39 sspwuni ⊢ ( 𝑈 ⊆ 𝒫 𝑋 ↔ ∪ 𝑈 ⊆ 𝑋 )
40 39 biimpi ⊢ ( 𝑈 ⊆ 𝒫 𝑋 → ∪ 𝑈 ⊆ 𝑋 )
41 40 adantl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ∪ 𝑈 ⊆ 𝑋 )
42 41 adantr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → ∪ 𝑈 ⊆ 𝑋 )
43 1 mrcss ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ ∪ 𝑈 ∧ ∪ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) )
44 36 38 42 43 syl3anc ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) )
45 44 ralrimiva ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ∀ 𝑥 ∈ 𝑈 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) )
46 sseq1 ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑥 ) → ( 𝑠 ⊆ ( 𝐹 ‘ ∪ 𝑈 ) ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) ) )
47 46 ralima ⊢ ( ( 𝐹 Fn 𝒫 𝑋 ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( ∀ 𝑠 ∈ ( 𝐹 “ 𝑈 ) 𝑠 ⊆ ( 𝐹 ‘ ∪ 𝑈 ) ↔ ∀ 𝑥 ∈ 𝑈 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) ) )
48 27 47 sylan ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( ∀ 𝑠 ∈ ( 𝐹 “ 𝑈 ) 𝑠 ⊆ ( 𝐹 ‘ ∪ 𝑈 ) ↔ ∀ 𝑥 ∈ 𝑈 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) ) )
49 45 48 mpbird ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ∀ 𝑠 ∈ ( 𝐹 “ 𝑈 ) 𝑠 ⊆ ( 𝐹 ‘ ∪ 𝑈 ) )
50 unissb ⊢ ( ∪ ( 𝐹 “ 𝑈 ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) ↔ ∀ 𝑠 ∈ ( 𝐹 “ 𝑈 ) 𝑠 ⊆ ( 𝐹 ‘ ∪ 𝑈 ) )
51 49 50 sylibr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ∪ ( 𝐹 “ 𝑈 ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) )
52 1 mrcssv ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐹 ‘ ∪ 𝑈 ) ⊆ 𝑋 )
53 52 adantr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( 𝐹 ‘ ∪ 𝑈 ) ⊆ 𝑋 )
54 1 mrcss ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∪ ( 𝐹 “ 𝑈 ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) ∧ ( 𝐹 ‘ ∪ 𝑈 ) ⊆ 𝑋 ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑈 ) ) ⊆ ( 𝐹 ‘ ( 𝐹 ‘ ∪ 𝑈 ) ) )
55 2 51 53 54 syl3anc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑈 ) ) ⊆ ( 𝐹 ‘ ( 𝐹 ‘ ∪ 𝑈 ) ) )
56 1 mrcidm ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∪ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ ( 𝐹 ‘ ∪ 𝑈 ) ) = ( 𝐹 ‘ ∪ 𝑈 ) )
57 2 41 56 syl2anc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( 𝐹 ‘ ( 𝐹 ‘ ∪ 𝑈 ) ) = ( 𝐹 ‘ ∪ 𝑈 ) )
58 55 57 sseqtrd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑈 ) ) ⊆ ( 𝐹 ‘ ∪ 𝑈 ) )
59 35 58 eqssd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝒫 𝑋 ) → ( 𝐹 ‘ ∪ 𝑈 ) = ( 𝐹 ‘ ∪ ( 𝐹 “ 𝑈 ) ) )