| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . 4
⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → 𝑔 ∈ 𝐴) | 
| 2 |  | simpr 484 | . . . . . . 7
⊢
(((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → 𝑝 = 𝑔) | 
| 3 | 2 | oveq1d 7447 | . . . . . 6
⊢
(((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑝 + 𝑇) = (𝑔 + 𝑇)) | 
| 4 | 3, 2 | oveq12d 7450 | . . . . 5
⊢
(((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → ((𝑝 + 𝑇) − 𝑝) = ((𝑔 + 𝑇) − 𝑔)) | 
| 5 | 4 | eqeq2d 2747 | . . . 4
⊢
(((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) ∧ 𝑝 = 𝑔) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = ((𝑔 + 𝑇) − 𝑔))) | 
| 6 |  | simplr 768 | . . . 4
⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → 𝑄 = ((𝑔 + 𝑇) − 𝑔)) | 
| 7 | 1, 5, 6 | rspcedvd 3623 | . . 3
⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ 𝑔 ∈ 𝐴) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝)) | 
| 8 |  | cyc3conja.d | . . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ Fin) | 
| 9 | 8 | ad5antr 734 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝐷 ∈ Fin) | 
| 10 | 9 | ad3antrrr 730 | . . . . . . 7
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝐷 ∈ Fin) | 
| 11 |  | simp-8r 791 | . . . . . . . 8
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑔 ∈ (Base‘𝑆)) | 
| 12 |  | simp-6r 787 | . . . . . . . 8
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ¬ 𝑔 ∈ 𝐴) | 
| 13 | 11, 12 | eldifd 3961 | . . . . . . 7
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴)) | 
| 14 |  | simpllr 775 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ (𝐷 ∖ ran 𝑢)) | 
| 15 | 14 | eldifad 3962 | . . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ∈ 𝐷) | 
| 16 |  | simplr 768 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ (𝐷 ∖ ran 𝑢)) | 
| 17 | 16 | eldifad 3962 | . . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑦 ∈ 𝐷) | 
| 18 | 15, 17 | prssd 4821 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ 𝐷) | 
| 19 |  | simpr 484 | . . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑥 ≠ 𝑦) | 
| 20 |  | enpr2 10043 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2o) | 
| 21 | 14, 16, 19, 20 | syl3anc 1372 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ≈ 2o) | 
| 22 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(pmTrsp‘𝐷) =
(pmTrsp‘𝐷) | 
| 23 |  | eqid 2736 | . . . . . . . . . . 11
⊢ ran
(pmTrsp‘𝐷) = ran
(pmTrsp‘𝐷) | 
| 24 | 22, 23 | pmtrrn 19476 | . . . . . . . . . 10
⊢ ((𝐷 ∈ Fin ∧ {𝑥, 𝑦} ⊆ 𝐷 ∧ {𝑥, 𝑦} ≈ 2o) →
((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷)) | 
| 25 | 10, 18, 21, 24 | syl3anc 1372 | . . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷)) | 
| 26 |  | cyc3conja.s | . . . . . . . . . 10
⊢ 𝑆 = (SymGrp‘𝐷) | 
| 27 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 28 | 26, 27, 23 | pmtrodpm 21616 | . . . . . . . . 9
⊢ ((𝐷 ∈ Fin ∧
((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ran (pmTrsp‘𝐷)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷))) | 
| 29 | 10, 25, 28 | syl2anc 584 | . . . . . . . 8
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ (pmEven‘𝐷))) | 
| 30 |  | cyc3conja.a | . . . . . . . . 9
⊢ 𝐴 = (pmEven‘𝐷) | 
| 31 | 30 | difeq2i 4122 | . . . . . . . 8
⊢
((Base‘𝑆)
∖ 𝐴) =
((Base‘𝑆) ∖
(pmEven‘𝐷)) | 
| 32 | 29, 31 | eleqtrrdi 2851 | . . . . . . 7
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴)) | 
| 33 | 26, 27, 30 | odpmco 33107 | . . . . . . 7
⊢ ((𝐷 ∈ Fin ∧ 𝑔 ∈ ((Base‘𝑆) ∖ 𝐴) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ ((Base‘𝑆) ∖ 𝐴)) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴) | 
| 34 | 10, 13, 32, 33 | syl3anc 1372 | . . . . . 6
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ 𝐴) | 
| 35 |  | simpr 484 | . . . . . . . . 9
⊢
((((((((((𝜑 ∧
𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) | 
| 36 | 35 | oveq1d 7447 | . . . . . . . 8
⊢
((((((((((𝜑 ∧
𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑝 + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇)) | 
| 37 | 36, 35 | oveq12d 7450 | . . . . . . 7
⊢
((((((((((𝜑 ∧
𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → ((𝑝 + 𝑇) − 𝑝) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))) | 
| 38 | 37 | eqeq2d 2747 | . . . . . 6
⊢
((((((((((𝜑 ∧
𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) ∧ 𝑝 = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) → (𝑄 = ((𝑝 + 𝑇) − 𝑝) ↔ 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))))) | 
| 39 | 29 | eldifad 3962 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) | 
| 40 |  | 0zd 12627 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ∈
ℤ) | 
| 41 |  | cyc3conja.n | . . . . . . . . . . . . . . . . . 18
⊢ 𝑁 = (♯‘𝐷) | 
| 42 |  | hashcl 14396 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 ∈ Fin →
(♯‘𝐷) ∈
ℕ0) | 
| 43 | 8, 42 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (♯‘𝐷) ∈
ℕ0) | 
| 44 | 41, 43 | eqeltrid 2844 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 45 | 44 | nn0zd 12641 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 46 |  | 3z 12652 | . . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℤ | 
| 47 | 46 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 3 ∈
ℤ) | 
| 48 |  | 0red 11265 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ∈
ℝ) | 
| 49 | 47 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 3 ∈
ℝ) | 
| 50 |  | 3pos 12372 | . . . . . . . . . . . . . . . . . 18
⊢ 0 <
3 | 
| 51 | 50 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < 3) | 
| 52 | 48, 49, 51 | ltled 11410 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 3) | 
| 53 |  | 5re 12354 | . . . . . . . . . . . . . . . . . 18
⊢ 5 ∈
ℝ | 
| 54 | 53 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 5 ∈
ℝ) | 
| 55 | 44 | nn0red 12590 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 56 |  | 3lt5 12445 | . . . . . . . . . . . . . . . . . . 19
⊢ 3 <
5 | 
| 57 | 56 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 3 < 5) | 
| 58 | 49, 54, 57 | ltled 11410 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 3 ≤ 5) | 
| 59 |  | cyc3conja.1 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 5 ≤ 𝑁) | 
| 60 | 49, 54, 55, 58, 59 | letrd 11419 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 3 ≤ 𝑁) | 
| 61 | 40, 45, 47, 52, 60 | elfzd 13556 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 3 ∈ (0...𝑁)) | 
| 62 |  | cyc3conja.c | . . . . . . . . . . . . . . . 16
⊢ 𝐶 = (𝑀 “ (◡♯ “ {3})) | 
| 63 |  | cyc3conja.m | . . . . . . . . . . . . . . . 16
⊢ 𝑀 = (toCyc‘𝐷) | 
| 64 | 62, 26, 41, 63, 27 | cycpmgcl 33174 | . . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ Fin ∧ 3 ∈
(0...𝑁)) → 𝐶 ⊆ (Base‘𝑆)) | 
| 65 | 8, 61, 64 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ⊆ (Base‘𝑆)) | 
| 66 |  | cyc3conja.t | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ 𝐶) | 
| 67 | 65, 66 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ (Base‘𝑆)) | 
| 68 | 67 | ad8antr 740 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑇 ∈ (Base‘𝑆)) | 
| 69 | 63, 10, 15, 17, 19, 22 | cycpm2tr 33140 | . . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑀‘〈“𝑥𝑦”〉) = ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) | 
| 70 | 69 | reseq1d 5995 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘〈“𝑥𝑦”〉) ↾ ran 𝑢) = (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢)) | 
| 71 | 15, 17 | s2cld 14911 | . . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 〈“𝑥𝑦”〉 ∈ Word 𝐷) | 
| 72 | 15, 17, 19 | s2f1 32930 | . . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 〈“𝑥𝑦”〉:dom 〈“𝑥𝑦”〉–1-1→𝐷) | 
| 73 | 63, 10, 71, 72 | tocycfvres2 33132 | . . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘〈“𝑥𝑦”〉) ↾ (𝐷 ∖ ran 〈“𝑥𝑦”〉)) = ( I ↾ (𝐷 ∖ ran 〈“𝑥𝑦”〉))) | 
| 74 | 73 | reseq1d 5995 | . . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑀‘〈“𝑥𝑦”〉) ↾ (𝐷 ∖ ran 〈“𝑥𝑦”〉)) ↾ ran 𝑢) = (( I ↾ (𝐷 ∖ ran 〈“𝑥𝑦”〉)) ↾ ran 𝑢)) | 
| 75 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) | 
| 76 | 75 | elin1d 4203 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 77 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢) | 
| 78 |  | dmeq 5913 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢) | 
| 79 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷) | 
| 80 | 77, 78, 79 | f1eq123d 6839 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷)) | 
| 81 | 80 | elrab 3691 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷)) | 
| 82 | 76, 81 | sylib 218 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷)) | 
| 83 | 82 | simprd 495 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢:dom 𝑢–1-1→𝐷) | 
| 84 |  | f1f 6803 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢:dom 𝑢–1-1→𝐷 → 𝑢:dom 𝑢⟶𝐷) | 
| 85 |  | frn 6742 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢:dom 𝑢⟶𝐷 → ran 𝑢 ⊆ 𝐷) | 
| 86 | 83, 84, 85 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ran 𝑢 ⊆ 𝐷) | 
| 87 | 86 | ad3antrrr 730 | . . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ 𝐷) | 
| 88 | 14, 16 | prssd 4821 | . . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢)) | 
| 89 |  | ssconb 4141 | . . . . . . . . . . . . . . . . . 18
⊢ (({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷) → ({𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢) ↔ ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦}))) | 
| 90 | 89 | biimpa 476 | . . . . . . . . . . . . . . . . 17
⊢ ((({𝑥, 𝑦} ⊆ 𝐷 ∧ ran 𝑢 ⊆ 𝐷) ∧ {𝑥, 𝑦} ⊆ (𝐷 ∖ ran 𝑢)) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦})) | 
| 91 | 18, 87, 88, 90 | syl21anc 837 | . . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ (𝐷 ∖ {𝑥, 𝑦})) | 
| 92 | 14, 16 | s2rn 15003 | . . . . . . . . . . . . . . . . 17
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 〈“𝑥𝑦”〉 = {𝑥, 𝑦}) | 
| 93 | 92 | difeq2d 4125 | . . . . . . . . . . . . . . . 16
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝐷 ∖ ran 〈“𝑥𝑦”〉) = (𝐷 ∖ {𝑥, 𝑦})) | 
| 94 | 91, 93 | sseqtrrd 4020 | . . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ran 𝑢 ⊆ (𝐷 ∖ ran 〈“𝑥𝑦”〉)) | 
| 95 | 94 | resabs1d 6025 | . . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑀‘〈“𝑥𝑦”〉) ↾ (𝐷 ∖ ran 〈“𝑥𝑦”〉)) ↾ ran 𝑢) = ((𝑀‘〈“𝑥𝑦”〉) ↾ ran 𝑢)) | 
| 96 | 94 | resabs1d 6025 | . . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (( I ↾ (𝐷 ∖ ran 〈“𝑥𝑦”〉)) ↾ ran 𝑢) = ( I ↾ ran 𝑢)) | 
| 97 | 74, 95, 96 | 3eqtr3d 2784 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘〈“𝑥𝑦”〉) ↾ ran 𝑢) = ( I ↾ ran 𝑢)) | 
| 98 | 70, 97 | eqtr3d 2778 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ↾ ran 𝑢) = ( I ↾ ran 𝑢)) | 
| 99 |  | simp-4r 783 | . . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑀‘𝑢) = 𝑇) | 
| 100 | 99 | reseq1d 5995 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = (𝑇 ↾ (𝐷 ∖ ran 𝑢))) | 
| 101 | 82 | simpld 494 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ Word 𝐷) | 
| 102 | 101 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑢 ∈ Word 𝐷) | 
| 103 | 83 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑢:dom 𝑢–1-1→𝐷) | 
| 104 | 63, 10, 102, 103 | tocycfvres2 33132 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑀‘𝑢) ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢))) | 
| 105 | 100, 104 | eqtr3d 2778 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑇 ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ (𝐷 ∖ ran 𝑢))) | 
| 106 |  | disjdif 4471 | . . . . . . . . . . . . 13
⊢ (ran
𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅ | 
| 107 | 106 | a1i 11 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (ran 𝑢 ∩ (𝐷 ∖ ran 𝑢)) = ∅) | 
| 108 |  | undif 4481 | . . . . . . . . . . . . 13
⊢ (ran
𝑢 ⊆ 𝐷 ↔ (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷) | 
| 109 | 87, 108 | sylib 218 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (ran 𝑢 ∪ (𝐷 ∖ ran 𝑢)) = 𝐷) | 
| 110 | 26, 27, 39, 68, 98, 105, 107, 109 | symgcom 33104 | . . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇) = (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) | 
| 111 | 110 | coeq2d 5872 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))) | 
| 112 |  | cyc3conja.p | . . . . . . . . . . . . . . 15
⊢  + =
(+g‘𝑆) | 
| 113 | 26, 27, 112 | symgov 19402 | . . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) | 
| 114 | 11, 39, 113 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) | 
| 115 | 26, 27, 112 | symgcl 19403 | . . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ (Base‘𝑆) ∧ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) | 
| 116 | 11, 39, 115 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) | 
| 117 | 114, 116 | eqeltrrd 2841 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) | 
| 118 | 26, 27, 112 | symgov 19402 | . . . . . . . . . . . 12
⊢ (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇)) | 
| 119 | 117, 68, 118 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇)) | 
| 120 |  | coass 6284 | . . . . . . . . . . 11
⊢ ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇)) | 
| 121 | 119, 120 | eqtrdi 2792 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = (𝑔 ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ 𝑇))) | 
| 122 |  | coass 6284 | . . . . . . . . . . 11
⊢ ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) | 
| 123 | 122 | a1i 11 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (𝑔 ∘ (𝑇 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))) | 
| 124 | 111, 121,
123 | 3eqtr4d 2786 | . . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) = ((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) | 
| 125 |  | cnvco 5895 | . . . . . . . . . 10
⊢ ◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡𝑔) | 
| 126 | 125 | a1i 11 | . . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = (◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡𝑔)) | 
| 127 | 124, 126 | coeq12d 5874 | . . . . . . . 8
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡𝑔))) | 
| 128 |  | coass 6284 | . . . . . . . . . 10
⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ◡𝑔) = (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡𝑔)) | 
| 129 |  | coass 6284 | . . . . . . . . . . 11
⊢ (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) | 
| 130 | 129 | coeq1i 5869 | . . . . . . . . . 10
⊢ ((((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ ◡𝑔) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ◡𝑔) | 
| 131 | 128, 130 | eqtr3i 2766 | . . . . . . . . 9
⊢ (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡𝑔)) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ◡𝑔) | 
| 132 | 131 | a1i 11 | . . . . . . . 8
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∘ (◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡𝑔)) = (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ◡𝑔)) | 
| 133 | 26, 27, 112 | symgov 19402 | . . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇)) | 
| 134 | 11, 68, 133 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) = (𝑔 ∘ 𝑇)) | 
| 135 | 26, 27, 112 | symgcl 19403 | . . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → (𝑔 + 𝑇) ∈ (Base‘𝑆)) | 
| 136 | 11, 68, 135 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 + 𝑇) ∈ (Base‘𝑆)) | 
| 137 | 134, 136 | eqeltrrd 2841 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (𝑔 ∘ 𝑇) ∈ (Base‘𝑆)) | 
| 138 | 26, 27 | symgbasf 19394 | . . . . . . . . . . . 12
⊢ ((𝑔 ∘ 𝑇) ∈ (Base‘𝑆) → (𝑔 ∘ 𝑇):𝐷⟶𝐷) | 
| 139 |  | fcoi1 6781 | . . . . . . . . . . . 12
⊢ ((𝑔 ∘ 𝑇):𝐷⟶𝐷 → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇)) | 
| 140 | 137, 138,
139 | 3syl 18 | . . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷)) = (𝑔 ∘ 𝑇)) | 
| 141 | 26, 27 | elsymgbas 19392 | . . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ Fin →
(((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆) ↔ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷)) | 
| 142 | 141 | biimpa 476 | . . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧
((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∈ (Base‘𝑆)) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷) | 
| 143 | 10, 39, 142 | syl2anc 584 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷) | 
| 144 |  | f1ococnv2 6874 | . . . . . . . . . . . . 13
⊢
(((pmTrsp‘𝐷)‘{𝑥, 𝑦}):𝐷–1-1-onto→𝐷 → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷)) | 
| 145 | 143, 144 | syl 17 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦})) = ( I ↾ 𝐷)) | 
| 146 | 145 | coeq2d 5872 | . . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 ∘ 𝑇) ∘ ( I ↾ 𝐷))) | 
| 147 | 140, 146,
134 | 3eqtr4d 2786 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (𝑔 + 𝑇)) | 
| 148 | 147 | coeq1d 5871 | . . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ◡𝑔) = ((𝑔 + 𝑇) ∘ ◡𝑔)) | 
| 149 |  | cyc3conja.l | . . . . . . . . . . 11
⊢  − =
(-g‘𝑆) | 
| 150 | 26, 27, 149 | symgsubg 33108 | . . . . . . . . . 10
⊢ (((𝑔 + 𝑇) ∈ (Base‘𝑆) ∧ 𝑔 ∈ (Base‘𝑆)) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ◡𝑔)) | 
| 151 | 136, 11, 150 | syl2anc 584 | . . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 + 𝑇) − 𝑔) = ((𝑔 + 𝑇) ∘ ◡𝑔)) | 
| 152 | 148, 151 | eqtr4d 2779 | . . . . . . . 8
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ 𝑇) ∘ (((pmTrsp‘𝐷)‘{𝑥, 𝑦}) ∘ ◡((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) ∘ ◡𝑔) = ((𝑔 + 𝑇) − 𝑔)) | 
| 153 | 127, 132,
152 | 3eqtrd 2780 | . . . . . . 7
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = ((𝑔 + 𝑇) − 𝑔)) | 
| 154 | 26 | symggrp 19419 | . . . . . . . . . . 11
⊢ (𝐷 ∈ Fin → 𝑆 ∈ Grp) | 
| 155 | 8, 154 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ Grp) | 
| 156 | 155 | ad8antr 740 | . . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑆 ∈ Grp) | 
| 157 | 27, 112 | grpcl 18960 | . . . . . . . . 9
⊢ ((𝑆 ∈ Grp ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆) ∧ 𝑇 ∈ (Base‘𝑆)) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆)) | 
| 158 | 156, 117,
68, 157 | syl3anc 1372 | . . . . . . . 8
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆)) | 
| 159 | 26, 27, 149 | symgsubg 33108 | . . . . . . . 8
⊢ ((((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∈ (Base‘𝑆) ∧ (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) ∈ (Base‘𝑆)) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))) | 
| 160 | 158, 117,
159 | syl2anc 584 | . . . . . . 7
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦}))) = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) ∘ ◡(𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))) | 
| 161 |  | simp-7r 789 | . . . . . . 7
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑄 = ((𝑔 + 𝑇) − 𝑔)) | 
| 162 | 153, 160,
161 | 3eqtr4rd 2787 | . . . . . 6
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → 𝑄 = (((𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})) + 𝑇) − (𝑔 ∘ ((pmTrsp‘𝐷)‘{𝑥, 𝑦})))) | 
| 163 | 34, 38, 162 | rspcedvd 3623 | . . . . 5
⊢
(((((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) ∧ 𝑥 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑦 ∈ (𝐷 ∖ ran 𝑢)) ∧ 𝑥 ≠ 𝑦) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝)) | 
| 164 | 8 | difexd 5330 | . . . . . . 7
⊢ (𝜑 → (𝐷 ∖ ran 𝑢) ∈ V) | 
| 165 | 164 | ad5antr 734 | . . . . . 6
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝐷 ∖ ran 𝑢) ∈ V) | 
| 166 |  | 3p2e5 12418 | . . . . . . . . . . 11
⊢ (3 + 2) =
5 | 
| 167 | 166, 59 | eqbrtrid 5177 | . . . . . . . . . 10
⊢ (𝜑 → (3 + 2) ≤ 𝑁) | 
| 168 |  | 2re 12341 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ | 
| 169 | 168 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) | 
| 170 | 49, 169, 55 | leaddsub2d 11866 | . . . . . . . . . 10
⊢ (𝜑 → ((3 + 2) ≤ 𝑁 ↔ 2 ≤ (𝑁 − 3))) | 
| 171 | 167, 170 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → 2 ≤ (𝑁 − 3)) | 
| 172 | 171 | ad5antr 734 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ (𝑁 − 3)) | 
| 173 | 41 | a1i 11 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑁 = (♯‘𝐷)) | 
| 174 | 75 | elin2d 4204 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 𝑢 ∈ (◡♯ “ {3})) | 
| 175 |  | hashf 14378 | . . . . . . . . . . . . 13
⊢
♯:V⟶(ℕ0 ∪ {+∞}) | 
| 176 |  | ffn 6735 | . . . . . . . . . . . . 13
⊢
(♯:V⟶(ℕ0 ∪ {+∞}) → ♯
Fn V) | 
| 177 |  | fniniseg 7079 | . . . . . . . . . . . . 13
⊢ (♯
Fn V → (𝑢 ∈
(◡♯ “ {3}) ↔ (𝑢 ∈ V ∧
(♯‘𝑢) =
3))) | 
| 178 | 175, 176,
177 | mp2b 10 | . . . . . . . . . . . 12
⊢ (𝑢 ∈ (◡♯ “ {3}) ↔ (𝑢 ∈ V ∧
(♯‘𝑢) =
3)) | 
| 179 | 178 | simprbi 496 | . . . . . . . . . . 11
⊢ (𝑢 ∈ (◡♯ “ {3}) →
(♯‘𝑢) =
3) | 
| 180 | 174, 179 | syl 17 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘𝑢) = 3) | 
| 181 |  | vex 3483 | . . . . . . . . . . . 12
⊢ 𝑢 ∈ V | 
| 182 | 181 | dmex 7932 | . . . . . . . . . . 11
⊢ dom 𝑢 ∈ V | 
| 183 |  | hashf1rn 14392 | . . . . . . . . . . 11
⊢ ((dom
𝑢 ∈ V ∧ 𝑢:dom 𝑢–1-1→𝐷) → (♯‘𝑢) = (♯‘ran 𝑢)) | 
| 184 | 182, 83, 183 | sylancr 587 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘𝑢) = (♯‘ran 𝑢)) | 
| 185 | 180, 184 | eqtr3d 2778 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 3 = (♯‘ran 𝑢)) | 
| 186 | 173, 185 | oveq12d 7450 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (𝑁 − 3) = ((♯‘𝐷) − (♯‘ran
𝑢))) | 
| 187 | 172, 186 | breqtrd 5168 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ ((♯‘𝐷) − (♯‘ran
𝑢))) | 
| 188 |  | hashssdif 14452 | . . . . . . . 8
⊢ ((𝐷 ∈ Fin ∧ ran 𝑢 ⊆ 𝐷) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢))) | 
| 189 | 9, 86, 188 | syl2anc 584 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → (♯‘(𝐷 ∖ ran 𝑢)) = ((♯‘𝐷) − (♯‘ran 𝑢))) | 
| 190 | 187, 189 | breqtrrd 5170 | . . . . . 6
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → 2 ≤ (♯‘(𝐷 ∖ ran 𝑢))) | 
| 191 |  | hashge2el2dif 14520 | . . . . . 6
⊢ (((𝐷 ∖ ran 𝑢) ∈ V ∧ 2 ≤ (♯‘(𝐷 ∖ ran 𝑢))) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥 ≠ 𝑦) | 
| 192 | 165, 190,
191 | syl2anc 584 | . . . . 5
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ∃𝑥 ∈ (𝐷 ∖ ran 𝑢)∃𝑦 ∈ (𝐷 ∖ ran 𝑢)𝑥 ≠ 𝑦) | 
| 193 | 163, 192 | r19.29vva 3215 | . . . 4
⊢
((((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))) ∧ (𝑀‘𝑢) = 𝑇) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝)) | 
| 194 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑢𝑀 | 
| 195 | 63, 26, 27 | tocycf 33138 | . . . . . . 7
⊢ (𝐷 ∈ Fin → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) | 
| 196 |  | ffn 6735 | . . . . . . 7
⊢ (𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆) → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 197 | 8, 195, 196 | 3syl 18 | . . . . . 6
⊢ (𝜑 → 𝑀 Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 198 | 66, 62 | eleqtrdi 2850 | . . . . . 6
⊢ (𝜑 → 𝑇 ∈ (𝑀 “ (◡♯ “ {3}))) | 
| 199 | 194, 197,
198 | fvelimad 6975 | . . . . 5
⊢ (𝜑 → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))(𝑀‘𝑢) = 𝑇) | 
| 200 | 199 | ad3antrrr 730 | . . . 4
⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ∩ (◡♯ “ {3}))(𝑀‘𝑢) = 𝑇) | 
| 201 | 193, 200 | r19.29a 3161 | . . 3
⊢ ((((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) ∧ ¬ 𝑔 ∈ 𝐴) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝)) | 
| 202 | 7, 201 | pm2.61dan 812 | . 2
⊢ (((𝜑 ∧ 𝑔 ∈ (Base‘𝑆)) ∧ 𝑄 = ((𝑔 + 𝑇) − 𝑔)) → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝)) | 
| 203 |  | cyc3conja.q | . . 3
⊢ (𝜑 → 𝑄 ∈ 𝐶) | 
| 204 | 62, 26, 41, 63, 27, 112, 149, 61, 8, 203, 66 | cycpmconjs 33177 | . 2
⊢ (𝜑 → ∃𝑔 ∈ (Base‘𝑆)𝑄 = ((𝑔 + 𝑇) − 𝑔)) | 
| 205 | 202, 204 | r19.29a 3161 | 1
⊢ (𝜑 → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝)) |