wwlktovf1

	Ref	Expression
Hypotheses	wwlktovf1o.d	$⊢ D = \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\}$
	wwlktovf1o.r	$⊢ R = \{n \in V \| \{P, n\} \in X\}$
	wwlktovf1o.f	$⊢ F = (t \in D ⟼ t (1))$
Assertion	wwlktovf1	$⊢ F : D \underset{1-1}{⟶} R$

Proof

Step	Hyp	Ref	Expression
1		wwlktovf1o.d	$⊢ D = \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\}$
2		wwlktovf1o.r	$⊢ R = \{n \in V \| \{P, n\} \in X\}$
3		wwlktovf1o.f	$⊢ F = (t \in D ⟼ t (1))$
4	1 2 3	wwlktovf	$⊢ F : D ⟶ R$
5		fveq1	$⊢ t = x \to t (1) = x (1)$
6		fvex	$⊢ x (1) \in V$
7	5 3 6	fvmpt	$⊢ x \in D \to F (x) = x (1)$
8		fveq1	$⊢ t = y \to t (1) = y (1)$
9		fvex	$⊢ y (1) \in V$
10	8 3 9	fvmpt	$⊢ y \in D \to F (y) = y (1)$
11	7 10	eqeqan12d	$⊢ (x \in D \land y \in D) \to (F (x) = F (y) \leftrightarrow x (1) = y (1))$
12		fveqeq2	$⊢ w = x \to (\|w\| = 2 \leftrightarrow \|x\| = 2)$
13		fveq1	$⊢ w = x \to w (0) = x (0)$
14	13	eqeq1d	$⊢ w = x \to (w (0) = P \leftrightarrow x (0) = P)$
15		fveq1	$⊢ w = x \to w (1) = x (1)$
16	13 15	preq12d	$⊢ w = x \to \{w (0), w (1)\} = \{x (0), x (1)\}$
17	16	eleq1d	$⊢ w = x \to (\{w (0), w (1)\} \in X \leftrightarrow \{x (0), x (1)\} \in X)$
18	12 14 17	3anbi123d	$⊢ w = x \to ((\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X) \leftrightarrow (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X))$
19	18 1	elrab2	$⊢ x \in D \leftrightarrow (x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X))$
20		fveqeq2	$⊢ w = y \to (\|w\| = 2 \leftrightarrow \|y\| = 2)$
21		fveq1	$⊢ w = y \to w (0) = y (0)$
22	21	eqeq1d	$⊢ w = y \to (w (0) = P \leftrightarrow y (0) = P)$
23		fveq1	$⊢ w = y \to w (1) = y (1)$
24	21 23	preq12d	$⊢ w = y \to \{w (0), w (1)\} = \{y (0), y (1)\}$
25	24	eleq1d	$⊢ w = y \to (\{w (0), w (1)\} \in X \leftrightarrow \{y (0), y (1)\} \in X)$
26	20 22 25	3anbi123d	$⊢ w = y \to ((\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X) \leftrightarrow (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))$
27	26 1	elrab2	$⊢ y \in D \leftrightarrow (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))$
28		simpr1	$⊢ (x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \to \|x\| = 2$
29		simpr1	$⊢ (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X)) \to \|y\| = 2$
30	29	eqcomd	$⊢ (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X)) \to 2 = \|y\|$
31	28 30	sylan9eq	$⊢ ((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \to \|x\| = \|y\|$
32	31	adantr	$⊢ (((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \land x (1) = y (1)) \to \|x\| = \|y\|$
33		simpr2	$⊢ (x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \to x (0) = P$
34		simpr2	$⊢ (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X)) \to y (0) = P$
35	34	eqcomd	$⊢ (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X)) \to P = y (0)$
36	33 35	sylan9eq	$⊢ ((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \to x (0) = y (0)$
37	36	adantr	$⊢ (((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \land x (1) = y (1)) \to x (0) = y (0)$
38		simpr	$⊢ (((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \land x (1) = y (1)) \to x (1) = y (1)$
39		oveq2	$⊢ \|x\| = 2 \to (0 ..^\|x\|) = (0 ..^2)$
40		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
41	39 40	eqtrdi	$⊢ \|x\| = 2 \to (0 ..^\|x\|) = \{0, 1\}$
42	41	raleqdv	$⊢ \|x\| = 2 \to (\forall i \in (0 ..^\|x\|) x (i) = y (i) \leftrightarrow \forall i \in \{0, 1\} x (i) = y (i))$
43		c0ex	$⊢ 0 \in V$
44		1ex	$⊢ 1 \in V$
45		fveq2	$⊢ i = 0 \to x (i) = x (0)$
46		fveq2	$⊢ i = 0 \to y (i) = y (0)$
47	45 46	eqeq12d	$⊢ i = 0 \to (x (i) = y (i) \leftrightarrow x (0) = y (0))$
48		fveq2	$⊢ i = 1 \to x (i) = x (1)$
49		fveq2	$⊢ i = 1 \to y (i) = y (1)$
50	48 49	eqeq12d	$⊢ i = 1 \to (x (i) = y (i) \leftrightarrow x (1) = y (1))$
51	43 44 47 50	ralpr	$⊢ \forall i \in \{0, 1\} x (i) = y (i) \leftrightarrow (x (0) = y (0) \land x (1) = y (1))$
52	42 51	bitrdi	$⊢ \|x\| = 2 \to (\forall i \in (0 ..^\|x\|) x (i) = y (i) \leftrightarrow (x (0) = y (0) \land x (1) = y (1)))$
53	52	3ad2ant1	$⊢ (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X) \to (\forall i \in (0 ..^\|x\|) x (i) = y (i) \leftrightarrow (x (0) = y (0) \land x (1) = y (1)))$
54	53	ad3antlr	$⊢ (((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \land x (1) = y (1)) \to (\forall i \in (0 ..^\|x\|) x (i) = y (i) \leftrightarrow (x (0) = y (0) \land x (1) = y (1)))$
55	37 38 54	mpbir2and	$⊢ (((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \land x (1) = y (1)) \to \forall i \in (0 ..^\|x\|) x (i) = y (i)$
56		eqwrd	$⊢ (x \in Word V \land y \in Word V) \to (x = y \leftrightarrow (\|x\| = \|y\| \land \forall i \in (0 ..^\|x\|) x (i) = y (i)))$
57	56	ad2ant2r	$⊢ ((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \to (x = y \leftrightarrow (\|x\| = \|y\| \land \forall i \in (0 ..^\|x\|) x (i) = y (i)))$
58	57	adantr	$⊢ (((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \land x (1) = y (1)) \to (x = y \leftrightarrow (\|x\| = \|y\| \land \forall i \in (0 ..^\|x\|) x (i) = y (i)))$
59	32 55 58	mpbir2and	$⊢ (((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \land x (1) = y (1)) \to x = y$
60	59	ex	$⊢ ((x \in Word V \land (\|x\| = 2 \land x (0) = P \land \{x (0), x (1)\} \in X)) \land (y \in Word V \land (\|y\| = 2 \land y (0) = P \land \{y (0), y (1)\} \in X))) \to (x (1) = y (1) \to x = y)$
61	19 27 60	syl2anb	$⊢ (x \in D \land y \in D) \to (x (1) = y (1) \to x = y)$
62	11 61	sylbid	$⊢ (x \in D \land y \in D) \to (F (x) = F (y) \to x = y)$
63	62	rgen2	$⊢ \forall x \in D \forall y \in D (F (x) = F (y) \to x = y)$
64		dff13	$⊢ F : D \underset{1-1}{⟶} R \leftrightarrow (F : D ⟶ R \land \forall x \in D \forall y \in D (F (x) = F (y) \to x = y))$
65	4 63 64	mpbir2an	$⊢ F : D \underset{1-1}{⟶} R$

Metamath Proof Explorer

Theorem wwlktovf1

Proof