Theorem motf1o

Description: Motions are bijections. (Contributed by Thierry Arnoux, 15-Dec-2019)

	Ref	Expression
Hypotheses	ismot.p	|- P = ( Base ` G )
	ismot.m	|- .- = ( dist ` G )
	motgrp.1	|- ( ph -> G e. V )
	motco.2	|- ( ph -> F e. ( G Ismt G ) )
Assertion	motf1o	|- ( ph -> F : P -1-1-onto-> P )

Proof

Step	Hyp	Ref	Expression
1		ismot.p	|- P = ( Base ` G )
2		ismot.m	|- .- = ( dist ` G )
3		motgrp.1	|- ( ph -> G e. V )
4		motco.2	|- ( ph -> F e. ( G Ismt G ) )
5	1 2	ismot	|- ( G e. V -> ( F e. ( G Ismt G ) <-> ( F : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) ) ) )
6	3 5	syl	|- ( ph -> ( F e. ( G Ismt G ) <-> ( F : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) ) ) )
7	4 6	mpbid	|- ( ph -> ( F : P -1-1-onto-> P /\ A. a e. P A. b e. P ( ( F ` a ) .- ( F ` b ) ) = ( a .- b ) ) )
8	7	simpld	|- ( ph -> F : P -1-1-onto-> P )