Theorem quseccl0

Description: Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015) Generalization of quseccl for arbitrary sets G . (Revised by AV, 24-Feb-2025)

	Ref	Expression
Hypotheses	quseccl0.e	|- .~ = ( G ~QG S )
	quseccl0.h	|- H = ( G /s .~ )
	quseccl0.c	|- C = ( Base ` G )
	quseccl0.b	|- B = ( Base ` H )
Assertion	quseccl0	|- ( ( G e. V /\ X e. C ) -> [ X ] .~ e. B )

Proof

Step	Hyp	Ref	Expression
1		quseccl0.e	|- .~ = ( G ~QG S )
2		quseccl0.h	|- H = ( G /s .~ )
3		quseccl0.c	|- C = ( Base ` G )
4		quseccl0.b	|- B = ( Base ` H )
5	1	ovexi	|- .~ e. _V
6	5	ecelqsi	|- ( X e. C -> [ X ] .~ e. ( C /. .~ ) )
7	6	adantl	|- ( ( G e. V /\ X e. C ) -> [ X ] .~ e. ( C /. .~ ) )
8	2	a1i	|- ( ( G e. V /\ X e. C ) -> H = ( G /s .~ ) )
9	3	a1i	|- ( ( G e. V /\ X e. C ) -> C = ( Base ` G ) )
10	5	a1i	|- ( ( G e. V /\ X e. C ) -> .~ e. _V )
11		simpl	|- ( ( G e. V /\ X e. C ) -> G e. V )
12	8 9 10 11	qusbas	|- ( ( G e. V /\ X e. C ) -> ( C /. .~ ) = ( Base ` H ) )
13	12 4	eqtr4di	|- ( ( G e. V /\ X e. C ) -> ( C /. .~ ) = B )
14	7 13	eleqtrd	|- ( ( G e. V /\ X e. C ) -> [ X ] .~ e. B )