Theorem nsgqusf1o

Description: The canonical projection homomorphism E defines a bijective correspondence between the set S of subgroups of G containing a normal subgroup N and the subgroups of the quotient group G / N . This theorem is sometimes called the correspondence theorem, or the fourth isomorphism theorem. (Contributed by Thierry Arnoux, 4-Aug-2024)

	Ref	Expression
Hypotheses	nsgqusf1o.b	$$⊢B={\mathrm{Base}}_G$$
	nsgqusf1o.s	$$⊢S=\left\{h\in \mathrm{SubGrp}\left(G\right)|N\subseteq h\right\}$$
	nsgqusf1o.t	$$⊢T=\mathrm{SubGrp}\left(Q\right)$$
	nsgqusf1o.1	$$⊢\underset{\dot{}}{\le }={\le }_{\mathrm{toInc}\left(S\right)}$$
	nsgqusf1o.2	No typesetting found for |- .c_ = ( le ` ( toInc ` T ) ) with typecode |-
	nsgqusf1o.q	$$⊢Q=G{/}_{𝑠}\left(G{~}_{\mathit{QG}}N\right)$$
	nsgqusf1o.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
	nsgqusf1o.e	$$⊢E=\left(h\in S⟼\mathrm{ran}\left(x\in h⟼\left\{x\right\}\underset{\dot{}}{\oplus }N\right)\right)$$
	nsgqusf1o.f	$$⊢F=\left(f\in T⟼\left\{a\in B|\left\{a\right\}\underset{\dot{}}{\oplus }N\in f\right\}\right)$$
	nsgqusf1o.n	$$⊢\phi \to N\in \mathrm{NrmSGrp}\left(G\right)$$
Assertion	nsgqusf1o	$$⊢\phi \to E:S\underset{1-1\; onto}{⟶}T$$

Proof

Step	Hyp	Ref	Expression
1		nsgqusf1o.b	$$⊢B={\mathrm{Base}}_G$$
2		nsgqusf1o.s	$$⊢S=\left\{h\in \mathrm{SubGrp}\left(G\right)|N\subseteq h\right\}$$
3		nsgqusf1o.t	$$⊢T=\mathrm{SubGrp}\left(Q\right)$$
4		nsgqusf1o.1	$$⊢\underset{\dot{}}{\le }={\le }_{\mathrm{toInc}\left(S\right)}$$
5		nsgqusf1o.2	Could not format .c_ = ( le ` ( toInc ` T ) ) : No typesetting found for |- .c_ = ( le ` ( toInc ` T ) ) with typecode |-
6		nsgqusf1o.q	$$⊢Q=G{/}_{𝑠}\left(G{~}_{\mathit{QG}}N\right)$$
7		nsgqusf1o.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(G\right)$$
8		nsgqusf1o.e	$$⊢E=\left(h\in S⟼\mathrm{ran}\left(x\in h⟼\left\{x\right\}\underset{\dot{}}{\oplus }N\right)\right)$$
9		nsgqusf1o.f	$$⊢F=\left(f\in T⟼\left\{a\in B|\left\{a\right\}\underset{\dot{}}{\oplus }N\in f\right\}\right)$$
10		nsgqusf1o.n	$$⊢\phi \to N\in \mathrm{NrmSGrp}\left(G\right)$$
11		eqid	$$⊢\mathrm{toInc}\left(S\right)\mathrm{MGalConn}\mathrm{toInc}\left(T\right)=\mathrm{toInc}\left(S\right)\mathrm{MGalConn}\mathrm{toInc}\left(T\right)$$
12		fvex	$$⊢\mathrm{SubGrp}\left(G\right)\in \mathrm{V}$$
13	2 12	rabex2	$$⊢S\in \mathrm{V}$$
14		eqid	$$⊢\mathrm{toInc}\left(S\right)=\mathrm{toInc}\left(S\right)$$
15	14	ipobas	$$⊢S\in \mathrm{V}\to S={\mathrm{Base}}_{\mathrm{toInc}\left(S\right)}$$
16	13 15	ax-mp	$$⊢S={\mathrm{Base}}_{\mathrm{toInc}\left(S\right)}$$
17	3	fvexi	$$⊢T\in \mathrm{V}$$
18		eqid	$$⊢\mathrm{toInc}\left(T\right)=\mathrm{toInc}\left(T\right)$$
19	18	ipobas	$$⊢T\in \mathrm{V}\to T={\mathrm{Base}}_{\mathrm{toInc}\left(T\right)}$$
20	17 19	ax-mp	$$⊢T={\mathrm{Base}}_{\mathrm{toInc}\left(T\right)}$$
21	14	ipopos	$$⊢\mathrm{toInc}\left(S\right)\in \mathrm{Poset}$$
22	21	a1i	$$⊢\phi \to \mathrm{toInc}\left(S\right)\in \mathrm{Poset}$$
23	18	ipopos	$$⊢\mathrm{toInc}\left(T\right)\in \mathrm{Poset}$$
24	23	a1i	$$⊢\phi \to \mathrm{toInc}\left(T\right)\in \mathrm{Poset}$$
25	1 2 3 11 14 18 6 7 8 9 10	nsgmgc	$$⊢\phi \to E\left(\mathrm{toInc}\left(S\right)\mathrm{MGalConn}\mathrm{toInc}\left(T\right)\right)F$$
26	11 16 20 4 5 22 24 25	mgcf1o	Could not format ( ph -> ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) ) : No typesetting found for |- ( ph -> ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) ) with typecode |-
27		isof1o	Could not format ( ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) -> ( E |` ran F ) : ran F -1-1-onto-> ran E ) : No typesetting found for |- ( ( E |` ran F ) Isom .<_ , .c_ ( ran F , ran E ) -> ( E |` ran F ) : ran F -1-1-onto-> ran E ) with typecode |-
28	26 27	syl	$$⊢\phi \to \left({E\upharpoonright }_{\mathrm{ran}F}\right):\mathrm{ran}F\underset{1-1\; onto}{⟶}\mathrm{ran}E$$
29	1 2 3 4 5 6 7 8 9 10	nsgqusf1olem3	$$⊢\phi \to \mathrm{ran}F=S$$
30	29	reseq2d	$$⊢\phi \to {E\upharpoonright }_{\mathrm{ran}F}={E\upharpoonright }_S$$
31		nfv	$$⊢Ⅎh\phi$$
32		vex	$$⊢h\in \mathrm{V}$$
33	32	mptex	$$⊢\left(x\in h⟼\left\{x\right\}\underset{\dot{}}{\oplus }N\right)\in \mathrm{V}$$
34	33	rnex	$$⊢\mathrm{ran}\left(x\in h⟼\left\{x\right\}\underset{\dot{}}{\oplus }N\right)\in \mathrm{V}$$
35	34	a1i	$$⊢\left(\phi \wedge h\in S\right)\to \mathrm{ran}\left(x\in h⟼\left\{x\right\}\underset{\dot{}}{\oplus }N\right)\in \mathrm{V}$$
36	31 35 8	fnmptd	$$⊢\phi \to EFnS$$
37		fnresdm	$$⊢EFnS\to {E\upharpoonright }_S=E$$
38	36 37	syl	$$⊢\phi \to {E\upharpoonright }_S=E$$
39	30 38	eqtrd	$$⊢\phi \to {E\upharpoonright }_{\mathrm{ran}F}=E$$
40	1 2 3 4 5 6 7 8 9 10	nsgqusf1olem2	$$⊢\phi \to \mathrm{ran}E=T$$
41	39 29 40	f1oeq123d	$$⊢\phi \to \left(\left({E\upharpoonright }_{\mathrm{ran}F}\right):\mathrm{ran}F\underset{1-1\; onto}{⟶}\mathrm{ran}E\leftrightarrow E:S\underset{1-1\; onto}{⟶}T\right)$$
42	28 41	mpbid	$$⊢\phi \to E:S\underset{1-1\; onto}{⟶}T$$