Metamath Proof Explorer

Theorem f1omvdmvd

Description: A permutation of any class moves a point which is moved to a different point which is moved. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Assertion f1omvdmvd 
|- ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( F ` X ) e. ( dom ( F \ _I ) \ { X } ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> X e. dom ( F \ _I ) )
2 f1ofn 
 |-  ( F : A -1-1-onto-> A -> F Fn A )
3 difss 
 |-  ( F \ _I ) C_ F
4 dmss 
 |-  ( ( F \ _I ) C_ F -> dom ( F \ _I ) C_ dom F )
5 3 4 ax-mp 
 |-  dom ( F \ _I ) C_ dom F
6 f1odm 
 |-  ( F : A -1-1-onto-> A -> dom F = A )
7 5 6 sseqtrid 
 |-  ( F : A -1-1-onto-> A -> dom ( F \ _I ) C_ A )
8 7 sselda 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> X e. A )
9 fnelnfp 
 |-  ( ( F Fn A /\ X e. A ) -> ( X e. dom ( F \ _I ) <-> ( F ` X ) =/= X ) )
10 2 8 9 syl2an2r 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( X e. dom ( F \ _I ) <-> ( F ` X ) =/= X ) )
11 1 10 mpbid 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( F ` X ) =/= X )
12 f1of1 
 |-  ( F : A -1-1-onto-> A -> F : A -1-1-> A )
13 12 adantr 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> F : A -1-1-> A )
14 f1of 
 |-  ( F : A -1-1-onto-> A -> F : A --> A )
15 14 adantr 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> F : A --> A )
16 15 8 ffvelrnd 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( F ` X ) e. A )
17 f1fveq 
 |-  ( ( F : A -1-1-> A /\ ( ( F ` X ) e. A /\ X e. A ) ) -> ( ( F ` ( F ` X ) ) = ( F ` X ) <-> ( F ` X ) = X ) )
18 13 16 8 17 syl12anc 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( ( F ` ( F ` X ) ) = ( F ` X ) <-> ( F ` X ) = X ) )
19 18 necon3bid 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( ( F ` ( F ` X ) ) =/= ( F ` X ) <-> ( F ` X ) =/= X ) )
20 11 19 mpbird 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( F ` ( F ` X ) ) =/= ( F ` X ) )
21 fnelnfp 
 |-  ( ( F Fn A /\ ( F ` X ) e. A ) -> ( ( F ` X ) e. dom ( F \ _I ) <-> ( F ` ( F ` X ) ) =/= ( F ` X ) ) )
22 2 16 21 syl2an2r 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( ( F ` X ) e. dom ( F \ _I ) <-> ( F ` ( F ` X ) ) =/= ( F ` X ) ) )
23 20 22 mpbird 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( F ` X ) e. dom ( F \ _I ) )
24 eldifsn 
 |-  ( ( F ` X ) e. ( dom ( F \ _I ) \ { X } ) <-> ( ( F ` X ) e. dom ( F \ _I ) /\ ( F ` X ) =/= X ) )
25 23 11 24 sylanbrc 
 |-  ( ( F : A -1-1-onto-> A /\ X e. dom ( F \ _I ) ) -> ( F ` X ) e. ( dom ( F \ _I ) \ { X } ) )