1wlkdlem4

	Ref	Expression
Hypotheses	1wlkd.p	$⊢ P = ⟨“ X Y ”⟩$
	1wlkd.f	$⊢ F = ⟨“ J ”⟩$
	1wlkd.x	$⊢ φ \to X \in V$
	1wlkd.y	$⊢ φ \to Y \in V$
	1wlkd.l	$⊢ (φ \land X = Y) \to I (J) = \{X\}$
	1wlkd.j	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq I (J)$
Assertion	1wlkdlem4	$⊢ φ \to \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$

Proof

Step	Hyp	Ref	Expression
1		1wlkd.p	$⊢ P = ⟨“ X Y ”⟩$
2		1wlkd.f	$⊢ F = ⟨“ J ”⟩$
3		1wlkd.x	$⊢ φ \to X \in V$
4		1wlkd.y	$⊢ φ \to Y \in V$
5		1wlkd.l	$⊢ (φ \land X = Y) \to I (J) = \{X\}$
6		1wlkd.j	$⊢ (φ \land X \neq Y) \to \{X, Y\} \subseteq I (J)$
7	2	fveq1i	$⊢ F (0) = ⟨“ J ”⟩ (0)$
8	1 2 3 4 5 6	1wlkdlem2	$⊢ φ \to X \in I (J)$
9	8	elfvexd	$⊢ φ \to J \in V$
10		s1fv	$⊢ J \in V \to ⟨“ J ”⟩ (0) = J$
11	9 10	syl	$⊢ φ \to ⟨“ J ”⟩ (0) = J$
12	7 11	eqtrid	$⊢ φ \to F (0) = J$
13	12	fveq2d	$⊢ φ \to I (F (0)) = I (J)$
14	13	adantr	$⊢ (φ \land X = Y) \to I (F (0)) = I (J)$
15	14 5	eqtrd	$⊢ (φ \land X = Y) \to I (F (0)) = \{X\}$
16		df-ne	$⊢ X \neq Y \leftrightarrow \neg X = Y$
17	16 6	sylan2br	$⊢ (φ \land \neg X = Y) \to \{X, Y\} \subseteq I (J)$
18	13	adantr	$⊢ (φ \land \neg X = Y) \to I (F (0)) = I (J)$
19	17 18	sseqtrrd	$⊢ (φ \land \neg X = Y) \to \{X, Y\} \subseteq I (F (0))$
20	15 19	ifpimpda	$⊢ φ \to if- (X = Y, I (F (0)) = \{X\}, \{X, Y\} \subseteq I (F (0)))$
21	1	fveq1i	$⊢ P (0) = ⟨“ X Y ”⟩ (0)$
22		s2fv0	$⊢ X \in V \to ⟨“ X Y ”⟩ (0) = X$
23	3 22	syl	$⊢ φ \to ⟨“ X Y ”⟩ (0) = X$
24	21 23	eqtrid	$⊢ φ \to P (0) = X$
25	1	fveq1i	$⊢ P (1) = ⟨“ X Y ”⟩ (1)$
26		s2fv1	$⊢ Y \in V \to ⟨“ X Y ”⟩ (1) = Y$
27	4 26	syl	$⊢ φ \to ⟨“ X Y ”⟩ (1) = Y$
28	25 27	eqtrid	$⊢ φ \to P (1) = Y$
29		eqeq12	$⊢ (P (0) = X \land P (1) = Y) \to (P (0) = P (1) \leftrightarrow X = Y)$
30		sneq	$⊢ P (0) = X \to \{P (0)\} = \{X\}$
31	30	adantr	$⊢ (P (0) = X \land P (1) = Y) \to \{P (0)\} = \{X\}$
32	31	eqeq2d	$⊢ (P (0) = X \land P (1) = Y) \to (I (F (0)) = \{P (0)\} \leftrightarrow I (F (0)) = \{X\})$
33		preq12	$⊢ (P (0) = X \land P (1) = Y) \to \{P (0), P (1)\} = \{X, Y\}$
34	33	sseq1d	$⊢ (P (0) = X \land P (1) = Y) \to (\{P (0), P (1)\} \subseteq I (F (0)) \leftrightarrow \{X, Y\} \subseteq I (F (0)))$
35	29 32 34	ifpbi123d	$⊢ (P (0) = X \land P (1) = Y) \to (if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0))) \leftrightarrow if- (X = Y, I (F (0)) = \{X\}, \{X, Y\} \subseteq I (F (0))))$
36	24 28 35	syl2anc	$⊢ φ \to (if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0))) \leftrightarrow if- (X = Y, I (F (0)) = \{X\}, \{X, Y\} \subseteq I (F (0))))$
37	20 36	mpbird	$⊢ φ \to if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0)))$
38		c0ex	$⊢ 0 \in V$
39		oveq1	$⊢ k = 0 \to k + 1 = 0 + 1$
40		0p1e1	$⊢ 0 + 1 = 1$
41	39 40	eqtrdi	$⊢ k = 0 \to k + 1 = 1$
42		wkslem2	$⊢ (k = 0 \land k + 1 = 1) \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \leftrightarrow if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0))))$
43	41 42	mpdan	$⊢ k = 0 \to (if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \leftrightarrow if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0))))$
44	38 43	ralsn	$⊢ \forall k \in \{0\} if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \leftrightarrow if- (P (0) = P (1), I (F (0)) = \{P (0)\}, \{P (0), P (1)\} \subseteq I (F (0)))$
45	37 44	sylibr	$⊢ φ \to \forall k \in \{0\} if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$
46	2	fveq2i	$⊢ \|F\| = \|⟨“ J ”⟩\|$
47		s1len	$⊢ \|⟨“ J ”⟩\| = 1$
48	46 47	eqtri	$⊢ \|F\| = 1$
49	48	oveq2i	$⊢ (0 ..^\|F\|) = (0 ..^1)$
50		fzo01	$⊢ (0 ..^1) = \{0\}$
51	49 50	eqtri	$⊢ (0 ..^\|F\|) = \{0\}$
52	51	a1i	$⊢ φ \to (0 ..^\|F\|) = \{0\}$
53	52	raleqdv	$⊢ φ \to (\forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))) \leftrightarrow \forall k \in \{0\} if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k))))$
54	45 53	mpbird	$⊢ φ \to \forall k \in (0 ..^\|F\|) if- (P (k) = P (k + 1), I (F (k)) = \{P (k)\}, \{P (k), P (k + 1)\} \subseteq I (F (k)))$

Metamath Proof Explorer

Theorem 1wlkdlem4

Proof