wrdlen2

		Ref	Expression
	Assertion	wrdlen2	$⊢ (S \in V \land T \in V) \to (W = \{⟨0, S⟩, ⟨1, T⟩\} \leftrightarrow ((W \in Word V \land \|W\| = 2) \land (W (0) = S \land W (1) = T)))$

Step	Hyp	Ref	Expression
1		wrdlen2i	$⊢ (S \in V \land T \in V) \to (W = \{⟨0, S⟩, ⟨1, T⟩\} \to ((W \in Word V \land \|W\| = 2) \land (W (0) = S \land W (1) = T)))$
2		wrd2pr2op	$⊢ (W \in Word V \land \|W\| = 2) \to W = \{⟨0, W (0)⟩, ⟨1, W (1)⟩\}$
3		opeq2	$⊢ W (0) = S \to ⟨0, W (0)⟩ = ⟨0, S⟩$
4	3	adantr	$⊢ (W (0) = S \land W (1) = T) \to ⟨0, W (0)⟩ = ⟨0, S⟩$
5		opeq2	$⊢ W (1) = T \to ⟨1, W (1)⟩ = ⟨1, T⟩$
6	5	adantl	$⊢ (W (0) = S \land W (1) = T) \to ⟨1, W (1)⟩ = ⟨1, T⟩$
7	4 6	preq12d	$⊢ (W (0) = S \land W (1) = T) \to \{⟨0, W (0)⟩, ⟨1, W (1)⟩\} = \{⟨0, S⟩, ⟨1, T⟩\}$
8	2 7	sylan9eq	$⊢ ((W \in Word V \land \|W\| = 2) \land (W (0) = S \land W (1) = T)) \to W = \{⟨0, S⟩, ⟨1, T⟩\}$
9	1 8	impbid1	$⊢ (S \in V \land T \in V) \to (W = \{⟨0, S⟩, ⟨1, T⟩\} \leftrightarrow ((W \in Word V \land \|W\| = 2) \land (W (0) = S \land W (1) = T)))$

Metamath Proof Explorer