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 ⊢ C ∈ ⋃ ran ⁡ Moore ↔ C ∈ Moore ⁡ ⋃ C

Proof

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