numclwwlk1lem2fo

Description: T is an onto function. (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 13-Feb-2022) (Revised by AV, 31-Oct-2022)

	Ref	Expression
Hypotheses	extwwlkfab.v	$⊢ V = Vtx (G)$
	extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
	extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
	numclwwlk.t	$⊢ T = (u \in (X C N) ⟼ ⟨u prefix (N - 2), u (N - 1)⟩)$
Assertion	numclwwlk1lem2fo	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N \underset{onto}{⟶} F \times (G NeighbVtx X)$

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	$⊢ V = Vtx (G)$
2		extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
3		extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
4		numclwwlk.t	$⊢ T = (u \in (X C N) ⟼ ⟨u prefix (N - 2), u (N - 1)⟩)$
5	1 2 3 4	numclwwlk1lem2f	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N ⟶ F \times (G NeighbVtx X)$
6		elxp	$⊢ p \in (F \times (G NeighbVtx X)) \leftrightarrow \exists a \exists b (p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X)))$
7	1 2 3	numclwwlk1lem2foa	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((a \in F \land b \in (G NeighbVtx X)) \to (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N))$
8	7	com12	$⊢ (a \in F \land b \in (G NeighbVtx X)) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N))$
9	8	adantl	$⊢ (p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N))$
10	9	imp	$⊢ ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \to (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N)$
11		simpl	$⊢ ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N) \land ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}))) \to (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N)$
12		fveq2	$⊢ x = (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \to T (x) = T ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩)$
13	12	eqeq2d	$⊢ x = (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \to (p = T (x) \leftrightarrow p = T ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩))$
14	1 2 3 4	numclwwlk1lem2fv	$⊢ (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N) \to T ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩$
15	14	adantr	$⊢ ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N) \land ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}))) \to T ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩$
16	15	eqeq2d	$⊢ ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N) \land ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}))) \to (p = T ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) \leftrightarrow p = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩)$
17	13 16	sylan9bbr	$⊢ (((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N) \land ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}))) \land x = (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) \to (p = T (x) \leftrightarrow p = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩)$
18		simprll	$⊢ ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N) \land ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}))) \to p = ⟨a, b⟩$
19	1	nbgrisvtx	$⊢ b \in (G NeighbVtx X) \to b \in V$
20	3	eleq2i	$⊢ a \in F \leftrightarrow a \in (X ClWWalksNOn (G) (N - 2))$
21		uz3m2nn	$⊢ N \in ℤ_{\geq 3} \to N - 2 \in ℕ$
22	21	nnne0d	$⊢ N \in ℤ_{\geq 3} \to N - 2 \neq 0$
23	22	3ad2ant3	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to N - 2 \neq 0$
24		eqid	$⊢ Edg (G) = Edg (G)$
25	1 24	clwwlknonel	$⊢ N - 2 \neq 0 \to (a \in (X ClWWalksNOn (G) (N - 2)) \leftrightarrow ((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2 \land a (0) = X))$
26	23 25	syl	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (a \in (X ClWWalksNOn (G) (N - 2)) \leftrightarrow ((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2 \land a (0) = X))$
27	20 26	syl5bb	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (a \in F \leftrightarrow ((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2 \land a (0) = X))$
28		df-3an	$⊢ ((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2 \land a (0) = X) \leftrightarrow (((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2) \land a (0) = X)$
29	27 28	bitrdi	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (a \in F \leftrightarrow (((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2) \land a (0) = X))$
30		simplll	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to a \in Word V$
31		s1cl	$⊢ X \in V \to ⟨“ X ”⟩ \in Word V$
32	31	adantr	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to ⟨“ X ”⟩ \in Word V$
33	32	adantl	$⊢ ((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \to ⟨“ X ”⟩ \in Word V$
34	33	adantr	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to ⟨“ X ”⟩ \in Word V$
35		s1cl	$⊢ b \in V \to ⟨“ b ”⟩ \in Word V$
36	35	adantl	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to ⟨“ b ”⟩ \in Word V$
37		ccatass	$⊢ (a \in Word V \land ⟨“ X ”⟩ \in Word V \land ⟨“ b ”⟩ \in Word V) \to (a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ = a ++ (⟨“ X ”⟩ ++ ⟨“ b ”⟩)$
38	37	oveq1d	$⊢ (a \in Word V \land ⟨“ X ”⟩ \in Word V \land ⟨“ b ”⟩ \in Word V) \to ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2) = (a ++ (⟨“ X ”⟩ ++ ⟨“ b ”⟩)) prefix (N - 2)$
39	30 34 36 38	syl3anc	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2) = (a ++ (⟨“ X ”⟩ ++ ⟨“ b ”⟩)) prefix (N - 2)$
40		ccatcl	$⊢ (⟨“ X ”⟩ \in Word V \land ⟨“ b ”⟩ \in Word V) \to ⟨“ X ”⟩ ++ ⟨“ b ”⟩ \in Word V$
41	33 35 40	syl2an	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to ⟨“ X ”⟩ ++ ⟨“ b ”⟩ \in Word V$
42		simpr	$⊢ (a \in Word V \land \|a\| = N - 2) \to \|a\| = N - 2$
43	42	eqcomd	$⊢ (a \in Word V \land \|a\| = N - 2) \to N - 2 = \|a\|$
44	43	adantr	$⊢ ((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \to N - 2 = \|a\|$
45	44	adantr	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to N - 2 = \|a\|$
46		pfxccatid	$⊢ (a \in Word V \land ⟨“ X ”⟩ ++ ⟨“ b ”⟩ \in Word V \land N - 2 = \|a\|) \to (a ++ (⟨“ X ”⟩ ++ ⟨“ b ”⟩)) prefix (N - 2) = a$
47	30 41 45 46	syl3anc	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to (a ++ (⟨“ X ”⟩ ++ ⟨“ b ”⟩)) prefix (N - 2) = a$
48	39 47	eqtr2d	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to a = ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2)$
49		1e2m1	$⊢ 1 = 2 - 1$
50	49	a1i	$⊢ N \in ℤ_{\geq 3} \to 1 = 2 - 1$
51	50	oveq2d	$⊢ N \in ℤ_{\geq 3} \to N - 1 = N - (2 - 1)$
52		eluzelcn	$⊢ N \in ℤ_{\geq 3} \to N \in ℂ$
53		2cnd	$⊢ N \in ℤ_{\geq 3} \to 2 \in ℂ$
54		1cnd	$⊢ N \in ℤ_{\geq 3} \to 1 \in ℂ$
55	52 53 54	subsubd	$⊢ N \in ℤ_{\geq 3} \to N - (2 - 1) = N - 2 + 1$
56	51 55	eqtrd	$⊢ N \in ℤ_{\geq 3} \to N - 1 = N - 2 + 1$
57	56	adantl	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to N - 1 = N - 2 + 1$
58	57	adantl	$⊢ ((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \to N - 1 = N - 2 + 1$
59	58	adantr	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to N - 1 = N - 2 + 1$
60	59	fveq2d	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1) = ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 2 + 1)$
61		simpll	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to (a \in Word V \land \|a\| = N - 2)$
62		simprl	$⊢ ((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \to X \in V$
63	62	anim1i	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to (X \in V \land b \in V)$
64		ccatw2s1p2	$⊢ ((a \in Word V \land \|a\| = N - 2) \land (X \in V \land b \in V)) \to ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 2 + 1) = b$
65	61 63 64	syl2anc	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 2 + 1) = b$
66	60 65	eqtr2d	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to b = ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)$
67	48 66	opeq12d	$⊢ (((a \in Word V \land \|a\| = N - 2) \land (X \in V \land N \in ℤ_{\geq 3})) \land b \in V) \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩$
68	67	exp31	$⊢ (a \in Word V \land \|a\| = N - 2) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (b \in V \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩))$
69	68	3ad2antl1	$⊢ ((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (b \in V \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩))$
70	69	adantr	$⊢ (((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2) \land a (0) = X) \to ((X \in V \land N \in ℤ_{\geq 3}) \to (b \in V \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩))$
71	70	com12	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to ((((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2) \land a (0) = X) \to (b \in V \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩))$
72	71	3adant1	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((((a \in Word V \land \forall i \in (0 ..^\|a\| - 1) \{a (i), a (i + 1)\} \in Edg (G) \land \{lastS (a), a (0)\} \in Edg (G)) \land \|a\| = N - 2) \land a (0) = X) \to (b \in V \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩))$
73	29 72	sylbid	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (a \in F \to (b \in V \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩))$
74	73	com23	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (b \in V \to (a \in F \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩))$
75	19 74	syl5	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to (b \in (G NeighbVtx X) \to (a \in F \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩))$
76	75	com13	$⊢ a \in F \to (b \in (G NeighbVtx X) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩))$
77	76	imp	$⊢ (a \in F \land b \in (G NeighbVtx X)) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩)$
78	77	adantl	$⊢ (p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩)$
79	78	imp	$⊢ ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩$
80	79	adantl	$⊢ ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N) \land ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}))) \to ⟨a, b⟩ = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩$
81	18 80	eqtrd	$⊢ ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N) \land ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}))) \to p = ⟨((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) prefix (N - 2), ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩) (N - 1)⟩$
82	11 17 81	rspcedvd	$⊢ ((a ++ ⟨“ X ”⟩) ++ ⟨“ b ”⟩ \in (X C N) \land ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}))) \to \exists x \in (X C N) p = T (x)$
83	10 82	mpancom	$⊢ ((p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \land (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3})) \to \exists x \in (X C N) p = T (x)$
84	83	ex	$⊢ (p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to \exists x \in (X C N) p = T (x))$
85	84	exlimivv	$⊢ \exists a \exists b (p = ⟨a, b⟩ \land (a \in F \land b \in (G NeighbVtx X))) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to \exists x \in (X C N) p = T (x))$
86	6 85	sylbi	$⊢ p \in (F \times (G NeighbVtx X)) \to ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to \exists x \in (X C N) p = T (x))$
87	86	impcom	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land p \in (F \times (G NeighbVtx X))) \to \exists x \in (X C N) p = T (x)$
88	87	ralrimiva	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to \forall p \in (F \times (G NeighbVtx X)) \exists x \in (X C N) p = T (x)$
89		dffo3	$⊢ T : X C N \underset{onto}{⟶} F \times (G NeighbVtx X) \leftrightarrow (T : X C N ⟶ F \times (G NeighbVtx X) \land \forall p \in (F \times (G NeighbVtx X)) \exists x \in (X C N) p = T (x))$
90	5 88 89	sylanbrc	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N \underset{onto}{⟶} F \times (G NeighbVtx X)$

Metamath Proof Explorer

Theorem numclwwlk1lem2fo

Proof