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 e. U. ran Moore <-> C e. ( Moore ` U. C ) )

Proof

Step Hyp Ref Expression
1 fnmre 
 |-  Moore Fn _V
2 fnunirn 
 |-  ( Moore Fn _V -> ( C e. U. ran Moore <-> E. x e. _V C e. ( Moore ` x ) ) )
3 1 2 ax-mp 
 |-  ( C e. U. ran Moore <-> E. x e. _V C e. ( Moore ` x ) )
4 mreuni 
 |-  ( C e. ( Moore ` x ) -> U. C = x )
5 4 fveq2d 
 |-  ( C e. ( Moore ` x ) -> ( Moore ` U. C ) = ( Moore ` x ) )
6 5 eleq2d 
 |-  ( C e. ( Moore ` x ) -> ( C e. ( Moore ` U. C ) <-> C e. ( Moore ` x ) ) )
7 6 ibir 
 |-  ( C e. ( Moore ` x ) -> C e. ( Moore ` U. C ) )
8 7 rexlimivw 
 |-  ( E. x e. _V C e. ( Moore ` x ) -> C e. ( Moore ` U. C ) )
9 3 8 sylbi 
 |-  ( C e. U. ran Moore -> C e. ( Moore ` U. C ) )
10 fvssunirn 
 |-  ( Moore ` U. C ) C_ U. ran Moore
11 10 sseli 
 |-  ( C e. ( Moore ` U. C ) -> C e. U. ran Moore )
12 9 11 impbii 
 |-  ( C e. U. ran Moore <-> C e. ( Moore ` U. C ) )