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