Theorem nelsubginvcld

Description: The inverse of a non-subgroup-member is a non-subgroup-member. (Contributed by Steven Nguyen, 15-Apr-2023)

	Ref	Expression
Hypotheses	nelsubginvcld.g	|- ( ph -> G e. Grp )
	nelsubginvcld.s	|- ( ph -> S e. ( SubGrp ` G ) )
	nelsubginvcld.x	|- ( ph -> X e. ( B \ S ) )
	nelsubginvcld.b	|- B = ( Base ` G )
	nelsubginvcld.p	|- N = ( invg ` G )
Assertion	nelsubginvcld	|- ( ph -> ( N ` X ) e. ( B \ S ) )

Proof

Step	Hyp	Ref	Expression
1		nelsubginvcld.g	|- ( ph -> G e. Grp )
2		nelsubginvcld.s	|- ( ph -> S e. ( SubGrp ` G ) )
3		nelsubginvcld.x	|- ( ph -> X e. ( B \ S ) )
4		nelsubginvcld.b	|- B = ( Base ` G )
5		nelsubginvcld.p	|- N = ( invg ` G )
6	3	eldifad	|- ( ph -> X e. B )
7	4 5	grpinvcl	|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
8	1 6 7	syl2anc	|- ( ph -> ( N ` X ) e. B )
9	3	eldifbd	|- ( ph -> -. X e. S )
10	4 5	grpinvinv	|- ( ( G e. Grp /\ X e. B ) -> ( N ` ( N ` X ) ) = X )
11	1 6 10	syl2anc	|- ( ph -> ( N ` ( N ` X ) ) = X )
12	11	adantr	|- ( ( ph /\ ( N ` X ) e. S ) -> ( N ` ( N ` X ) ) = X )
13	5	subginvcl	|- ( ( S e. ( SubGrp ` G ) /\ ( N ` X ) e. S ) -> ( N ` ( N ` X ) ) e. S )
14	2 13	sylan	|- ( ( ph /\ ( N ` X ) e. S ) -> ( N ` ( N ` X ) ) e. S )
15	12 14	eqeltrrd	|- ( ( ph /\ ( N ` X ) e. S ) -> X e. S )
16	9 15	mtand	|- ( ph -> -. ( N ` X ) e. S )
17	8 16	eldifd	|- ( ph -> ( N ` X ) e. ( B \ S ) )