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	⊢ ∼ = ( 𝐺 ~QG 𝑆 )
	quseccl0.h	⊢ 𝐻 = ( 𝐺 /s ∼ )
	quseccl0.c	⊢ 𝐶 = ( Base ‘ 𝐺 )
	quseccl0.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion	quseccl0	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → [ 𝑋 ] ∼ ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		quseccl0.e	⊢ ∼ = ( 𝐺 ~QG 𝑆 )
2		quseccl0.h	⊢ 𝐻 = ( 𝐺 /s ∼ )
3		quseccl0.c	⊢ 𝐶 = ( Base ‘ 𝐺 )
4		quseccl0.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
5	1	ovexi	⊢ ∼ ∈ V
6	5	ecelqsi	⊢ ( 𝑋 ∈ 𝐶 → [ 𝑋 ] ∼ ∈ ( 𝐶 / ∼ ) )
7	6	adantl	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → [ 𝑋 ] ∼ ∈ ( 𝐶 / ∼ ) )
8	2	a1i	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → 𝐻 = ( 𝐺 /s ∼ ) )
9	3	a1i	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → 𝐶 = ( Base ‘ 𝐺 ) )
10	5	a1i	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → ∼ ∈ V )
11		simpl	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → 𝐺 ∈ 𝑉 )
12	8 9 10 11	qusbas	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐶 / ∼ ) = ( Base ‘ 𝐻 ) )
13	12 4	eqtr4di	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐶 / ∼ ) = 𝐵 )
14	7 13	eleqtrd	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → [ 𝑋 ] ∼ ∈ 𝐵 )