Theorem sseqmw

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

	Ref	Expression
Hypotheses	sseqval.1	⊢ ( 𝜑 → 𝑆 ∈ V )
	sseqval.2	⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
	sseqval.3	⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
	sseqval.4	⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
Assertion	sseqmw	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		sseqval.1	⊢ ( 𝜑 → 𝑆 ∈ V )
2		sseqval.2	⊢ ( 𝜑 → 𝑀 ∈ Word 𝑆 )
3		sseqval.3	⊢ 𝑊 = ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
4		sseqval.4	⊢ ( 𝜑 → 𝐹 : 𝑊 ⟶ 𝑆 )
5		elex	⊢ ( 𝑀 ∈ Word 𝑆 → 𝑀 ∈ V )
6	2 5	syl	⊢ ( 𝜑 → 𝑀 ∈ V )
7		lencl	⊢ ( 𝑀 ∈ Word 𝑆 → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
8	7	nn0zd	⊢ ( 𝑀 ∈ Word 𝑆 → ( ♯ ‘ 𝑀 ) ∈ ℤ )
9		uzid	⊢ ( ( ♯ ‘ 𝑀 ) ∈ ℤ → ( ♯ ‘ 𝑀 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
10	2 8 9	3syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) )
11		hashf	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
12		ffn	⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
13		elpreima	⊢ ( ♯ Fn V → ( 𝑀 ∈ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) ↔ ( 𝑀 ∈ V ∧ ( ♯ ‘ 𝑀 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) ) )
14	11 12 13	mp2b	⊢ ( 𝑀 ∈ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) ↔ ( 𝑀 ∈ V ∧ ( ♯ ‘ 𝑀 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
15	6 10 14	sylanbrc	⊢ ( 𝜑 → 𝑀 ∈ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) )
16	2 15	elind	⊢ ( 𝜑 → 𝑀 ∈ ( Word 𝑆 ∩ ( ◡ ♯ “ ( ℤ≥ ‘ ( ♯ ‘ 𝑀 ) ) ) ) )
17	16 3	eleqtrrdi	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )