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

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		f1oeq1	⊢ ( 𝑥 = 𝐹 → ( 𝑥 : 𝐴 –1-1-onto→ 𝐴 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐴 ) )
4	1 2	symgbas	⊢ 𝐵 = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 }
5	3 4	elab2g	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐵 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝐴 ) )