Metamath Proof Explorer

Theorem symgfixfolem1

Description: Lemma 1 for symgfixfo . (Contributed by AV, 7-Jan-2019)

Ref Expression
Hypotheses symgfixf.p 
|- P = ( Base ` ( SymGrp ` N ) )
symgfixf.q 
|- Q = { q e. P | ( q ` K ) = K }
symgfixf.s 
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
symgfixf.h 
|- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )
symgfixfo.e 
|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
Assertion symgfixfolem1 
|- ( ( N e. V /\ K e. N /\ Z e. S ) -> E e. Q )

Proof

Step Hyp Ref Expression
1 symgfixf.p 
 |-  P = ( Base ` ( SymGrp ` N ) )
2 symgfixf.q 
 |-  Q = { q e. P | ( q ` K ) = K }
3 symgfixf.s 
 |-  S = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
4 symgfixf.h 
 |-  H = ( q e. Q |-> ( q |` ( N \ { K } ) ) )
5 symgfixfo.e 
 |-  E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) )
6 3 5 symgextf1o 
 |-  ( ( K e. N /\ Z e. S ) -> E : N -1-1-onto-> N )
7 6 3adant1 
 |-  ( ( N e. V /\ K e. N /\ Z e. S ) -> E : N -1-1-onto-> N )
8 iftrue 
 |-  ( x = K -> if ( x = K , K , ( Z ` x ) ) = K )
9 simp2 
 |-  ( ( N e. V /\ K e. N /\ Z e. S ) -> K e. N )
10 5 8 9 9 fvmptd3 
 |-  ( ( N e. V /\ K e. N /\ Z e. S ) -> ( E ` K ) = K )
11 mptexg 
 |-  ( N e. V -> ( x e. N |-> if ( x = K , K , ( Z ` x ) ) ) e. _V )
12 11 3ad2ant1 
 |-  ( ( N e. V /\ K e. N /\ Z e. S ) -> ( x e. N |-> if ( x = K , K , ( Z ` x ) ) ) e. _V )
13 5 12 eqeltrid 
 |-  ( ( N e. V /\ K e. N /\ Z e. S ) -> E e. _V )
14 1 2 symgfixelq 
 |-  ( E e. _V -> ( E e. Q <-> ( E : N -1-1-onto-> N /\ ( E ` K ) = K ) ) )
15 13 14 syl 
 |-  ( ( N e. V /\ K e. N /\ Z e. S ) -> ( E e. Q <-> ( E : N -1-1-onto-> N /\ ( E ` K ) = K ) ) )
16 7 10 15 mpbir2and 
 |-  ( ( N e. V /\ K e. N /\ Z e. S ) -> E e. Q )