Metamath Proof Explorer

Theorem quselbas

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

Ref Expression
Hypotheses quselbas.e ⊢ ∼ ˙ = G ~ QG S
quselbas.u ⊢ U = G / 𝑠 ∼ ˙
quselbas.b ⊢ B = Base G
Assertion quselbas ⊢ G ∈ V ∧ X ∈ W → X ∈ Base U ↔ ∃ x ∈ B X = x ∼ ˙

Proof

Step Hyp Ref Expression
1 quselbas.e ⊢ ∼ ˙ = G ~ QG S
2 quselbas.u ⊢ U = G / 𝑠 ∼ ˙
3 quselbas.b ⊢ B = Base G
4 2 a1i ⊢ G ∈ V ∧ X ∈ W → U = G / 𝑠 ∼ ˙
5 3 a1i ⊢ G ∈ V ∧ X ∈ W → B = Base G
6 1 ovexi ⊢ ∼ ˙ ∈ V
7 6 a1i ⊢ G ∈ V ∧ X ∈ W → ∼ ˙ ∈ V
8 simpl ⊢ G ∈ V ∧ X ∈ W → G ∈ V
9 4 5 7 8 qusbas ⊢ G ∈ V ∧ X ∈ W → B / ∼ ˙ = Base U
10 9 eqcomd ⊢ G ∈ V ∧ X ∈ W → Base U = B / ∼ ˙
11 10 eleq2d ⊢ G ∈ V ∧ X ∈ W → X ∈ Base U ↔ X ∈ B / ∼ ˙
12 elqsg ⊢ X ∈ W → X ∈ B / ∼ ˙ ↔ ∃ x ∈ B X = x ∼ ˙
13 12 adantl ⊢ G ∈ V ∧ X ∈ W → X ∈ B / ∼ ˙ ↔ ∃ x ∈ B X = x ∼ ˙
14 11 13 bitrd ⊢ G ∈ V ∧ X ∈ W → X ∈ Base U ↔ ∃ x ∈ B X = x ∼ ˙