Step |
Hyp |
Ref |
Expression |
1 |
|
lmrel |
|- Rel ( ~~>t ` J ) |
2 |
1
|
a1i |
|- ( J e. Haus -> Rel ( ~~>t ` J ) ) |
3 |
|
simpl |
|- ( ( J e. Haus /\ ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) ) -> J e. Haus ) |
4 |
|
simprl |
|- ( ( J e. Haus /\ ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) ) -> x ( ~~>t ` J ) y ) |
5 |
|
simprr |
|- ( ( J e. Haus /\ ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) ) -> x ( ~~>t ` J ) z ) |
6 |
3 4 5
|
lmmo |
|- ( ( J e. Haus /\ ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) ) -> y = z ) |
7 |
6
|
ex |
|- ( J e. Haus -> ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) ) |
8 |
7
|
alrimiv |
|- ( J e. Haus -> A. z ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) ) |
9 |
8
|
alrimiv |
|- ( J e. Haus -> A. y A. z ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) ) |
10 |
9
|
alrimiv |
|- ( J e. Haus -> A. x A. y A. z ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) ) |
11 |
|
dffun2 |
|- ( Fun ( ~~>t ` J ) <-> ( Rel ( ~~>t ` J ) /\ A. x A. y A. z ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) ) ) |
12 |
2 10 11
|
sylanbrc |
|- ( J e. Haus -> Fun ( ~~>t ` J ) ) |