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

Metamath Proof Explorer

Theorem elsymgbas

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

Ref Expression
Hypotheses symgbas.1 ⊢ G = SymGrp ⁡ A
symgbas.2 ⊢ B = Base G
Assertion elsymgbas ⊢ A ∈ V → F ∈ B ↔ F : A ⟶ 1-1 onto A

Proof

Step Hyp Ref Expression
1 symgbas.1 ⊢ G = SymGrp ⁡ A
2 symgbas.2 ⊢ B = Base G
3 elex ⊢ F ∈ B → F ∈ V
4 3 a1i ⊢ A ∈ V → F ∈ B → F ∈ V
5 f1of ⊢ F : A ⟶ 1-1 onto A → F : A ⟶ A
6 fex ⊢ F : A ⟶ A ∧ A ∈ V → F ∈ V
7 6 expcom ⊢ A ∈ V → F : A ⟶ A → F ∈ V
8 5 7 syl5 ⊢ A ∈ V → F : A ⟶ 1-1 onto A → F ∈ V
9 1 2 elsymgbas2 ⊢ F ∈ V → F ∈ B ↔ F : A ⟶ 1-1 onto A
10 9 a1i ⊢ A ∈ V → F ∈ V → F ∈ B ↔ F : A ⟶ 1-1 onto A
11 4 8 10 pm5.21ndd ⊢ A ∈ V → F ∈ B ↔ F : A ⟶ 1-1 onto A