Theorem sseqmw

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

	Ref	Expression
Hypotheses	sseqval.1	|- ( ph -> S e. _V )
	sseqval.2	|- ( ph -> M e. Word S )
	sseqval.3	|- W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
	sseqval.4	|- ( ph -> F : W --> S )
Assertion	sseqmw	|- ( ph -> M e. W )

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	|- ( ph -> S e. _V )
2		sseqval.2	|- ( ph -> M e. Word S )
3		sseqval.3	|- W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
4		sseqval.4	|- ( ph -> F : W --> S )
5		elex	|- ( M e. Word S -> M e. _V )
6	2 5	syl	|- ( ph -> M e. _V )
7		lencl	|- ( M e. Word S -> ( # ` M ) e. NN0 )
8	7	nn0zd	|- ( M e. Word S -> ( # ` M ) e. ZZ )
9		uzid	|- ( ( # ` M ) e. ZZ -> ( # ` M ) e. ( ZZ>= ` ( # ` M ) ) )
10	2 8 9	3syl	|- ( ph -> ( # ` M ) e. ( ZZ>= ` ( # ` M ) ) )
11		hashf	|- # : _V --> ( NN0 u. { +oo } )
12		ffn	|- ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
13		elpreima	|- ( # Fn _V -> ( M e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( M e. _V /\ ( # ` M ) e. ( ZZ>= ` ( # ` M ) ) ) ) )
14	11 12 13	mp2b	|- ( M e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) <-> ( M e. _V /\ ( # ` M ) e. ( ZZ>= ` ( # ` M ) ) ) )
15	6 10 14	sylanbrc	|- ( ph -> M e. ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
16	2 15	elind	|- ( ph -> M e. ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) ) )
17	16 3	eleqtrrdi	|- ( ph -> M e. W )