0frgp

Description: The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	0frgp.g	$⊢ G = freeGrp (\emptyset)$
	0frgp.b	$⊢ B = {Base}_{G}$
Assertion	0frgp	$⊢ B \approx 1_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		0frgp.g	$⊢ G = freeGrp (\emptyset)$
2		0frgp.b	$⊢ B = {Base}_{G}$
3		0ex	$⊢ \emptyset \in V$
4	1	frgpgrp	$⊢ \emptyset \in V \to G \in Grp$
5	3 4	ax-mp	$⊢ G \in Grp$
6		f0	$⊢ \emptyset : \emptyset ⟶ B$
7		eqid	$⊢ ~_{FG} (\emptyset) = ~_{FG} (\emptyset)$
8		eqid	$⊢ {var}_{FGrp} (\emptyset) = {var}_{FGrp} (\emptyset)$
9	7 8 1 2	vrgpf	$⊢ \emptyset \in V \to {var}_{FGrp} (\emptyset) : \emptyset ⟶ B$
10		ffn	$⊢ {var}_{FGrp} (\emptyset) : \emptyset ⟶ B \to {var}_{FGrp} (\emptyset) Fn \emptyset$
11	3 9 10	mp2b	$⊢ {var}_{FGrp} (\emptyset) Fn \emptyset$
12		fn0	$⊢ {var}_{FGrp} (\emptyset) Fn \emptyset \leftrightarrow {var}_{FGrp} (\emptyset) = \emptyset$
13	11 12	mpbi	$⊢ {var}_{FGrp} (\emptyset) = \emptyset$
14	13	eqcomi	$⊢ \emptyset = {var}_{FGrp} (\emptyset)$
15	1 2 14	frgpup3	$⊢ (G \in Grp \land \emptyset \in V \land \emptyset : \emptyset ⟶ B) \to \exists! f \in (G GrpHom G) f \circ \emptyset = \emptyset$
16	5 3 6 15	mp3an	$⊢ \exists! f \in (G GrpHom G) f \circ \emptyset = \emptyset$
17		reurmo	$⊢ \exists! f \in (G GrpHom G) f \circ \emptyset = \emptyset \to \exists^{*} f \in (G GrpHom G) f \circ \emptyset = \emptyset$
18	16 17	ax-mp	$⊢ \exists^{*} f \in (G GrpHom G) f \circ \emptyset = \emptyset$
19	2	idghm	$⊢ G \in Grp \to {I ↾}_{B} \in (G GrpHom G)$
20	5 19	ax-mp	$⊢ {I ↾}_{B} \in (G GrpHom G)$
21		tru	$⊢ ⊤$
22	20 21	pm3.2i	$⊢ ({I ↾}_{B} \in (G GrpHom G) \land ⊤)$
23		eqid	$⊢ 0_{G} = 0_{G}$
24	23 2	0ghm	$⊢ (G \in Grp \land G \in Grp) \to B \times \{0_{G}\} \in (G GrpHom G)$
25	5 5 24	mp2an	$⊢ B \times \{0_{G}\} \in (G GrpHom G)$
26	25 21	pm3.2i	$⊢ (B \times \{0_{G}\} \in (G GrpHom G) \land ⊤)$
27		co02	$⊢ f \circ \emptyset = \emptyset$
28	27	bitru	$⊢ f \circ \emptyset = \emptyset \leftrightarrow ⊤$
29	28	a1i	$⊢ f = {I ↾}_{B} \to (f \circ \emptyset = \emptyset \leftrightarrow ⊤)$
30	28	a1i	$⊢ f = B \times \{0_{G}\} \to (f \circ \emptyset = \emptyset \leftrightarrow ⊤)$
31	29 30	rmoi	$⊢ (\exists^{*} f \in (G GrpHom G) f \circ \emptyset = \emptyset \land ({I ↾}_{B} \in (G GrpHom G) \land ⊤) \land (B \times \{0_{G}\} \in (G GrpHom G) \land ⊤)) \to {I ↾}_{B} = B \times \{0_{G}\}$
32	18 22 26 31	mp3an	$⊢ {I ↾}_{B} = B \times \{0_{G}\}$
33		mptresid	$⊢ {I ↾}_{B} = (x \in B ⟼ x)$
34		fconstmpt	$⊢ B \times \{0_{G}\} = (x \in B ⟼ 0_{G})$
35	32 33 34	3eqtr3i	$⊢ (x \in B ⟼ x) = (x \in B ⟼ 0_{G})$
36		mpteqb	$⊢ \forall x \in B x \in B \to ((x \in B ⟼ x) = (x \in B ⟼ 0_{G}) \leftrightarrow \forall x \in B x = 0_{G})$
37		id	$⊢ x \in B \to x \in B$
38	36 37	mprg	$⊢ (x \in B ⟼ x) = (x \in B ⟼ 0_{G}) \leftrightarrow \forall x \in B x = 0_{G}$
39	35 38	mpbi	$⊢ \forall x \in B x = 0_{G}$
40	39	rspec	$⊢ x \in B \to x = 0_{G}$
41		velsn	$⊢ x \in \{0_{G}\} \leftrightarrow x = 0_{G}$
42	40 41	sylibr	$⊢ x \in B \to x \in \{0_{G}\}$
43	42	ssriv	$⊢ B \subseteq \{0_{G}\}$
44	2 23	grpidcl	$⊢ G \in Grp \to 0_{G} \in B$
45	5 44	ax-mp	$⊢ 0_{G} \in B$
46		snssi	$⊢ 0_{G} \in B \to \{0_{G}\} \subseteq B$
47	45 46	ax-mp	$⊢ \{0_{G}\} \subseteq B$
48	43 47	eqssi	$⊢ B = \{0_{G}\}$
49		fvex	$⊢ 0_{G} \in V$
50	49	ensn1	$⊢ \{0_{G}\} \approx 1_{𝑜}$
51	48 50	eqbrtri	$⊢ B \approx 1_{𝑜}$

Metamath Proof Explorer

Theorem 0frgp

Proof