3wlkdlem6

	Ref	Expression
Hypotheses	3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
	3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
	3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
	3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
	3wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K) \land \{C, D\} \subseteq I (L))$
Assertion	3wlkdlem6	$⊢ φ \to (A \in I (J) \land B \in I (K) \land C \in I (L))$

Proof

Step	Hyp	Ref	Expression
1		3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
2		3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
3		3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
4		3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
5		3wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K) \land \{C, D\} \subseteq I (L))$
6	1 2 3	3wlkdlem3	$⊢ φ \to ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D))$
7		preq12	$⊢ (P (0) = A \land P (1) = B) \to \{P (0), P (1)\} = \{A, B\}$
8	7	sseq1d	$⊢ (P (0) = A \land P (1) = B) \to (\{P (0), P (1)\} \subseteq I (J) \leftrightarrow \{A, B\} \subseteq I (J))$
9	8	adantr	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (\{P (0), P (1)\} \subseteq I (J) \leftrightarrow \{A, B\} \subseteq I (J))$
10		preq12	$⊢ (P (1) = B \land P (2) = C) \to \{P (1), P (2)\} = \{B, C\}$
11	10	ad2ant2lr	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to \{P (1), P (2)\} = \{B, C\}$
12	11	sseq1d	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (\{P (1), P (2)\} \subseteq I (K) \leftrightarrow \{B, C\} \subseteq I (K))$
13		preq12	$⊢ (P (2) = C \land P (3) = D) \to \{P (2), P (3)\} = \{C, D\}$
14	13	sseq1d	$⊢ (P (2) = C \land P (3) = D) \to (\{P (2), P (3)\} \subseteq I (L) \leftrightarrow \{C, D\} \subseteq I (L))$
15	14	adantl	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (\{P (2), P (3)\} \subseteq I (L) \leftrightarrow \{C, D\} \subseteq I (L))$
16	9 12 15	3anbi123d	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to ((\{P (0), P (1)\} \subseteq I (J) \land \{P (1), P (2)\} \subseteq I (K) \land \{P (2), P (3)\} \subseteq I (L)) \leftrightarrow (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K) \land \{C, D\} \subseteq I (L)))$
17	5 16	syl5ibrcom	$⊢ φ \to (((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (\{P (0), P (1)\} \subseteq I (J) \land \{P (1), P (2)\} \subseteq I (K) \land \{P (2), P (3)\} \subseteq I (L)))$
18	6 17	mpd	$⊢ φ \to (\{P (0), P (1)\} \subseteq I (J) \land \{P (1), P (2)\} \subseteq I (K) \land \{P (2), P (3)\} \subseteq I (L))$
19		fvex	$⊢ P (0) \in V$
20		fvex	$⊢ P (1) \in V$
21	19 20	prss	$⊢ (P (0) \in I (J) \land P (1) \in I (J)) \leftrightarrow \{P (0), P (1)\} \subseteq I (J)$
22		simpl	$⊢ (P (0) \in I (J) \land P (1) \in I (J)) \to P (0) \in I (J)$
23	21 22	sylbir	$⊢ \{P (0), P (1)\} \subseteq I (J) \to P (0) \in I (J)$
24		fvex	$⊢ P (2) \in V$
25	20 24	prss	$⊢ (P (1) \in I (K) \land P (2) \in I (K)) \leftrightarrow \{P (1), P (2)\} \subseteq I (K)$
26		simpl	$⊢ (P (1) \in I (K) \land P (2) \in I (K)) \to P (1) \in I (K)$
27	25 26	sylbir	$⊢ \{P (1), P (2)\} \subseteq I (K) \to P (1) \in I (K)$
28		fvex	$⊢ P (3) \in V$
29	24 28	prss	$⊢ (P (2) \in I (L) \land P (3) \in I (L)) \leftrightarrow \{P (2), P (3)\} \subseteq I (L)$
30		simpl	$⊢ (P (2) \in I (L) \land P (3) \in I (L)) \to P (2) \in I (L)$
31	29 30	sylbir	$⊢ \{P (2), P (3)\} \subseteq I (L) \to P (2) \in I (L)$
32	23 27 31	3anim123i	$⊢ (\{P (0), P (1)\} \subseteq I (J) \land \{P (1), P (2)\} \subseteq I (K) \land \{P (2), P (3)\} \subseteq I (L)) \to (P (0) \in I (J) \land P (1) \in I (K) \land P (2) \in I (L))$
33	18 32	syl	$⊢ φ \to (P (0) \in I (J) \land P (1) \in I (K) \land P (2) \in I (L))$
34		eleq1	$⊢ P (0) = A \to (P (0) \in I (J) \leftrightarrow A \in I (J))$
35	34	adantr	$⊢ (P (0) = A \land P (1) = B) \to (P (0) \in I (J) \leftrightarrow A \in I (J))$
36	35	adantr	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (P (0) \in I (J) \leftrightarrow A \in I (J))$
37		eleq1	$⊢ P (1) = B \to (P (1) \in I (K) \leftrightarrow B \in I (K))$
38	37	adantl	$⊢ (P (0) = A \land P (1) = B) \to (P (1) \in I (K) \leftrightarrow B \in I (K))$
39	38	adantr	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (P (1) \in I (K) \leftrightarrow B \in I (K))$
40		eleq1	$⊢ P (2) = C \to (P (2) \in I (L) \leftrightarrow C \in I (L))$
41	40	adantr	$⊢ (P (2) = C \land P (3) = D) \to (P (2) \in I (L) \leftrightarrow C \in I (L))$
42	41	adantl	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to (P (2) \in I (L) \leftrightarrow C \in I (L))$
43	36 39 42	3anbi123d	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to ((P (0) \in I (J) \land P (1) \in I (K) \land P (2) \in I (L)) \leftrightarrow (A \in I (J) \land B \in I (K) \land C \in I (L)))$
44	43	bicomd	$⊢ ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D)) \to ((A \in I (J) \land B \in I (K) \land C \in I (L)) \leftrightarrow (P (0) \in I (J) \land P (1) \in I (K) \land P (2) \in I (L)))$
45	6 44	syl	$⊢ φ \to ((A \in I (J) \land B \in I (K) \land C \in I (L)) \leftrightarrow (P (0) \in I (J) \land P (1) \in I (K) \land P (2) \in I (L)))$
46	33 45	mpbird	$⊢ φ \to (A \in I (J) \land B \in I (K) \land C \in I (L))$

Metamath Proof Explorer

Theorem 3wlkdlem6

Proof