quselbas

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

	Ref	Expression
Hypotheses	quselbas.e	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
	quselbas.u	$⊢ U = G /_{𝑠} \underset{˙}{\sim}$
	quselbas.b	$⊢ B = {Base}_{G}$
Assertion	quselbas	$⊢ (G \in V \land X \in W) \to (X \in {Base}_{U} \leftrightarrow \exists x \in B X = [x] \underset{˙}{\sim})$

Step	Hyp	Ref	Expression
1		quselbas.e	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
2		quselbas.u	$⊢ U = G /_{𝑠} \underset{˙}{\sim}$
3		quselbas.b	$⊢ B = {Base}_{G}$
4	2	a1i	$⊢ (G \in V \land X \in W) \to U = G /_{𝑠} \underset{˙}{\sim}$
5	3	a1i	$⊢ (G \in V \land X \in W) \to B = {Base}_{G}$
6	1	ovexi	$⊢ \underset{˙}{\sim} \in V$
7	6	a1i	$⊢ (G \in V \land X \in W) \to \underset{˙}{\sim} \in V$
8		simpl	$⊢ (G \in V \land X \in W) \to G \in V$
9	4 5 7 8	qusbas	$⊢ (G \in V \land X \in W) \to B / \underset{˙}{\sim} = {Base}_{U}$
10	9	eqcomd	$⊢ (G \in V \land X \in W) \to {Base}_{U} = B / \underset{˙}{\sim}$
11	10	eleq2d	$⊢ (G \in V \land X \in W) \to (X \in {Base}_{U} \leftrightarrow X \in (B / \underset{˙}{\sim}))$
12		elqsg	$⊢ X \in W \to (X \in (B / \underset{˙}{\sim}) \leftrightarrow \exists x \in B X = [x] \underset{˙}{\sim})$
13	12	adantl	$⊢ (G \in V \land X \in W) \to (X \in (B / \underset{˙}{\sim}) \leftrightarrow \exists x \in B X = [x] \underset{˙}{\sim})$
14	11 13	bitrd	$⊢ (G \in V \land X \in W) \to (X \in {Base}_{U} \leftrightarrow \exists x \in B X = [x] \underset{˙}{\sim})$

Metamath Proof Explorer