Theorem 0subgALT

Description: A shorter proof of 0subg using df-od . (Contributed by SN, 31-Jan-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	0subgALT.z	|- .0. = ( 0g ` G )
Assertion	0subgALT	|- ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )

Proof

Step	Hyp	Ref	Expression
1		0subgALT.z	|- .0. = ( 0g ` G )
2		eqid	|- ( od ` G ) = ( od ` G )
3		id	|- ( G e. Grp -> G e. Grp )
4		grpmnd	|- ( G e. Grp -> G e. Mnd )
5	1	0subm	|- ( G e. Mnd -> { .0. } e. ( SubMnd ` G ) )
6	4 5	syl	|- ( G e. Grp -> { .0. } e. ( SubMnd ` G ) )
7	2 1	od1	|- ( G e. Grp -> ( ( od ` G ) ` .0. ) = 1 )
8		1nn	|- 1 e. NN
9	7 8	eqeltrdi	|- ( G e. Grp -> ( ( od ` G ) ` .0. ) e. NN )
10	1	fvexi	|- .0. e. _V
11		fveq2	|- ( a = .0. -> ( ( od ` G ) ` a ) = ( ( od ` G ) ` .0. ) )
12	11	eleq1d	|- ( a = .0. -> ( ( ( od ` G ) ` a ) e. NN <-> ( ( od ` G ) ` .0. ) e. NN ) )
13	10 12	ralsn	|- ( A. a e. { .0. } ( ( od ` G ) ` a ) e. NN <-> ( ( od ` G ) ` .0. ) e. NN )
14	9 13	sylibr	|- ( G e. Grp -> A. a e. { .0. } ( ( od ` G ) ` a ) e. NN )
15	2 3 6 14	finodsubmsubg	|- ( G e. Grp -> { .0. } e. ( SubGrp ` G ) )