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 𝐺 = ( 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𝐴 ) )