Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | marypha2lem.t | |
|
Assertion | marypha2lem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | marypha2lem.t | |
|
2 | iunss | |
|
3 | snssi | |
|
4 | fvssunirn | |
|
5 | xpss12 | |
|
6 | 3 4 5 | sylancl | |
7 | 2 6 | mprgbir | |
8 | 1 7 | eqsstri | |