wlkp1lem4

	Ref	Expression
Hypotheses	wlkp1.v	$⊢ V = Vtx (G)$
	wlkp1.i	$⊢ I = iEdg (G)$
	wlkp1.f	$⊢ φ \to Fun I$
	wlkp1.a	$⊢ φ \to I \in Fin$
	wlkp1.b	$⊢ φ \to B \in W$
	wlkp1.c	$⊢ φ \to C \in V$
	wlkp1.d	$⊢ φ \to \neg B \in dom I$
	wlkp1.w	$⊢ φ \to F Walks (G) P$
	wlkp1.n	$⊢ N = \|F\|$
	wlkp1.e	$⊢ φ \to E \in Edg (G)$
	wlkp1.x	$⊢ φ \to \{P (N), C\} \subseteq E$
	wlkp1.u	$⊢ φ \to iEdg (S) = I \cup \{⟨B, E⟩\}$
	wlkp1.h	$⊢ H = F \cup \{⟨N, B⟩\}$
	wlkp1.q	$⊢ Q = P \cup \{⟨N + 1, C⟩\}$
	wlkp1.s	$⊢ φ \to Vtx (S) = V$
Assertion	wlkp1lem4	$⊢ φ \to (S \in V \land H \in V \land Q \in V)$

Proof

Step	Hyp	Ref	Expression
1		wlkp1.v	$⊢ V = Vtx (G)$
2		wlkp1.i	$⊢ I = iEdg (G)$
3		wlkp1.f	$⊢ φ \to Fun I$
4		wlkp1.a	$⊢ φ \to I \in Fin$
5		wlkp1.b	$⊢ φ \to B \in W$
6		wlkp1.c	$⊢ φ \to C \in V$
7		wlkp1.d	$⊢ φ \to \neg B \in dom I$
8		wlkp1.w	$⊢ φ \to F Walks (G) P$
9		wlkp1.n	$⊢ N = \|F\|$
10		wlkp1.e	$⊢ φ \to E \in Edg (G)$
11		wlkp1.x	$⊢ φ \to \{P (N), C\} \subseteq E$
12		wlkp1.u	$⊢ φ \to iEdg (S) = I \cup \{⟨B, E⟩\}$
13		wlkp1.h	$⊢ H = F \cup \{⟨N, B⟩\}$
14		wlkp1.q	$⊢ Q = P \cup \{⟨N + 1, C⟩\}$
15		wlkp1.s	$⊢ φ \to Vtx (S) = V$
16		eqid	$⊢ iEdg (G) = iEdg (G)$
17	16	wlkf	$⊢ F Walks (G) P \to F \in Word dom iEdg (G)$
18		eqid	$⊢ Vtx (G) = Vtx (G)$
19	18	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
20	17 19	jca	$⊢ F Walks (G) P \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))$
21	8 20	syl	$⊢ φ \to (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))$
22	6 15	eleqtrrd	$⊢ φ \to C \in Vtx (S)$
23	22	elfvexd	$⊢ φ \to S \in V$
24	23	adantr	$⊢ (φ \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))) \to S \in V$
25		simprl	$⊢ (φ \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))) \to F \in Word dom iEdg (G)$
26		snex	$⊢ \{⟨N, B⟩\} \in V$
27		unexg	$⊢ (F \in Word dom iEdg (G) \land \{⟨N, B⟩\} \in V) \to F \cup \{⟨N, B⟩\} \in V$
28	25 26 27	sylancl	$⊢ (φ \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))) \to F \cup \{⟨N, B⟩\} \in V$
29	13 28	eqeltrid	$⊢ (φ \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))) \to H \in V$
30		ovex	$⊢ (0 \dots \|F\|) \in V$
31		fvex	$⊢ Vtx (G) \in V$
32	30 31	fpm	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to P \in (Vtx (G) ↑_{𝑝𝑚} (0 \dots \|F\|))$
33	32	ad2antll	$⊢ (φ \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))) \to P \in (Vtx (G) ↑_{𝑝𝑚} (0 \dots \|F\|))$
34		snex	$⊢ \{⟨N + 1, C⟩\} \in V$
35		unexg	$⊢ (P \in (Vtx (G) ↑_{𝑝𝑚} (0 \dots \|F\|)) \land \{⟨N + 1, C⟩\} \in V) \to P \cup \{⟨N + 1, C⟩\} \in V$
36	33 34 35	sylancl	$⊢ (φ \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))) \to P \cup \{⟨N + 1, C⟩\} \in V$
37	14 36	eqeltrid	$⊢ (φ \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))) \to Q \in V$
38	24 29 37	3jca	$⊢ (φ \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G))) \to (S \in V \land H \in V \land Q \in V)$
39	21 38	mpdan	$⊢ φ \to (S \in V \land H \in V \land Q \in V)$

Metamath Proof Explorer

Theorem wlkp1lem4

Proof