wrdlen2i

Description: Implications of a word of length two. (Contributed by AV, 27-Jul-2018) (Proof shortened by AV, 14-Oct-2018)

		Ref	Expression
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		c0ex	$⊢ 0 \in V$
2		1ex	$⊢ 1 \in V$
3	1 2	pm3.2i	$⊢ (0 \in V \land 1 \in V)$
4		simpl	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to (S \in V \land T \in V)$
5		0ne1	$⊢ 0 \neq 1$
6	5	a1i	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to 0 \neq 1$
7		fprg	$⊢ ((0 \in V \land 1 \in V) \land (S \in V \land T \in V) \land 0 \neq 1) \to \{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\}$
8	3 4 6 7	mp3an2i	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to \{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\}$
9		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
10	9	eqcomi	$⊢ \{0, 1\} = (0 ..^2)$
11	10	a1i	$⊢ (S \in V \land T \in V) \to \{0, 1\} = (0 ..^2)$
12	11	feq2d	$⊢ (S \in V \land T \in V) \to (\{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\} \leftrightarrow \{⟨0, S⟩, ⟨1, T⟩\} : (0 ..^2) ⟶ \{S, T\})$
13	12	biimpa	$⊢ ((S \in V \land T \in V) \land \{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\}) \to \{⟨0, S⟩, ⟨1, T⟩\} : (0 ..^2) ⟶ \{S, T\}$
14		prssi	$⊢ (S \in V \land T \in V) \to \{S, T\} \subseteq V$
15	14	adantr	$⊢ ((S \in V \land T \in V) \land \{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\}) \to \{S, T\} \subseteq V$
16	13 15	fssd	$⊢ ((S \in V \land T \in V) \land \{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\}) \to \{⟨0, S⟩, ⟨1, T⟩\} : (0 ..^2) ⟶ V$
17	16	ex	$⊢ (S \in V \land T \in V) \to (\{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\} \to \{⟨0, S⟩, ⟨1, T⟩\} : (0 ..^2) ⟶ V)$
18	17	adantr	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to (\{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\} \to \{⟨0, S⟩, ⟨1, T⟩\} : (0 ..^2) ⟶ V)$
19	18	impcom	$⊢ (\{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\} \land ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\})) \to \{⟨0, S⟩, ⟨1, T⟩\} : (0 ..^2) ⟶ V$
20		feq1	$⊢ W = \{⟨0, S⟩, ⟨1, T⟩\} \to (W : (0 ..^2) ⟶ V \leftrightarrow \{⟨0, S⟩, ⟨1, T⟩\} : (0 ..^2) ⟶ V)$
21	20	adantl	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to (W : (0 ..^2) ⟶ V \leftrightarrow \{⟨0, S⟩, ⟨1, T⟩\} : (0 ..^2) ⟶ V)$
22	21	adantl	$⊢ (\{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\} \land ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\})) \to (W : (0 ..^2) ⟶ V \leftrightarrow \{⟨0, S⟩, ⟨1, T⟩\} : (0 ..^2) ⟶ V)$
23	19 22	mpbird	$⊢ (\{⟨0, S⟩, ⟨1, T⟩\} : \{0, 1\} ⟶ \{S, T\} \land ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\})) \to W : (0 ..^2) ⟶ V$
24	8 23	mpancom	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to W : (0 ..^2) ⟶ V$
25		iswrdi	$⊢ W : (0 ..^2) ⟶ V \to W \in Word V$
26	24 25	syl	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to W \in Word V$
27		fveq2	$⊢ W = \{⟨0, S⟩, ⟨1, T⟩\} \to \|W\| = \|\{⟨0, S⟩, ⟨1, T⟩\}\|$
28	5	neii	$⊢ \neg 0 = 1$
29		simpl	$⊢ (S \in V \land T \in V) \to S \in V$
30		opth1g	$⊢ (0 \in V \land S \in V) \to (⟨0, S⟩ = ⟨1, T⟩ \to 0 = 1)$
31	1 29 30	sylancr	$⊢ (S \in V \land T \in V) \to (⟨0, S⟩ = ⟨1, T⟩ \to 0 = 1)$
32	28 31	mtoi	$⊢ (S \in V \land T \in V) \to \neg ⟨0, S⟩ = ⟨1, T⟩$
33	32	neqned	$⊢ (S \in V \land T \in V) \to ⟨0, S⟩ \neq ⟨1, T⟩$
34		opex	$⊢ ⟨0, S⟩ \in V$
35		opex	$⊢ ⟨1, T⟩ \in V$
36	34 35	pm3.2i	$⊢ (⟨0, S⟩ \in V \land ⟨1, T⟩ \in V)$
37		hashprg	$⊢ (⟨0, S⟩ \in V \land ⟨1, T⟩ \in V) \to (⟨0, S⟩ \neq ⟨1, T⟩ \leftrightarrow \|\{⟨0, S⟩, ⟨1, T⟩\}\| = 2)$
38	36 37	mp1i	$⊢ (S \in V \land T \in V) \to (⟨0, S⟩ \neq ⟨1, T⟩ \leftrightarrow \|\{⟨0, S⟩, ⟨1, T⟩\}\| = 2)$
39	33 38	mpbid	$⊢ (S \in V \land T \in V) \to \|\{⟨0, S⟩, ⟨1, T⟩\}\| = 2$
40	27 39	sylan9eqr	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to \|W\| = 2$
41	5	a1i	$⊢ (S \in V \land T \in V) \to 0 \neq 1$
42		fvpr1g	$⊢ (0 \in V \land S \in V \land 0 \neq 1) \to \{⟨0, S⟩, ⟨1, T⟩\} (0) = S$
43	1 29 41 42	mp3an2i	$⊢ (S \in V \land T \in V) \to \{⟨0, S⟩, ⟨1, T⟩\} (0) = S$
44		simpr	$⊢ (S \in V \land T \in V) \to T \in V$
45		fvpr2g	$⊢ (1 \in V \land T \in V \land 0 \neq 1) \to \{⟨0, S⟩, ⟨1, T⟩\} (1) = T$
46	2 44 41 45	mp3an2i	$⊢ (S \in V \land T \in V) \to \{⟨0, S⟩, ⟨1, T⟩\} (1) = T$
47	43 46	jca	$⊢ (S \in V \land T \in V) \to (\{⟨0, S⟩, ⟨1, T⟩\} (0) = S \land \{⟨0, S⟩, ⟨1, T⟩\} (1) = T)$
48	47	adantr	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to (\{⟨0, S⟩, ⟨1, T⟩\} (0) = S \land \{⟨0, S⟩, ⟨1, T⟩\} (1) = T)$
49		fveq1	$⊢ W = \{⟨0, S⟩, ⟨1, T⟩\} \to W (0) = \{⟨0, S⟩, ⟨1, T⟩\} (0)$
50	49	eqeq1d	$⊢ W = \{⟨0, S⟩, ⟨1, T⟩\} \to (W (0) = S \leftrightarrow \{⟨0, S⟩, ⟨1, T⟩\} (0) = S)$
51		fveq1	$⊢ W = \{⟨0, S⟩, ⟨1, T⟩\} \to W (1) = \{⟨0, S⟩, ⟨1, T⟩\} (1)$
52	51	eqeq1d	$⊢ W = \{⟨0, S⟩, ⟨1, T⟩\} \to (W (1) = T \leftrightarrow \{⟨0, S⟩, ⟨1, T⟩\} (1) = T)$
53	50 52	anbi12d	$⊢ W = \{⟨0, S⟩, ⟨1, T⟩\} \to ((W (0) = S \land W (1) = T) \leftrightarrow (\{⟨0, S⟩, ⟨1, T⟩\} (0) = S \land \{⟨0, S⟩, ⟨1, T⟩\} (1) = T))$
54	53	adantl	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to ((W (0) = S \land W (1) = T) \leftrightarrow (\{⟨0, S⟩, ⟨1, T⟩\} (0) = S \land \{⟨0, S⟩, ⟨1, T⟩\} (1) = T))$
55	48 54	mpbird	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to (W (0) = S \land W (1) = T)$
56	26 40 55	jca31	$⊢ ((S \in V \land T \in V) \land W = \{⟨0, S⟩, ⟨1, T⟩\}) \to ((W \in Word V \land \|W\| = 2) \land (W (0) = S \land W (1) = T))$
57	56	ex	$⊢ (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)))$

Metamath Proof Explorer

Theorem wrdlen2i

Proof