Theorem quselbas

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

	Ref	Expression
Hypotheses	quselbas.e	⊢ ∼ = ( 𝐺 ~QG 𝑆 )
	quselbas.u	⊢ 𝑈 = ( 𝐺 /s ∼ )
	quselbas.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	quselbas	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝑋 ∈ ( Base ‘ 𝑈 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )

Proof

Step	Hyp	Ref	Expression
1		quselbas.e	⊢ ∼ = ( 𝐺 ~QG 𝑆 )
2		quselbas.u	⊢ 𝑈 = ( 𝐺 /s ∼ )
3		quselbas.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4	2	a1i	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → 𝑈 = ( 𝐺 /s ∼ ) )
5	3	a1i	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → 𝐵 = ( Base ‘ 𝐺 ) )
6	1	ovexi	⊢ ∼ ∈ V
7	6	a1i	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ∼ ∈ V )
8		simpl	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → 𝐺 ∈ 𝑉 )
9	4 5 7 8	qusbas	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝐵 / ∼ ) = ( Base ‘ 𝑈 ) )
10	9	eqcomd	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( Base ‘ 𝑈 ) = ( 𝐵 / ∼ ) )
11	10	eleq2d	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝑋 ∈ ( Base ‘ 𝑈 ) ↔ 𝑋 ∈ ( 𝐵 / ∼ ) ) )
12		elqsg	⊢ ( 𝑋 ∈ 𝑊 → ( 𝑋 ∈ ( 𝐵 / ∼ ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )
13	12	adantl	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝑋 ∈ ( 𝐵 / ∼ ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )
14	11 13	bitrd	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝑋 ∈ ( Base ‘ 𝑈 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑋 = [ 𝑥 ] ∼ ) )