Metamath Proof Explorer


Theorem marypha2lem1

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

Ref Expression
Hypothesis marypha2lem.t T=xAx×Fx
Assertion marypha2lem1 TA×ranF

Proof

Step Hyp Ref Expression
1 marypha2lem.t T=xAx×Fx
2 iunss xAx×FxA×ranFxAx×FxA×ranF
3 snssi xAxA
4 fvssunirn FxranF
5 xpss12 xAFxranFx×FxA×ranF
6 3 4 5 sylancl xAx×FxA×ranF
7 2 6 mprgbir xAx×FxA×ranF
8 1 7 eqsstri TA×ranF