Theorem motf1o

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

	Ref	Expression
Hypotheses	ismot.p	$$⊢P={\mathrm{Base}}_G$$
	ismot.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	motgrp.1	$$⊢\phi \to G\in V$$
	motco.2	$$⊢\phi \to F\in \left(GIsmtG\right)$$
Assertion	motf1o	$$⊢\phi \to F:P\underset{1-1\; onto}{⟶}P$$

Proof

Step	Hyp	Ref	Expression
1		ismot.p	$$⊢P={\mathrm{Base}}_G$$
2		ismot.m	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		motgrp.1	$$⊢\phi \to G\in V$$
4		motco.2	$$⊢\phi \to F\in \left(GIsmtG\right)$$
5	1 2	ismot	$$⊢G\in V\to \left(F\in \left(GIsmtG\right)\leftrightarrow \left(F:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in PF\left(a\right)\underset{\dot{}}{-}F\left(b\right)=a\underset{\dot{}}{-}b\right)\right)$$
6	3 5	syl	$$⊢\phi \to \left(F\in \left(GIsmtG\right)\leftrightarrow \left(F:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in PF\left(a\right)\underset{\dot{}}{-}F\left(b\right)=a\underset{\dot{}}{-}b\right)\right)$$
7	4 6	mpbid	$$⊢\phi \to \left(F:P\underset{1-1\; onto}{⟶}P\wedge \forall a\in P\forall b\in PF\left(a\right)\underset{\dot{}}{-}F\left(b\right)=a\underset{\dot{}}{-}b\right)$$
8	7	simpld	$$⊢\phi \to F:P\underset{1-1\; onto}{⟶}P$$