Description: Closure of the 3-cycles in the permutations. (Contributed by Thierry Arnoux, 19-Sep-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cycpm3.c | ⊢ 𝐶 = ( toCyc ‘ 𝐷 ) | |
| cycpm3.s | ⊢ 𝑆 = ( SymGrp ‘ 𝐷 ) | ||
| cycpm3.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 ) | ||
| cycpm3.i | ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 ) | ||
| cycpm3.j | ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 ) | ||
| cycpm3.k | ⊢ ( 𝜑 → 𝐾 ∈ 𝐷 ) | ||
| cycpm3.1 | ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 ) | ||
| cycpm3.2 | ⊢ ( 𝜑 → 𝐽 ≠ 𝐾 ) | ||
| cycpm3.3 | ⊢ ( 𝜑 → 𝐾 ≠ 𝐼 ) | ||
| Assertion | cycpm3cl | ⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cycpm3.c | ⊢ 𝐶 = ( toCyc ‘ 𝐷 ) | |
| 2 | cycpm3.s | ⊢ 𝑆 = ( SymGrp ‘ 𝐷 ) | |
| 3 | cycpm3.d | ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 ) | |
| 4 | cycpm3.i | ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 ) | |
| 5 | cycpm3.j | ⊢ ( 𝜑 → 𝐽 ∈ 𝐷 ) | |
| 6 | cycpm3.k | ⊢ ( 𝜑 → 𝐾 ∈ 𝐷 ) | |
| 7 | cycpm3.1 | ⊢ ( 𝜑 → 𝐼 ≠ 𝐽 ) | |
| 8 | cycpm3.2 | ⊢ ( 𝜑 → 𝐽 ≠ 𝐾 ) | |
| 9 | cycpm3.3 | ⊢ ( 𝜑 → 𝐾 ≠ 𝐼 ) | |
| 10 | 4 5 6 | s3cld | ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ Word 𝐷 ) |
| 11 | 4 5 6 7 8 9 | s3f1 | ⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ : dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ –1-1→ 𝐷 ) |
| 12 | 1 3 10 11 2 | cycpmcl | ⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∈ ( Base ‘ 𝑆 ) ) |