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 ⊢ ∼ ˙ = G ~ QG S
quseccl0.h ⊢ H = G / 𝑠 ∼ ˙
quseccl0.c ⊢ C = Base G
quseccl0.b ⊢ B = Base H
Assertion quseccl0 ⊢ G ∈ V ∧ X ∈ C → X ∼ ˙ ∈ B

Proof

Step Hyp Ref Expression
1 quseccl0.e ⊢ ∼ ˙ = G ~ QG S
2 quseccl0.h ⊢ H = G / 𝑠 ∼ ˙
3 quseccl0.c ⊢ C = Base G
4 quseccl0.b ⊢ B = Base H
5 1 ovexi ⊢ ∼ ˙ ∈ V
6 5 ecelqsi ⊢ X ∈ C → X ∼ ˙ ∈ C / ∼ ˙
7 6 adantl ⊢ G ∈ V ∧ X ∈ C → X ∼ ˙ ∈ C / ∼ ˙
8 2 a1i ⊢ G ∈ V ∧ X ∈ C → H = G / 𝑠 ∼ ˙
9 3 a1i ⊢ G ∈ V ∧ X ∈ C → C = Base G
10 5 a1i ⊢ G ∈ V ∧ X ∈ C → ∼ ˙ ∈ V
11 simpl ⊢ G ∈ V ∧ X ∈ C → G ∈ V
12 8 9 10 11 qusbas ⊢ G ∈ V ∧ X ∈ C → C / ∼ ˙ = Base H
13 12 4 eqtr4di ⊢ G ∈ V ∧ X ∈ C → C / ∼ ˙ = B
14 7 13 eleqtrd ⊢ G ∈ V ∧ X ∈ C → X ∼ ˙ ∈ B