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	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	elsymgbas	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		elex	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ V )
4	3	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ∈ 𝐵 → 𝐹 ∈ V ) )
5		f1of	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 : 𝐴 ⟶ 𝐴 )
6		fex	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
7	6	expcom	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : 𝐴 ⟶ 𝐴 → 𝐹 ∈ V ) )
8	5 7	syl5	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 ∈ V ) )
9	1 2	elsymgbas2	⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐴 ) )
10	9	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ∈ V → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐴 ) ) )
11	4 8 10	pm5.21ndd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐴 ) )