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

Theorem marypha2lem4 7970
 Description: Lemma for marypha2 7971. 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 7968 . . . . 5
32imaeq1i 5171 . . . 4
4 df-ima 4852 . . . 4
53, 4eqtri 2493 . . 3
6 resopab2 5159 . . . . . 6
76adantl 473 . . . . 5
87rneqd 5068 . . . 4
9 rnopab 5085 . . . . 5
10 df-rex 2762 . . . . . . . . 9
1110bicomi 207 . . . . . . . 8
1211abbii 2587 . . . . . . 7
13 df-iun 4271 . . . . . . 7
1412, 13eqtr4i 2496 . . . . . 6
1514a1i 11 . . . . 5
169, 15syl5eq 2517 . . . 4
178, 16eqtrd 2505 . . 3
185, 17syl5eq 2517 . 2
19 fnfun 5683 . . . 4