Theorem quselbas

Description: Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025)

	Ref	Expression
Hypotheses	quselbas.e	|- .~ = ( G ~QG S )
	quselbas.u	|- U = ( G /s .~ )
	quselbas.b	|- B = ( Base ` G )
Assertion	quselbas	|- ( ( G e. V /\ X e. W ) -> ( X e. ( Base ` U ) <-> E. x e. B X = [ x ] .~ ) )

Proof

Step	Hyp	Ref	Expression
1		quselbas.e	|- .~ = ( G ~QG S )
2		quselbas.u	|- U = ( G /s .~ )
3		quselbas.b	|- B = ( Base ` G )
4	2	a1i	|- ( ( G e. V /\ X e. W ) -> U = ( G /s .~ ) )
5	3	a1i	|- ( ( G e. V /\ X e. W ) -> B = ( Base ` G ) )
6	1	ovexi	|- .~ e. _V
7	6	a1i	|- ( ( G e. V /\ X e. W ) -> .~ e. _V )
8		simpl	|- ( ( G e. V /\ X e. W ) -> G e. V )
9	4 5 7 8	qusbas	|- ( ( G e. V /\ X e. W ) -> ( B /. .~ ) = ( Base ` U ) )
10	9	eqcomd	|- ( ( G e. V /\ X e. W ) -> ( Base ` U ) = ( B /. .~ ) )
11	10	eleq2d	|- ( ( G e. V /\ X e. W ) -> ( X e. ( Base ` U ) <-> X e. ( B /. .~ ) ) )
12		elqsg	|- ( X e. W -> ( X e. ( B /. .~ ) <-> E. x e. B X = [ x ] .~ ) )
13	12	adantl	|- ( ( G e. V /\ X e. W ) -> ( X e. ( B /. .~ ) <-> E. x e. B X = [ x ] .~ ) )
14	11 13	bitrd	|- ( ( G e. V /\ X e. W ) -> ( X e. ( Base ` U ) <-> E. x e. B X = [ x ] .~ ) )