This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elsymgbas2

Description: Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Mario Carneiro, 28-Jan-2015)

	Ref	Expression
Hypotheses	symgbas.1	$⊢ G = SymGrp (A)$
	symgbas.2	$⊢ B = {Base}_{G}$
Assertion	elsymgbas2	$⊢ F \in V \to (F \in B \leftrightarrow F : A \underset{1-1 onto}{⟶} A)$

Step	Hyp	Ref	Expression
1		symgbas.1	$⊢ G = SymGrp (A)$
2		symgbas.2	$⊢ B = {Base}_{G}$
3		f1oeq1	$⊢ x = F \to (x : A \underset{1-1 onto}{⟶} A \leftrightarrow F : A \underset{1-1 onto}{⟶} A)$
4	1 2	symgbas	$⊢ B = \{x \| x : A \underset{1-1 onto}{⟶} A\}$
5	3 4	elab2g	$⊢ F \in V \to (F \in B \leftrightarrow F : A \underset{1-1 onto}{⟶} A)$