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

Metamath Proof Explorer

Theorem nsmndex1

Description: The base set B of the constructed monoid S is not a submonoid of the monoid M of endofunctions on set NN0 , although M e. Mnd and S e. Mnd and B C_ ( BaseM ) hold. (Contributed by AV, 17-Feb-2024)

		Ref	Expression
	Hypotheses	smndex1ibas.m	$⊢ M = EndoFMnd (ℕ_{0})$
		smndex1ibas.n	$⊢ N \in ℕ$
		smndex1ibas.i	$⊢ I = (x \in ℕ_{0} ⟼ x \mod N)$
		smndex1ibas.g	$⊢ G = (n \in (0 ..^N) ⟼ (x \in ℕ_{0} ⟼ n))$
		smndex1mgm.b	$⊢ B = \{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\}$
		smndex1mgm.s	$⊢ S = M ↾_{𝑠} B$
	Assertion	nsmndex1	$⊢ B \notin SubMnd (M)$

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	$⊢ M = EndoFMnd (ℕ_{0})$
2		smndex1ibas.n	$⊢ N \in ℕ$
3		smndex1ibas.i	$⊢ I = (x \in ℕ_{0} ⟼ x \mod N)$
4		smndex1ibas.g	$⊢ G = (n \in (0 ..^N) ⟼ (x \in ℕ_{0} ⟼ n))$
5		smndex1mgm.b	$⊢ B = \{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\}$
6		smndex1mgm.s	$⊢ S = M ↾_{𝑠} B$
7	1 2 3 4 5 6	smndex1n0mnd	$⊢ 0_{M} \notin B$
8	7	neli	$⊢ \neg 0_{M} \in B$
9	8	intnan	$⊢ \neg (B \subseteq {Base}_{M} \land 0_{M} \in B)$
10	9	intnan	$⊢ \neg ((M \in Mnd \land M ↾_{𝑠} B \in Mnd) \land (B \subseteq {Base}_{M} \land 0_{M} \in B))$
11		eqid	$⊢ {Base}_{M} = {Base}_{M}$
12		eqid	$⊢ 0_{M} = 0_{M}$
13	11 12	issubmndb	$⊢ B \in SubMnd (M) \leftrightarrow ((M \in Mnd \land M ↾_{𝑠} B \in Mnd) \land (B \subseteq {Base}_{M} \land 0_{M} \in B))$
14	10 13	mtbir	$⊢ \neg B \in SubMnd (M)$
15	14	nelir	$⊢ B \notin SubMnd (M)$