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 CranMooreCMooreC

Proof

Step Hyp Ref Expression
1 fnmre MooreFnV
2 fnunirn MooreFnVCranMoorexVCMoorex
3 1 2 ax-mp CranMoorexVCMoorex
4 mreuni CMoorexC=x
5 4 fveq2d CMoorexMooreC=Moorex
6 5 eleq2d CMoorexCMooreCCMoorex
7 6 ibir CMoorexCMooreC
8 7 rexlimivw xVCMoorexCMooreC
9 3 8 sylbi CranMooreCMooreC
10 fvssunirn MooreCranMoore
11 10 sseli CMooreCCranMoore
12 9 11 impbii CranMooreCMooreC