Step |
Hyp |
Ref |
Expression |
1 |
|
pjinvar.1 |
|- S : ~H --> ~H |
2 |
|
pjinvar.2 |
|- H e. CH |
3 |
|
pjinvar.3 |
|- T = ( projh ` H ) |
4 |
3
|
fveq1i |
|- ( T ` ( ( S o. T ) ` x ) ) = ( ( projh ` H ) ` ( ( S o. T ) ` x ) ) |
5 |
|
ffvelrn |
|- ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( S o. T ) ` x ) e. H ) |
6 |
|
pjid |
|- ( ( H e. CH /\ ( ( S o. T ) ` x ) e. H ) -> ( ( projh ` H ) ` ( ( S o. T ) ` x ) ) = ( ( S o. T ) ` x ) ) |
7 |
2 5 6
|
sylancr |
|- ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( projh ` H ) ` ( ( S o. T ) ` x ) ) = ( ( S o. T ) ` x ) ) |
8 |
4 7
|
syl5req |
|- ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( S o. T ) ` x ) = ( T ` ( ( S o. T ) ` x ) ) ) |
9 |
|
fvco3 |
|- ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( T o. ( S o. T ) ) ` x ) = ( T ` ( ( S o. T ) ` x ) ) ) |
10 |
8 9
|
eqtr4d |
|- ( ( ( S o. T ) : ~H --> H /\ x e. ~H ) -> ( ( S o. T ) ` x ) = ( ( T o. ( S o. T ) ) ` x ) ) |
11 |
10
|
ralrimiva |
|- ( ( S o. T ) : ~H --> H -> A. x e. ~H ( ( S o. T ) ` x ) = ( ( T o. ( S o. T ) ) ` x ) ) |
12 |
2
|
pjfoi |
|- ( projh ` H ) : ~H -onto-> H |
13 |
|
fof |
|- ( ( projh ` H ) : ~H -onto-> H -> ( projh ` H ) : ~H --> H ) |
14 |
12 13
|
ax-mp |
|- ( projh ` H ) : ~H --> H |
15 |
3
|
feq1i |
|- ( T : ~H --> H <-> ( projh ` H ) : ~H --> H ) |
16 |
14 15
|
mpbir |
|- T : ~H --> H |
17 |
2
|
chssii |
|- H C_ ~H |
18 |
|
fss |
|- ( ( T : ~H --> H /\ H C_ ~H ) -> T : ~H --> ~H ) |
19 |
16 17 18
|
mp2an |
|- T : ~H --> ~H |
20 |
1 19
|
hocofni |
|- ( S o. T ) Fn ~H |
21 |
1 19
|
hocofi |
|- ( S o. T ) : ~H --> ~H |
22 |
19 21
|
hocofni |
|- ( T o. ( S o. T ) ) Fn ~H |
23 |
|
eqfnfv |
|- ( ( ( S o. T ) Fn ~H /\ ( T o. ( S o. T ) ) Fn ~H ) -> ( ( S o. T ) = ( T o. ( S o. T ) ) <-> A. x e. ~H ( ( S o. T ) ` x ) = ( ( T o. ( S o. T ) ) ` x ) ) ) |
24 |
20 22 23
|
mp2an |
|- ( ( S o. T ) = ( T o. ( S o. T ) ) <-> A. x e. ~H ( ( S o. T ) ` x ) = ( ( T o. ( S o. T ) ) ` x ) ) |
25 |
11 24
|
sylibr |
|- ( ( S o. T ) : ~H --> H -> ( S o. T ) = ( T o. ( S o. T ) ) ) |
26 |
|
fco |
|- ( ( T : ~H --> H /\ ( S o. T ) : ~H --> ~H ) -> ( T o. ( S o. T ) ) : ~H --> H ) |
27 |
16 21 26
|
mp2an |
|- ( T o. ( S o. T ) ) : ~H --> H |
28 |
|
feq1 |
|- ( ( S o. T ) = ( T o. ( S o. T ) ) -> ( ( S o. T ) : ~H --> H <-> ( T o. ( S o. T ) ) : ~H --> H ) ) |
29 |
27 28
|
mpbiri |
|- ( ( S o. T ) = ( T o. ( S o. T ) ) -> ( S o. T ) : ~H --> H ) |
30 |
25 29
|
impbii |
|- ( ( S o. T ) : ~H --> H <-> ( S o. T ) = ( T o. ( S o. T ) ) ) |