cyc3evpm

Description: 3-Cycles are even permutations. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Hypotheses	cyc3evpm.t	$⊢ C = toCyc (D) [{\|.\|}^{-1} [\{3\}]]$
	cyc3evpm.a	$⊢ A = pmEven (D)$
Assertion	cyc3evpm	$⊢ D \in Fin \to C \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		cyc3evpm.t	$⊢ C = toCyc (D) [{\|.\|}^{-1} [\{3\}]]$
2		cyc3evpm.a	$⊢ A = pmEven (D)$
3		simpr	$⊢ (((D \in Fin \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land toCyc (D) (u) = p) \to toCyc (D) (u) = p$
4		simpl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to D \in Fin$
5		eqid	$⊢ toCyc (D) = toCyc (D)$
6		simpr	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])$
7	6	elin1d	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
8		elrabi	$⊢ u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \to u \in Word D$
9	7 8	syl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u \in Word D$
10		id	$⊢ w = u \to w = u$
11		dmeq	$⊢ w = u \to dom w = dom u$
12		eqidd	$⊢ w = u \to D = D$
13	10 11 12	f1eq123d	$⊢ w = u \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow u : dom u \underset{1-1}{⟶} D)$
14	13	elrab	$⊢ u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \leftrightarrow (u \in Word D \land u : dom u \underset{1-1}{⟶} D)$
15	14	simprbi	$⊢ u \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \to u : dom u \underset{1-1}{⟶} D$
16	7 15	syl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u : dom u \underset{1-1}{⟶} D$
17		eqid	$⊢ SymGrp (D) = SymGrp (D)$
18	5 4 9 16 17	cycpmcl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (u) \in {Base}_{SymGrp (D)}$
19		c0ex	$⊢ 0 \in V$
20	19	tpid1	$⊢ 0 \in \{0, 1, 2\}$
21		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
22	20 21	eleqtrri	$⊢ 0 \in (0 ..^3)$
23	6	elin2d	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u \in {\|.\|}^{-1} [\{3\}]$
24		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
25		ffn	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \to \|.\| Fn V$
26		elpreima	$⊢ \|.\| Fn V \to (u \in {\|.\|}^{-1} [\{3\}] \leftrightarrow (u \in V \land \|u\| \in \{3\}))$
27	24 25 26	mp2b	$⊢ u \in {\|.\|}^{-1} [\{3\}] \leftrightarrow (u \in V \land \|u\| \in \{3\})$
28	27	simprbi	$⊢ u \in {\|.\|}^{-1} [\{3\}] \to \|u\| \in \{3\}$
29		elsni	$⊢ \|u\| \in \{3\} \to \|u\| = 3$
30	23 28 29	3syl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to \|u\| = 3$
31	30	oveq2d	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to (0 ..^\|u\|) = (0 ..^3)$
32	22 31	eleqtrrid	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to 0 \in (0 ..^\|u\|)$
33		wrdsymbcl	$⊢ (u \in Word D \land 0 \in (0 ..^\|u\|)) \to u (0) \in D$
34	9 32 33	syl2anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (0) \in D$
35		1eltp012	$⊢ 1 \in \{0, 1, 2\}$
36	35 21	eleqtrri	$⊢ 1 \in (0 ..^3)$
37	36 31	eleqtrrid	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to 1 \in (0 ..^\|u\|)$
38		wrdsymbcl	$⊢ (u \in Word D \land 1 \in (0 ..^\|u\|)) \to u (1) \in D$
39	9 37 38	syl2anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (1) \in D$
40		2ex	$⊢ 2 \in V$
41	40	tpid3	$⊢ 2 \in \{0, 1, 2\}$
42	41 21	eleqtrri	$⊢ 2 \in (0 ..^3)$
43	42 31	eleqtrrid	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to 2 \in (0 ..^\|u\|)$
44		wrdsymbcl	$⊢ (u \in Word D \land 2 \in (0 ..^\|u\|)) \to u (2) \in D$
45	9 43 44	syl2anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (2) \in D$
46	34 39 45	3jca	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to (u (0) \in D \land u (1) \in D \land u (2) \in D)$
47		eqidd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (0) = u (0)$
48		eqidd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (1) = u (1)$
49		eqidd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (2) = u (2)$
50	47 48 49	3jca	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to (u (0) = u (0) \land u (1) = u (1) \land u (2) = u (2))$
51		eqwrds3	$⊢ (u \in Word D \land (u (0) \in D \land u (1) \in D \land u (2) \in D)) \to (u = ⟨“ u (0) u (1) u (2) ”⟩ \leftrightarrow (\|u\| = 3 \land (u (0) = u (0) \land u (1) = u (1) \land u (2) = u (2))))$
52	51	biimpar	$⊢ ((u \in Word D \land (u (0) \in D \land u (1) \in D \land u (2) \in D)) \land (\|u\| = 3 \land (u (0) = u (0) \land u (1) = u (1) \land u (2) = u (2)))) \to u = ⟨“ u (0) u (1) u (2) ”⟩$
53	9 46 30 50 52	syl22anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u = ⟨“ u (0) u (1) u (2) ”⟩$
54	53	fveq2d	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (u) = toCyc (D) (⟨“ u (0) u (1) u (2) ”⟩)$
55		wrddm	$⊢ u \in Word D \to dom u = (0 ..^\|u\|)$
56	9 55	syl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to dom u = (0 ..^\|u\|)$
57	56 31	eqtrd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to dom u = (0 ..^3)$
58	57 21	eqtrdi	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to dom u = \{0, 1, 2\}$
59		f1eq2	$⊢ dom u = \{0, 1, 2\} \to (u : dom u \underset{1-1}{⟶} D \leftrightarrow u : \{0, 1, 2\} \underset{1-1}{⟶} D)$
60	59	biimpa	$⊢ (dom u = \{0, 1, 2\} \land u : dom u \underset{1-1}{⟶} D) \to u : \{0, 1, 2\} \underset{1-1}{⟶} D$
61	58 16 60	syl2anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u : \{0, 1, 2\} \underset{1-1}{⟶} D$
62		1ex	$⊢ 1 \in V$
63	19 62 40	3pm3.2i	$⊢ (0 \in V \land 1 \in V \land 2 \in V)$
64		0ne1	$⊢ 0 \neq 1$
65		0ne2	$⊢ 0 \neq 2$
66		1ne2	$⊢ 1 \neq 2$
67	64 65 66	3pm3.2i	$⊢ (0 \neq 1 \land 0 \neq 2 \land 1 \neq 2)$
68		eqid	$⊢ \{0, 1, 2\} = \{0, 1, 2\}$
69	68	f13dfv	$⊢ ((0 \in V \land 1 \in V \land 2 \in V) \land (0 \neq 1 \land 0 \neq 2 \land 1 \neq 2)) \to (u : \{0, 1, 2\} \underset{1-1}{⟶} D \leftrightarrow (u : \{0, 1, 2\} ⟶ D \land (u (0) \neq u (1) \land u (0) \neq u (2) \land u (1) \neq u (2))))$
70	63 67 69	mp2an	$⊢ u : \{0, 1, 2\} \underset{1-1}{⟶} D \leftrightarrow (u : \{0, 1, 2\} ⟶ D \land (u (0) \neq u (1) \land u (0) \neq u (2) \land u (1) \neq u (2)))$
71	70	simprbi	$⊢ u : \{0, 1, 2\} \underset{1-1}{⟶} D \to (u (0) \neq u (1) \land u (0) \neq u (2) \land u (1) \neq u (2))$
72	61 71	syl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to (u (0) \neq u (1) \land u (0) \neq u (2) \land u (1) \neq u (2))$
73	72	simp1d	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (0) \neq u (1)$
74	72	simp3d	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (1) \neq u (2)$
75	72	simp2d	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (0) \neq u (2)$
76	75	necomd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to u (2) \neq u (0)$
77		eqid	$⊢ +_{SymGrp (D)} = +_{SymGrp (D)}$
78	5 17 4 34 39 45 73 74 76 77	cyc3co2	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (⟨“ u (0) u (1) u (2) ”⟩) = toCyc (D) (⟨“ u (0) u (2) ”⟩) +_{SymGrp (D)} toCyc (D) (⟨“ u (0) u (1) ”⟩)$
79	5 4 34 45 75 17	cycpm2cl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (⟨“ u (0) u (2) ”⟩) \in {Base}_{SymGrp (D)}$
80	5 4 34 39 73 17	cycpm2cl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (⟨“ u (0) u (1) ”⟩) \in {Base}_{SymGrp (D)}$
81		eqid	$⊢ {Base}_{SymGrp (D)} = {Base}_{SymGrp (D)}$
82	17 81 77	symgov	$⊢ (toCyc (D) (⟨“ u (0) u (2) ”⟩) \in {Base}_{SymGrp (D)} \land toCyc (D) (⟨“ u (0) u (1) ”⟩) \in {Base}_{SymGrp (D)}) \to toCyc (D) (⟨“ u (0) u (2) ”⟩) +_{SymGrp (D)} toCyc (D) (⟨“ u (0) u (1) ”⟩) = toCyc (D) (⟨“ u (0) u (2) ”⟩) \circ toCyc (D) (⟨“ u (0) u (1) ”⟩)$
83	79 80 82	syl2anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (⟨“ u (0) u (2) ”⟩) +_{SymGrp (D)} toCyc (D) (⟨“ u (0) u (1) ”⟩) = toCyc (D) (⟨“ u (0) u (2) ”⟩) \circ toCyc (D) (⟨“ u (0) u (1) ”⟩)$
84	54 78 83	3eqtrd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (u) = toCyc (D) (⟨“ u (0) u (2) ”⟩) \circ toCyc (D) (⟨“ u (0) u (1) ”⟩)$
85	84	fveq2d	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to pmSgn (D) (toCyc (D) (u)) = pmSgn (D) (toCyc (D) (⟨“ u (0) u (2) ”⟩) \circ toCyc (D) (⟨“ u (0) u (1) ”⟩))$
86		eqid	$⊢ pmSgn (D) = pmSgn (D)$
87	17 86 81	psgnco	$⊢ (D \in Fin \land toCyc (D) (⟨“ u (0) u (2) ”⟩) \in {Base}_{SymGrp (D)} \land toCyc (D) (⟨“ u (0) u (1) ”⟩) \in {Base}_{SymGrp (D)}) \to pmSgn (D) (toCyc (D) (⟨“ u (0) u (2) ”⟩) \circ toCyc (D) (⟨“ u (0) u (1) ”⟩)) = pmSgn (D) (toCyc (D) (⟨“ u (0) u (2) ”⟩)) pmSgn (D) (toCyc (D) (⟨“ u (0) u (1) ”⟩))$
88	4 79 80 87	syl3anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to pmSgn (D) (toCyc (D) (⟨“ u (0) u (2) ”⟩) \circ toCyc (D) (⟨“ u (0) u (1) ”⟩)) = pmSgn (D) (toCyc (D) (⟨“ u (0) u (2) ”⟩)) pmSgn (D) (toCyc (D) (⟨“ u (0) u (1) ”⟩))$
89		eqid	$⊢ pmTrsp (D) = pmTrsp (D)$
90	5 4 34 45 75 89	cycpm2tr	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (⟨“ u (0) u (2) ”⟩) = pmTrsp (D) (\{u (0), u (2)\})$
91	34 45	prssd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to \{u (0), u (2)\} \subseteq D$
92		enpr2	$⊢ (u (0) \in D \land u (2) \in D \land u (0) \neq u (2)) \to \{u (0), u (2)\} \approx 2_{𝑜}$
93	34 45 75 92	syl3anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to \{u (0), u (2)\} \approx 2_{𝑜}$
94		eqid	$⊢ ran pmTrsp (D) = ran pmTrsp (D)$
95	89 94	pmtrrn	$⊢ (D \in Fin \land \{u (0), u (2)\} \subseteq D \land \{u (0), u (2)\} \approx 2_{𝑜}) \to pmTrsp (D) (\{u (0), u (2)\}) \in ran pmTrsp (D)$
96	4 91 93 95	syl3anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to pmTrsp (D) (\{u (0), u (2)\}) \in ran pmTrsp (D)$
97	90 96	eqeltrd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (⟨“ u (0) u (2) ”⟩) \in ran pmTrsp (D)$
98	17 94 86	psgnpmtr	$⊢ toCyc (D) (⟨“ u (0) u (2) ”⟩) \in ran pmTrsp (D) \to pmSgn (D) (toCyc (D) (⟨“ u (0) u (2) ”⟩)) = - 1$
99	97 98	syl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to pmSgn (D) (toCyc (D) (⟨“ u (0) u (2) ”⟩)) = - 1$
100	5 4 34 39 73 89	cycpm2tr	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (⟨“ u (0) u (1) ”⟩) = pmTrsp (D) (\{u (0), u (1)\})$
101	34 39	prssd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to \{u (0), u (1)\} \subseteq D$
102		enpr2	$⊢ (u (0) \in D \land u (1) \in D \land u (0) \neq u (1)) \to \{u (0), u (1)\} \approx 2_{𝑜}$
103	34 39 73 102	syl3anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to \{u (0), u (1)\} \approx 2_{𝑜}$
104	89 94	pmtrrn	$⊢ (D \in Fin \land \{u (0), u (1)\} \subseteq D \land \{u (0), u (1)\} \approx 2_{𝑜}) \to pmTrsp (D) (\{u (0), u (1)\}) \in ran pmTrsp (D)$
105	4 101 103 104	syl3anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to pmTrsp (D) (\{u (0), u (1)\}) \in ran pmTrsp (D)$
106	100 105	eqeltrd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (⟨“ u (0) u (1) ”⟩) \in ran pmTrsp (D)$
107	17 94 86	psgnpmtr	$⊢ toCyc (D) (⟨“ u (0) u (1) ”⟩) \in ran pmTrsp (D) \to pmSgn (D) (toCyc (D) (⟨“ u (0) u (1) ”⟩)) = - 1$
108	106 107	syl	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to pmSgn (D) (toCyc (D) (⟨“ u (0) u (1) ”⟩)) = - 1$
109	99 108	oveq12d	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to pmSgn (D) (toCyc (D) (⟨“ u (0) u (2) ”⟩)) pmSgn (D) (toCyc (D) (⟨“ u (0) u (1) ”⟩)) = -1 -1$
110		neg1mulneg1e1	$⊢ -1 -1 = 1$
111	109 110	eqtrdi	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to pmSgn (D) (toCyc (D) (⟨“ u (0) u (2) ”⟩)) pmSgn (D) (toCyc (D) (⟨“ u (0) u (1) ”⟩)) = 1$
112	85 88 111	3eqtrd	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to pmSgn (D) (toCyc (D) (u)) = 1$
113	17 81 86	psgnevpmb	$⊢ D \in Fin \to (toCyc (D) (u) \in pmEven (D) \leftrightarrow (toCyc (D) (u) \in {Base}_{SymGrp (D)} \land pmSgn (D) (toCyc (D) (u)) = 1))$
114	113	biimpar	$⊢ (D \in Fin \land (toCyc (D) (u) \in {Base}_{SymGrp (D)} \land pmSgn (D) (toCyc (D) (u)) = 1)) \to toCyc (D) (u) \in pmEven (D)$
115	4 18 112 114	syl12anc	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (u) \in pmEven (D)$
116	115 2	eleqtrrdi	$⊢ (D \in Fin \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \to toCyc (D) (u) \in A$
117	116	ad4ant13	$⊢ (((D \in Fin \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land toCyc (D) (u) = p) \to toCyc (D) (u) \in A$
118	3 117	eqeltrrd	$⊢ (((D \in Fin \land p \in C) \land u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}])) \land toCyc (D) (u) = p) \to p \in A$
119		nfcv	$⊢ \underline{Ⅎ} u toCyc (D)$
120	5 17 81	tocycf	$⊢ D \in Fin \to toCyc (D) : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{SymGrp (D)}$
121	120	ffnd	$⊢ D \in Fin \to toCyc (D) Fn \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
122	121	adantr	$⊢ (D \in Fin \land p \in C) \to toCyc (D) Fn \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
123		simpr	$⊢ (D \in Fin \land p \in C) \to p \in C$
124	123 1	eleqtrdi	$⊢ (D \in Fin \land p \in C) \to p \in toCyc (D) [{\|.\|}^{-1} [\{3\}]]$
125	119 122 124	fvelimad	$⊢ (D \in Fin \land p \in C) \to \exists u \in (\{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \cap {\|.\|}^{-1} [\{3\}]) toCyc (D) (u) = p$
126	118 125	r19.29a	$⊢ (D \in Fin \land p \in C) \to p \in A$
127	126	ex	$⊢ D \in Fin \to (p \in C \to p \in A)$
128	127	ssrdv	$⊢ D \in Fin \to C \subseteq A$

Metamath Proof Explorer

Theorem cyc3evpm

Proof