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

Metamath Proof Explorer

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 ) )