wrdl2exs2

Description: A word of length two is a doubleton word. (Contributed by AV, 25-Jan-2021)

		Ref	Expression
	Assertion	wrdl2exs2	$⊢ (W \in Word S \land \|W\| = 2) \to \exists s \in S \exists t \in S W = ⟨“ s t ”⟩$

Proof

Step	Hyp	Ref	Expression
1		1le2	$⊢ 1 \leq 2$
2		breq2	$⊢ \|W\| = 2 \to (1 \leq \|W\| \leftrightarrow 1 \leq 2)$
3	1 2	mpbiri	$⊢ \|W\| = 2 \to 1 \leq \|W\|$
4		wrdsymb1	$⊢ (W \in Word S \land 1 \leq \|W\|) \to W (0) \in S$
5	3 4	sylan2	$⊢ (W \in Word S \land \|W\| = 2) \to W (0) \in S$
6		lsw	$⊢ W \in Word S \to lastS (W) = W (\|W\| - 1)$
7		oveq1	$⊢ \|W\| = 2 \to \|W\| - 1 = 2 - 1$
8		2m1e1	$⊢ 2 - 1 = 1$
9	7 8	eqtrdi	$⊢ \|W\| = 2 \to \|W\| - 1 = 1$
10	9	fveq2d	$⊢ \|W\| = 2 \to W (\|W\| - 1) = W (1)$
11	6 10	sylan9eq	$⊢ (W \in Word S \land \|W\| = 2) \to lastS (W) = W (1)$
12		2nn	$⊢ 2 \in ℕ$
13		lswlgt0cl	$⊢ (2 \in ℕ \land (W \in Word S \land \|W\| = 2)) \to lastS (W) \in S$
14	12 13	mpan	$⊢ (W \in Word S \land \|W\| = 2) \to lastS (W) \in S$
15	11 14	eqeltrrd	$⊢ (W \in Word S \land \|W\| = 2) \to W (1) \in S$
16		wrdlen2s2	$⊢ (W \in Word S \land \|W\| = 2) \to W = ⟨“ W (0) W (1) ”⟩$
17		id	$⊢ s = W (0) \to s = W (0)$
18		eqidd	$⊢ s = W (0) \to t = t$
19	17 18	s2eqd	$⊢ s = W (0) \to ⟨“ s t ”⟩ = ⟨“ W (0) t ”⟩$
20	19	eqeq2d	$⊢ s = W (0) \to (W = ⟨“ s t ”⟩ \leftrightarrow W = ⟨“ W (0) t ”⟩)$
21		eqidd	$⊢ t = W (1) \to W (0) = W (0)$
22		id	$⊢ t = W (1) \to t = W (1)$
23	21 22	s2eqd	$⊢ t = W (1) \to ⟨“ W (0) t ”⟩ = ⟨“ W (0) W (1) ”⟩$
24	23	eqeq2d	$⊢ t = W (1) \to (W = ⟨“ W (0) t ”⟩ \leftrightarrow W = ⟨“ W (0) W (1) ”⟩)$
25	20 24	rspc2ev	$⊢ (W (0) \in S \land W (1) \in S \land W = ⟨“ W (0) W (1) ”⟩) \to \exists s \in S \exists t \in S W = ⟨“ s t ”⟩$
26	5 15 16 25	syl3anc	$⊢ (W \in Word S \land \|W\| = 2) \to \exists s \in S \exists t \in S W = ⟨“ s t ”⟩$

Metamath Proof Explorer

Theorem wrdl2exs2

Proof