Metamath Proof Explorer

Theorem ispautN

Description: The predicate "is a projective automorphism". (Contributed by NM, 26-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pautset.s 
|- S = ( PSubSp ` K )
pautset.m 
|- M = ( PAut ` K )
Assertion ispautN 
|- ( K e. B -> ( F e. M <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pautset.s 
 |-  S = ( PSubSp ` K )
2 pautset.m 
 |-  M = ( PAut ` K )
3 1 2 pautsetN 
 |-  ( K e. B -> M = { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } )
4 3 eleq2d 
 |-  ( K e. B -> ( F e. M <-> F e. { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } ) )
5 f1of 
 |-  ( F : S -1-1-onto-> S -> F : S --> S )
6 1 fvexi 
 |-  S e. _V
7 fex 
 |-  ( ( F : S --> S /\ S e. _V ) -> F e. _V )
8 5 6 7 sylancl 
 |-  ( F : S -1-1-onto-> S -> F e. _V )
9 8 adantr 
 |-  ( ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) -> F e. _V )
10 f1oeq1 
 |-  ( f = F -> ( f : S -1-1-onto-> S <-> F : S -1-1-onto-> S ) )
11 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
12 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
13 11 12 sseq12d 
 |-  ( f = F -> ( ( f ` x ) C_ ( f ` y ) <-> ( F ` x ) C_ ( F ` y ) ) )
14 13 bibi2d 
 |-  ( f = F -> ( ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) <-> ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) )
15 14 2ralbidv 
 |-  ( f = F -> ( A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) <-> A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) )
16 10 15 anbi12d 
 |-  ( f = F -> ( ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) )
17 9 16 elab3 
 |-  ( F e. { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) )
18 4 17 bitrdi 
 |-  ( K e. B -> ( F e. M <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) )