Theorem symgbasexOLD

Description: Obsolete as of 8-Aug-2024. B e. _V follows immediatly from fvex . (Contributed by AV, 30-Mar-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	symgbasexOLD	⊢ ( 𝐴 ∈ 𝑉 → 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3	1 2	symgbas	⊢ 𝐵 = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 }
4		permsetexOLD	⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ∈ V )
5	3 4	eqeltrid	⊢ ( 𝐴 ∈ 𝑉 → 𝐵 ∈ V )