| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . 5
⊢ ((((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧
((toCyc‘𝐷)‘𝑢) = 𝑝) → ((toCyc‘𝐷)‘𝑢) = 𝑝) | 
| 2 |  | simpl 482 | . . . . . . . 8
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 𝐷 ∈ Fin) | 
| 3 |  | eqid 2737 | . . . . . . . . 9
⊢
(toCyc‘𝐷) =
(toCyc‘𝐷) | 
| 4 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) | 
| 5 | 4 | elin1d 4204 | . . . . . . . . . 10
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 6 |  | elrabi 3687 | . . . . . . . . . 10
⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} → 𝑢 ∈ Word 𝐷) | 
| 7 | 5, 6 | syl 17 | . . . . . . . . 9
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 𝑢 ∈ Word 𝐷) | 
| 8 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢) | 
| 9 |  | dmeq 5914 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢) | 
| 10 |  | eqidd 2738 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷) | 
| 11 | 8, 9, 10 | f1eq123d 6840 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷)) | 
| 12 | 11 | elrab 3692 | . . . . . . . . . . 11
⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷)) | 
| 13 | 12 | simprbi 496 | . . . . . . . . . 10
⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} → 𝑢:dom 𝑢–1-1→𝐷) | 
| 14 | 5, 13 | syl 17 | . . . . . . . . 9
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 𝑢:dom 𝑢–1-1→𝐷) | 
| 15 |  | eqid 2737 | . . . . . . . . 9
⊢
(SymGrp‘𝐷) =
(SymGrp‘𝐷) | 
| 16 | 3, 2, 7, 14, 15 | cycpmcl 33136 | . . . . . . . 8
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘𝑢) ∈ (Base‘(SymGrp‘𝐷))) | 
| 17 |  | c0ex 11255 | . . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
V | 
| 18 | 17 | tpid1 4768 | . . . . . . . . . . . . . . . . 17
⊢ 0 ∈
{0, 1, 2} | 
| 19 |  | fzo0to3tp 13791 | . . . . . . . . . . . . . . . . 17
⊢ (0..^3) =
{0, 1, 2} | 
| 20 | 18, 19 | eleqtrri 2840 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
(0..^3) | 
| 21 | 4 | elin2d 4205 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 𝑢 ∈ (◡♯ “ {3})) | 
| 22 |  | hashf 14377 | . . . . . . . . . . . . . . . . . . . 20
⊢
♯:V⟶(ℕ0 ∪ {+∞}) | 
| 23 |  | ffn 6736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(♯:V⟶(ℕ0 ∪ {+∞}) → ♯
Fn V) | 
| 24 |  | elpreima 7078 | . . . . . . . . . . . . . . . . . . . 20
⊢ (♯
Fn V → (𝑢 ∈
(◡♯ “ {3}) ↔ (𝑢 ∈ V ∧
(♯‘𝑢) ∈
{3}))) | 
| 25 | 22, 23, 24 | mp2b 10 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ (◡♯ “ {3}) ↔ (𝑢 ∈ V ∧
(♯‘𝑢) ∈
{3})) | 
| 26 | 25 | simprbi 496 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (◡♯ “ {3}) →
(♯‘𝑢) ∈
{3}) | 
| 27 |  | elsni 4643 | . . . . . . . . . . . . . . . . . 18
⊢
((♯‘𝑢)
∈ {3} → (♯‘𝑢) = 3) | 
| 28 | 21, 26, 27 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
(♯‘𝑢) =
3) | 
| 29 | 28 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
(0..^(♯‘𝑢)) =
(0..^3)) | 
| 30 | 20, 29 | eleqtrrid 2848 | . . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 0 ∈
(0..^(♯‘𝑢))) | 
| 31 |  | wrdsymbcl 14565 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘𝑢))) → (𝑢‘0) ∈ 𝐷) | 
| 32 | 7, 30, 31 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘0) ∈ 𝐷) | 
| 33 |  | 1ex 11257 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
V | 
| 34 | 33 | tpid2 4770 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
{0, 1, 2} | 
| 35 | 34, 19 | eleqtrri 2840 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
(0..^3) | 
| 36 | 35, 29 | eleqtrrid 2848 | . . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 1 ∈
(0..^(♯‘𝑢))) | 
| 37 |  | wrdsymbcl 14565 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Word 𝐷 ∧ 1 ∈ (0..^(♯‘𝑢))) → (𝑢‘1) ∈ 𝐷) | 
| 38 | 7, 36, 37 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘1) ∈ 𝐷) | 
| 39 |  | 2ex 12343 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
V | 
| 40 | 39 | tpid3 4773 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
{0, 1, 2} | 
| 41 | 40, 19 | eleqtrri 2840 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
(0..^3) | 
| 42 | 41, 29 | eleqtrrid 2848 | . . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 2 ∈
(0..^(♯‘𝑢))) | 
| 43 |  | wrdsymbcl 14565 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ Word 𝐷 ∧ 2 ∈ (0..^(♯‘𝑢))) → (𝑢‘2) ∈ 𝐷) | 
| 44 | 7, 42, 43 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘2) ∈ 𝐷) | 
| 45 | 32, 38, 44 | 3jca 1129 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → ((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘1) ∈ 𝐷 ∧ (𝑢‘2) ∈ 𝐷)) | 
| 46 |  | eqidd 2738 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘0) = (𝑢‘0)) | 
| 47 |  | eqidd 2738 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘1) = (𝑢‘1)) | 
| 48 |  | eqidd 2738 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘2) = (𝑢‘2)) | 
| 49 | 46, 47, 48 | 3jca 1129 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → ((𝑢‘0) = (𝑢‘0) ∧ (𝑢‘1) = (𝑢‘1) ∧ (𝑢‘2) = (𝑢‘2))) | 
| 50 |  | eqwrds3 15000 | . . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ Word 𝐷 ∧ ((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘1) ∈ 𝐷 ∧ (𝑢‘2) ∈ 𝐷)) → (𝑢 = 〈“(𝑢‘0)(𝑢‘1)(𝑢‘2)”〉 ↔
((♯‘𝑢) = 3
∧ ((𝑢‘0) = (𝑢‘0) ∧ (𝑢‘1) = (𝑢‘1) ∧ (𝑢‘2) = (𝑢‘2))))) | 
| 51 | 50 | biimpar 477 | . . . . . . . . . . . . 13
⊢ (((𝑢 ∈ Word 𝐷 ∧ ((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘1) ∈ 𝐷 ∧ (𝑢‘2) ∈ 𝐷)) ∧ ((♯‘𝑢) = 3 ∧ ((𝑢‘0) = (𝑢‘0) ∧ (𝑢‘1) = (𝑢‘1) ∧ (𝑢‘2) = (𝑢‘2)))) → 𝑢 = 〈“(𝑢‘0)(𝑢‘1)(𝑢‘2)”〉) | 
| 52 | 7, 45, 28, 49, 51 | syl22anc 839 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 𝑢 = 〈“(𝑢‘0)(𝑢‘1)(𝑢‘2)”〉) | 
| 53 | 52 | fveq2d 6910 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘𝑢) = ((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)(𝑢‘2)”〉)) | 
| 54 |  | wrddm 14559 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢))) | 
| 55 | 7, 54 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → dom 𝑢 = (0..^(♯‘𝑢))) | 
| 56 | 55, 29 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → dom 𝑢 = (0..^3)) | 
| 57 | 56, 19 | eqtrdi 2793 | . . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → dom 𝑢 = {0, 1, 2}) | 
| 58 |  | f1eq2 6800 | . . . . . . . . . . . . . . . 16
⊢ (dom
𝑢 = {0, 1, 2} → (𝑢:dom 𝑢–1-1→𝐷 ↔ 𝑢:{0, 1, 2}–1-1→𝐷)) | 
| 59 | 58 | biimpa 476 | . . . . . . . . . . . . . . 15
⊢ ((dom
𝑢 = {0, 1, 2} ∧ 𝑢:dom 𝑢–1-1→𝐷) → 𝑢:{0, 1, 2}–1-1→𝐷) | 
| 60 | 57, 14, 59 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → 𝑢:{0, 1, 2}–1-1→𝐷) | 
| 61 | 17, 33, 39 | 3pm3.2i 1340 | . . . . . . . . . . . . . . . 16
⊢ (0 ∈
V ∧ 1 ∈ V ∧ 2 ∈ V) | 
| 62 |  | 0ne1 12337 | . . . . . . . . . . . . . . . . 17
⊢ 0 ≠
1 | 
| 63 |  | 0ne2 12473 | . . . . . . . . . . . . . . . . 17
⊢ 0 ≠
2 | 
| 64 |  | 1ne2 12474 | . . . . . . . . . . . . . . . . 17
⊢ 1 ≠
2 | 
| 65 | 62, 63, 64 | 3pm3.2i 1340 | . . . . . . . . . . . . . . . 16
⊢ (0 ≠ 1
∧ 0 ≠ 2 ∧ 1 ≠ 2) | 
| 66 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢ {0, 1, 2}
= {0, 1, 2} | 
| 67 | 66 | f13dfv 7294 | . . . . . . . . . . . . . . . 16
⊢ (((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))))) | 
| 68 | 61, 65, 67 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢ (𝑢:{0, 1, 2}–1-1→𝐷 ↔ (𝑢:{0, 1, 2}⟶𝐷 ∧ ((𝑢‘0) ≠ (𝑢‘1) ∧ (𝑢‘0) ≠ (𝑢‘2) ∧ (𝑢‘1) ≠ (𝑢‘2)))) | 
| 69 | 68 | simprbi 496 | . . . . . . . . . . . . . 14
⊢ (𝑢:{0, 1, 2}–1-1→𝐷 → ((𝑢‘0) ≠ (𝑢‘1) ∧ (𝑢‘0) ≠ (𝑢‘2) ∧ (𝑢‘1) ≠ (𝑢‘2))) | 
| 70 | 60, 69 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → ((𝑢‘0) ≠ (𝑢‘1) ∧ (𝑢‘0) ≠ (𝑢‘2) ∧ (𝑢‘1) ≠ (𝑢‘2))) | 
| 71 | 70 | simp1d 1143 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘0) ≠ (𝑢‘1)) | 
| 72 | 70 | simp3d 1145 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘1) ≠ (𝑢‘2)) | 
| 73 | 70 | simp2d 1144 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘0) ≠ (𝑢‘2)) | 
| 74 | 73 | necomd 2996 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → (𝑢‘2) ≠ (𝑢‘0)) | 
| 75 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(+g‘(SymGrp‘𝐷)) =
(+g‘(SymGrp‘𝐷)) | 
| 76 | 3, 15, 2, 32, 38, 44, 71, 72, 74, 75 | cyc3co2 33160 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)(𝑢‘2)”〉) =
(((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉)(+g‘(SymGrp‘𝐷))((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉))) | 
| 77 | 3, 2, 32, 44, 73, 15 | cycpm2cl 33140 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) ∈
(Base‘(SymGrp‘𝐷))) | 
| 78 | 3, 2, 32, 38, 71, 15 | cycpm2cl 33140 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉) ∈
(Base‘(SymGrp‘𝐷))) | 
| 79 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(Base‘(SymGrp‘𝐷)) = (Base‘(SymGrp‘𝐷)) | 
| 80 | 15, 79, 75 | symgov 19401 | . . . . . . . . . . . 12
⊢
((((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) ∈
(Base‘(SymGrp‘𝐷)) ∧ ((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉) ∈
(Base‘(SymGrp‘𝐷))) → (((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉)(+g‘(SymGrp‘𝐷))((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉)) = (((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) ∘ ((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉))) | 
| 81 | 77, 78, 80 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
(((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉)(+g‘(SymGrp‘𝐷))((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉)) = (((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) ∘ ((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉))) | 
| 82 | 53, 76, 81 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘𝑢) = (((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) ∘
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉))) | 
| 83 | 82 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((pmSgn‘𝐷)‘((toCyc‘𝐷)‘𝑢)) = ((pmSgn‘𝐷)‘(((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) ∘
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉)))) | 
| 84 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(pmSgn‘𝐷) =
(pmSgn‘𝐷) | 
| 85 | 15, 84, 79 | psgnco 21601 | . . . . . . . . . 10
⊢ ((𝐷 ∈ 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)”〉)))) | 
| 86 | 2, 77, 78, 85 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((pmSgn‘𝐷)‘(((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) ∘
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉))) =
(((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉)) ·
((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉)))) | 
| 87 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(pmTrsp‘𝐷) =
(pmTrsp‘𝐷) | 
| 88 | 3, 2, 32, 44, 73, 87 | cycpm2tr 33139 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) =
((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘2)})) | 
| 89 | 32, 44 | prssd 4822 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → {(𝑢‘0), (𝑢‘2)} ⊆ 𝐷) | 
| 90 |  | enpr2 10042 | . . . . . . . . . . . . . . 15
⊢ (((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘2) ∈ 𝐷 ∧ (𝑢‘0) ≠ (𝑢‘2)) → {(𝑢‘0), (𝑢‘2)} ≈
2o) | 
| 91 | 32, 44, 73, 90 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → {(𝑢‘0), (𝑢‘2)} ≈
2o) | 
| 92 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢ ran
(pmTrsp‘𝐷) = ran
(pmTrsp‘𝐷) | 
| 93 | 87, 92 | pmtrrn 19475 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ {(𝑢‘0), (𝑢‘2)} ⊆ 𝐷 ∧ {(𝑢‘0), (𝑢‘2)} ≈ 2o) →
((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘2)}) ∈ ran (pmTrsp‘𝐷)) | 
| 94 | 2, 89, 91, 93 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘2)}) ∈ ran (pmTrsp‘𝐷)) | 
| 95 | 88, 94 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) ∈ ran
(pmTrsp‘𝐷)) | 
| 96 | 15, 92, 84 | psgnpmtr 19528 | . . . . . . . . . . . 12
⊢
(((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉) ∈ ran
(pmTrsp‘𝐷) →
((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉)) =
-1) | 
| 97 | 95, 96 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉)) =
-1) | 
| 98 | 3, 2, 32, 38, 71, 87 | cycpm2tr 33139 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉) =
((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘1)})) | 
| 99 | 32, 38 | prssd 4822 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → {(𝑢‘0), (𝑢‘1)} ⊆ 𝐷) | 
| 100 |  | enpr2 10042 | . . . . . . . . . . . . . . 15
⊢ (((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘1) ∈ 𝐷 ∧ (𝑢‘0) ≠ (𝑢‘1)) → {(𝑢‘0), (𝑢‘1)} ≈
2o) | 
| 101 | 32, 38, 71, 100 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) → {(𝑢‘0), (𝑢‘1)} ≈
2o) | 
| 102 | 87, 92 | pmtrrn 19475 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ {(𝑢‘0), (𝑢‘1)} ⊆ 𝐷 ∧ {(𝑢‘0), (𝑢‘1)} ≈ 2o) →
((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘1)}) ∈ ran (pmTrsp‘𝐷)) | 
| 103 | 2, 99, 101, 102 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘1)}) ∈ ran (pmTrsp‘𝐷)) | 
| 104 | 98, 103 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉) ∈ ran
(pmTrsp‘𝐷)) | 
| 105 | 15, 92, 84 | psgnpmtr 19528 | . . . . . . . . . . . 12
⊢
(((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉) ∈ ran
(pmTrsp‘𝐷) →
((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉)) =
-1) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉)) =
-1) | 
| 107 | 97, 106 | oveq12d 7449 | . . . . . . . . . 10
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
(((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉)) ·
((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉))) = (-1 ·
-1)) | 
| 108 |  | neg1mulneg1e1 12479 | . . . . . . . . . 10
⊢ (-1
· -1) = 1 | 
| 109 | 107, 108 | eqtrdi 2793 | . . . . . . . . 9
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
(((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘2)”〉)) ·
((pmSgn‘𝐷)‘((toCyc‘𝐷)‘〈“(𝑢‘0)(𝑢‘1)”〉))) =
1) | 
| 110 | 83, 86, 109 | 3eqtrd 2781 | . . . . . . . 8
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((pmSgn‘𝐷)‘((toCyc‘𝐷)‘𝑢)) = 1) | 
| 111 | 15, 79, 84 | psgnevpmb 21605 | . . . . . . . . 9
⊢ (𝐷 ∈ Fin →
(((toCyc‘𝐷)‘𝑢) ∈ (pmEven‘𝐷) ↔ (((toCyc‘𝐷)‘𝑢) ∈ (Base‘(SymGrp‘𝐷)) ∧ ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘𝑢)) = 1))) | 
| 112 | 111 | biimpar 477 | . . . . . . . 8
⊢ ((𝐷 ∈ Fin ∧
(((toCyc‘𝐷)‘𝑢) ∈ (Base‘(SymGrp‘𝐷)) ∧ ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘𝑢)) = 1)) → ((toCyc‘𝐷)‘𝑢) ∈ (pmEven‘𝐷)) | 
| 113 | 2, 16, 110, 112 | syl12anc 837 | . . . . . . 7
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘𝑢) ∈ (pmEven‘𝐷)) | 
| 114 |  | cyc3evpm.a | . . . . . . 7
⊢ 𝐴 = (pmEven‘𝐷) | 
| 115 | 113, 114 | eleqtrrdi 2852 | . . . . . 6
⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) →
((toCyc‘𝐷)‘𝑢) ∈ 𝐴) | 
| 116 | 115 | ad4ant13 751 | . . . . 5
⊢ ((((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧
((toCyc‘𝐷)‘𝑢) = 𝑝) → ((toCyc‘𝐷)‘𝑢) ∈ 𝐴) | 
| 117 | 1, 116 | eqeltrrd 2842 | . . . 4
⊢ ((((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧
((toCyc‘𝐷)‘𝑢) = 𝑝) → 𝑝 ∈ 𝐴) | 
| 118 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑢(toCyc‘𝐷) | 
| 119 | 3, 15, 79 | tocycf 33137 | . . . . . . 7
⊢ (𝐷 ∈ Fin →
(toCyc‘𝐷):{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘(SymGrp‘𝐷))) | 
| 120 | 119 | ffnd 6737 | . . . . . 6
⊢ (𝐷 ∈ Fin →
(toCyc‘𝐷) Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 121 | 120 | adantr 480 | . . . . 5
⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → (toCyc‘𝐷) Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 122 |  | simpr 484 | . . . . . 6
⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → 𝑝 ∈ 𝐶) | 
| 123 |  | cyc3evpm.t | . . . . . 6
⊢ 𝐶 = ((toCyc‘𝐷) “ (◡♯ “ {3})) | 
| 124 | 122, 123 | eleqtrdi 2851 | . . . . 5
⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → 𝑝 ∈ ((toCyc‘𝐷) “ (◡♯ “ {3}))) | 
| 125 | 118, 121,
124 | fvelimad 6976 | . . . 4
⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))((toCyc‘𝐷)‘𝑢) = 𝑝) | 
| 126 | 117, 125 | r19.29a 3162 | . . 3
⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → 𝑝 ∈ 𝐴) | 
| 127 | 126 | ex 412 | . 2
⊢ (𝐷 ∈ Fin → (𝑝 ∈ 𝐶 → 𝑝 ∈ 𝐴)) | 
| 128 | 127 | ssrdv 3989 | 1
⊢ (𝐷 ∈ Fin → 𝐶 ⊆ 𝐴) |