Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  marypha2lem4 Structured version   Unicode version

Theorem marypha2lem4 7435
 Description: Lemma for marypha2 7436. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.)
Hypothesis
Ref Expression
marypha2lem.t
Assertion
Ref Expression
marypha2lem4
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem marypha2lem4
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 marypha2lem.t . . . . . 6
21marypha2lem2 7433 . . . . 5
32imaeq1i 5192 . . . 4
4 df-ima 4883 . . . 4
53, 4eqtri 2455 . . 3
6 resopab2 5182 . . . . . 6
76adantl 453 . . . . 5
87rneqd 5089 . . . 4
9 rnopab 5107 . . . . 5
10 df-rex 2703 . . . . . . . . 9
1110bicomi 194 . . . . . . . 8
1211abbii 2547 . . . . . . 7
13 df-iun 4087 . . . . . . 7
1412, 13eqtr4i 2458 . . . . . 6
1514a1i 11 . . . . 5
169, 15syl5eq 2479 . . . 4
178, 16eqtrd 2467 . . 3
185, 17syl5eq 2479 . 2
19 fnfun 5534 . . . 4