Theorem qus0subgbas

Description: The base set of a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025)

	Ref	Expression
Hypotheses	qus0subg.0	|- .0. = ( 0g ` G )
	qus0subg.s	|- S = { .0. }
	qus0subg.e	|- .~ = ( G ~QG S )
	qus0subg.u	|- U = ( G /s .~ )
	qus0subg.b	|- B = ( Base ` G )
Assertion	qus0subgbas	|- ( G e. Grp -> ( Base ` U ) = { u | E. x e. B u = { x } } )

Proof

Step	Hyp	Ref	Expression
1		qus0subg.0	|- .0. = ( 0g ` G )
2		qus0subg.s	|- S = { .0. }
3		qus0subg.e	|- .~ = ( G ~QG S )
4		qus0subg.u	|- U = ( G /s .~ )
5		qus0subg.b	|- B = ( Base ` G )
6		df-qs	|- ( B /. .~ ) = { u | E. x e. B u = [ x ] .~ }
7	4	a1i	|- ( G e. Grp -> U = ( G /s .~ ) )
8	5	a1i	|- ( G e. Grp -> B = ( Base ` G ) )
9	3	ovexi	|- .~ e. _V
10	9	a1i	|- ( G e. Grp -> .~ e. _V )
11		id	|- ( G e. Grp -> G e. Grp )
12	7 8 10 11	qusbas	|- ( G e. Grp -> ( B /. .~ ) = ( Base ` U ) )
13	1 2 5 3	eqg0subgecsn	|- ( ( G e. Grp /\ x e. B ) -> [ x ] .~ = { x } )
14	13	eqeq2d	|- ( ( G e. Grp /\ x e. B ) -> ( u = [ x ] .~ <-> u = { x } ) )
15	14	rexbidva	|- ( G e. Grp -> ( E. x e. B u = [ x ] .~ <-> E. x e. B u = { x } ) )
16	15	abbidv	|- ( G e. Grp -> { u | E. x e. B u = [ x ] .~ } = { u | E. x e. B u = { x } } )
17	6 12 16	3eqtr3a	|- ( G e. Grp -> ( Base ` U ) = { u | E. x e. B u = { x } } )