This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ) → [ 𝑋 ] ∼ ∈ 𝐵 )