Metamath Proof Explorer

Theorem cyc3evpm

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

Ref Expression
Hypotheses cyc3evpm.t ⊢ 𝐶 = ( ( toCyc ‘ 𝐷 ) “ ( ◡ ♯ “ { 3 } ) )
cyc3evpm.a ⊢ 𝐴 = ( pmEven ‘ 𝐷 )
Assertion cyc3evpm ( 𝐷 ∈ Fin → 𝐶 ⊆ 𝐴 )

Proof

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