Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hilex |
|- ~H e. _V |
2 |
|
fex2 |
|- ( ( T : ~H --> ~H /\ ~H e. _V /\ ~H e. _V ) -> T e. _V ) |
3 |
1 1 2
|
mp3an23 |
|- ( T : ~H --> ~H -> T e. _V ) |
4 |
|
feq1 |
|- ( t = T -> ( t : ~H --> ~H <-> T : ~H --> ~H ) ) |
5 |
|
fveq1 |
|- ( t = T -> ( t ` y ) = ( T ` y ) ) |
6 |
5
|
oveq2d |
|- ( t = T -> ( x .ih ( t ` y ) ) = ( x .ih ( T ` y ) ) ) |
7 |
6
|
eqeq1d |
|- ( t = T -> ( ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) <-> ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) |
8 |
7
|
2ralbidv |
|- ( t = T -> ( A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) <-> A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) |
9 |
4 8
|
3anbi13d |
|- ( t = T -> ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) |
10 |
|
3anass |
|- ( ( T : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) |
11 |
9 10
|
syl6bb |
|- ( t = T -> ( ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) ) |
12 |
11
|
exbidv |
|- ( t = T -> ( E. u ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) <-> E. u ( T : ~H --> ~H /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) ) |
13 |
|
19.42v |
|- ( E. u ( T : ~H --> ~H /\ ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) <-> ( T : ~H --> ~H /\ E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) |
14 |
12 13
|
syl6bb |
|- ( t = T -> ( E. u ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( T : ~H --> ~H /\ E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) ) |
15 |
|
dfadj2 |
|- adjh = { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) } |
16 |
15
|
dmeqi |
|- dom adjh = dom { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) } |
17 |
|
dmopab |
|- dom { <. t , u >. | ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) } = { t | E. u ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) } |
18 |
16 17
|
eqtri |
|- dom adjh = { t | E. u ( t : ~H --> ~H /\ u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( t ` y ) ) = ( ( u ` x ) .ih y ) ) } |
19 |
14 18
|
elab2g |
|- ( T e. _V -> ( T e. dom adjh <-> ( T : ~H --> ~H /\ E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) ) |
20 |
19
|
baibd |
|- ( ( T e. _V /\ T : ~H --> ~H ) -> ( T e. dom adjh <-> E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) |
21 |
3 20
|
mpancom |
|- ( T : ~H --> ~H -> ( T e. dom adjh <-> E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) |
22 |
|
df-reu |
|- ( E! u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> E! u ( u e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) |
23 |
1 1
|
elmap |
|- ( u e. ( ~H ^m ~H ) <-> u : ~H --> ~H ) |
24 |
23
|
anbi1i |
|- ( ( u e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) |
25 |
24
|
eubii |
|- ( E! u ( u e. ( ~H ^m ~H ) /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> E! u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) |
26 |
|
adjmo |
|- E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) |
27 |
|
df-eu |
|- ( E! u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> ( E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) /\ E* u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) ) |
28 |
26 27
|
mpbiran2 |
|- ( E! u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) <-> E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) |
29 |
22 25 28
|
3bitri |
|- ( E! u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) <-> E. u ( u : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) |
30 |
21 29
|
bitr4di |
|- ( T : ~H --> ~H -> ( T e. dom adjh <-> E! u e. ( ~H ^m ~H ) A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( u ` x ) .ih y ) ) ) |