**Description:** Since the entire base set of a Moore collection is the greatest element
of it, the base set can be recovered from a Moore collection by set
union. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref | Expression | ||
---|---|---|---|

Assertion | mreuni | ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 = 𝑋 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | mre1cl | ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 ) | |

2 | mresspw | ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 ⊆ 𝒫 𝑋 ) | |

3 | elpwuni | ⊢ ( 𝑋 ∈ 𝐶 → ( 𝐶 ⊆ 𝒫 𝑋 ↔ ∪ 𝐶 = 𝑋 ) ) | |

4 | 3 | biimpa | ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐶 ⊆ 𝒫 𝑋 ) → ∪ 𝐶 = 𝑋 ) |

5 | 1 2 4 | syl2anc | ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 = 𝑋 ) |