wrdpmcl

Description: Closure of a word with permuted symbols. (Contributed by Thierry Arnoux, 27-May-2025)

Step	Hyp	Ref	Expression
1		wrdpmcl.1	$⊢ J = (0 ..^\|W\|)$
2		wrdpmcl.2	$⊢ φ \to E : J \underset{1-1 onto}{⟶} J$
3		wrdpmcl.3	$⊢ φ \to W \in Word S$
4		eqidd	$⊢ φ \to \|W\| = \|W\|$
5	4 3	wrdfd	$⊢ φ \to W : (0 ..^\|W\|) ⟶ S$
6		f1oeq23	$⊢ (J = (0 ..^\|W\|) \land J = (0 ..^\|W\|)) \to (E : J \underset{1-1 onto}{⟶} J \leftrightarrow E : (0 ..^\|W\|) \underset{1-1 onto}{⟶} (0 ..^\|W\|))$
7	1 1 6	mp2an	$⊢ E : J \underset{1-1 onto}{⟶} J \leftrightarrow E : (0 ..^\|W\|) \underset{1-1 onto}{⟶} (0 ..^\|W\|)$
8	2 7	sylib	$⊢ φ \to E : (0 ..^\|W\|) \underset{1-1 onto}{⟶} (0 ..^\|W\|)$
9		f1of	$⊢ E : (0 ..^\|W\|) \underset{1-1 onto}{⟶} (0 ..^\|W\|) \to E : (0 ..^\|W\|) ⟶ (0 ..^\|W\|)$
10	8 9	syl	$⊢ φ \to E : (0 ..^\|W\|) ⟶ (0 ..^\|W\|)$
11	5 10	fcod	$⊢ φ \to (W \circ E) : (0 ..^\|W\|) ⟶ S$
12		iswrdi	$⊢ (W \circ E) : (0 ..^\|W\|) ⟶ S \to W \circ E \in Word S$
13	11 12	syl	$⊢ φ \to W \circ E \in Word S$

Metamath Proof Explorer