Theorem sseqmw

Description: Lemma for sseqf amd sseqp1 . (Contributed by Thierry Arnoux, 25-Apr-2019)

	Ref	Expression
Hypotheses	sseqval.1	$$⊢\phi \to S\in \mathrm{V}$$
	sseqval.2	$$⊢\phi \to M\in \mathrm{Word}S$$
	sseqval.3	$$⊢W=\mathrm{Word}S\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]$$
	sseqval.4	$$⊢\phi \to F:W⟶S$$
Assertion	sseqmw	$$⊢\phi \to M\in W$$

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	$$⊢\phi \to S\in \mathrm{V}$$
2		sseqval.2	$$⊢\phi \to M\in \mathrm{Word}S$$
3		sseqval.3	$$⊢W=\mathrm{Word}S\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]$$
4		sseqval.4	$$⊢\phi \to F:W⟶S$$
5		elex	$$⊢M\in \mathrm{Word}S\to M\in \mathrm{V}$$
6	2 5	syl	$$⊢\phi \to M\in \mathrm{V}$$
7		lencl	$$⊢M\in \mathrm{Word}S\to \left|M\right|\in {\mathbb{N}}_0$$
8	7	nn0zd	$$⊢M\in \mathrm{Word}S\to \left|M\right|\in \mathbb{Z}$$
9		uzid	$$⊢\left|M\right|\in \mathbb{Z}\to \left|M\right|\in {\mathbb{Z}}_{\ge \left|M\right|}$$
10	2 8 9	3syl	$$⊢\phi \to \left|M\right|\in {\mathbb{Z}}_{\ge \left|M\right|}$$
11		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
12		ffn	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\to \left|.\right|Fn\mathrm{V}$$
13		elpreima	$$⊢\left|.\right|Fn\mathrm{V}\to \left(M\in {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]\leftrightarrow \left(M\in \mathrm{V}\wedge \left|M\right|\in {\mathbb{Z}}_{\ge \left|M\right|}\right)\right)$$
14	11 12 13	mp2b	$$⊢M\in {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]\leftrightarrow \left(M\in \mathrm{V}\wedge \left|M\right|\in {\mathbb{Z}}_{\ge \left|M\right|}\right)$$
15	6 10 14	sylanbrc	$$⊢\phi \to M\in {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]$$
16	2 15	elind	$$⊢\phi \to M\in \left(\mathrm{Word}S\cap {\left|.\right|}^{-1}\left[{\mathbb{Z}}_{\ge \left|M\right|}\right]\right)$$
17	16 3	eleqtrrdi	$$⊢\phi \to M\in W$$