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	$$⊢\underset{\dot{}}{\sim }=G{~}_{\mathit{QG}}S$$
	quseccl0.h	$$⊢H=G{/}_{𝑠}\underset{\dot{}}{\sim }$$
	quseccl0.c	$$⊢C={\mathrm{Base}}_G$$
	quseccl0.b	$$⊢B={\mathrm{Base}}_H$$
Assertion	quseccl0	$$⊢\left(G\in V\wedge X\in C\right)\to \left[X\right]\underset{\dot{}}{\sim }\in B$$

Proof

Step	Hyp	Ref	Expression
1		quseccl0.e	$$⊢\underset{\dot{}}{\sim }=G{~}_{\mathit{QG}}S$$
2		quseccl0.h	$$⊢H=G{/}_{𝑠}\underset{\dot{}}{\sim }$$
3		quseccl0.c	$$⊢C={\mathrm{Base}}_G$$
4		quseccl0.b	$$⊢B={\mathrm{Base}}_H$$
5	1	ovexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
6	5	ecelqsi	$$⊢X\in C\to \left[X\right]\underset{\dot{}}{\sim }\in \left(C/\underset{\dot{}}{\sim }\right)$$
7	6	adantl	$$⊢\left(G\in V\wedge X\in C\right)\to \left[X\right]\underset{\dot{}}{\sim }\in \left(C/\underset{\dot{}}{\sim }\right)$$
8	2	a1i	$$⊢\left(G\in V\wedge X\in C\right)\to H=G{/}_{𝑠}\underset{\dot{}}{\sim }$$
9	3	a1i	$$⊢\left(G\in V\wedge X\in C\right)\to C={\mathrm{Base}}_G$$
10	5	a1i	$$⊢\left(G\in V\wedge X\in C\right)\to \underset{\dot{}}{\sim }\in \mathrm{V}$$
11		simpl	$$⊢\left(G\in V\wedge X\in C\right)\to G\in V$$
12	8 9 10 11	qusbas	$$⊢\left(G\in V\wedge X\in C\right)\to C/\underset{\dot{}}{\sim }={\mathrm{Base}}_H$$
13	12 4	eqtr4di	$$⊢\left(G\in V\wedge X\in C\right)\to C/\underset{\dot{}}{\sim }=B$$
14	7 13	eleqtrd	$$⊢\left(G\in V\wedge X\in C\right)\to \left[X\right]\underset{\dot{}}{\sim }\in B$$