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

Metamath Proof Explorer

Theorem mreunirn

Description: Two ways to express the notion of being a Moore collection on an unspecified base. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion mreunirn ( 𝐶 ∈ ∪ ran Moore ↔ 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fnmre ⊢ Moore Fn V
2 fnunirn ⊢ ( Moore Fn V → ( 𝐶 ∈ ∪ ran Moore ↔ ∃ 𝑥 ∈ V 𝐶 ∈ ( Moore ‘ 𝑥 ) ) )
3 1 2 ax-mp ⊢ ( 𝐶 ∈ ∪ ran Moore ↔ ∃ 𝑥 ∈ V 𝐶 ∈ ( Moore ‘ 𝑥 ) )
4 mreuni ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑥 ) → ∪ 𝐶 = 𝑥 )
5 4 fveq2d ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑥 ) → ( Moore ‘ ∪ 𝐶 ) = ( Moore ‘ 𝑥 ) )
6 5 eleq2d ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑥 ) → ( 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) ↔ 𝐶 ∈ ( Moore ‘ 𝑥 ) ) )
7 6 ibir ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑥 ) → 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )
8 7 rexlimivw ⊢ ( ∃ 𝑥 ∈ V 𝐶 ∈ ( Moore ‘ 𝑥 ) → 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )
9 3 8 sylbi ⊢ ( 𝐶 ∈ ∪ ran Moore → 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )
10 fvssunirn ⊢ ( Moore ‘ ∪ 𝐶 ) ⊆ ∪ ran Moore
11 10 sseli ⊢ ( 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) → 𝐶 ∈ ∪ ran Moore )
12 9 11 impbii ⊢ ( 𝐶 ∈ ∪ ran Moore ↔ 𝐶 ∈ ( Moore ‘ ∪ 𝐶 ) )