Theorem trivnsimpgd

Description: Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	trivnsimpgd.1	|- B = ( Base ` G )
	trivnsimpgd.2	|- .0. = ( 0g ` G )
	trivnsimpgd.3	|- ( ph -> G e. Grp )
	trivnsimpgd.4	|- ( ph -> B = { .0. } )
Assertion	trivnsimpgd	|- ( ph -> -. G e. SimpGrp )

Proof

Step	Hyp	Ref	Expression
1		trivnsimpgd.1	|- B = ( Base ` G )
2		trivnsimpgd.2	|- .0. = ( 0g ` G )
3		trivnsimpgd.3	|- ( ph -> G e. Grp )
4		trivnsimpgd.4	|- ( ph -> B = { .0. } )
5		snnen2o	|- -. { B } ~~ 2o
6	1 2 3 4	trivnsgd	|- ( ph -> ( NrmSGrp ` G ) = { B } )
7	6	breq1d	|- ( ph -> ( ( NrmSGrp ` G ) ~~ 2o <-> { B } ~~ 2o ) )
8	5 7	mtbiri	|- ( ph -> -. ( NrmSGrp ` G ) ~~ 2o )
9		simpg2nsg	|- ( G e. SimpGrp -> ( NrmSGrp ` G ) ~~ 2o )
10	8 9	nsyl	|- ( ph -> -. G e. SimpGrp )