upgrimpths

Description: Graph isomorphisms between simple pseudographs map paths onto paths. (Contributed by AV, 31-Oct-2025)

	Ref	Expression
Hypotheses	upgrimwlk.i	$⊢ I = iEdg (G)$
	upgrimwlk.j	$⊢ J = iEdg (H)$
	upgrimwlk.g	$⊢ φ \to G \in USHGraph$
	upgrimwlk.h	$⊢ φ \to H \in USHGraph$
	upgrimwlk.n	$⊢ φ \to N \in (G GraphIso H)$
	upgrimwlk.e	$⊢ E = (x \in dom F ⟼ J^{-1} (N [I (F (x))]))$
	upgrimpths.p	$⊢ φ \to F Paths (G) P$
Assertion	upgrimpths	$⊢ φ \to E Paths (H) (N \circ P)$

Proof

Step	Hyp	Ref	Expression
1		upgrimwlk.i	$⊢ I = iEdg (G)$
2		upgrimwlk.j	$⊢ J = iEdg (H)$
3		upgrimwlk.g	$⊢ φ \to G \in USHGraph$
4		upgrimwlk.h	$⊢ φ \to H \in USHGraph$
5		upgrimwlk.n	$⊢ φ \to N \in (G GraphIso H)$
6		upgrimwlk.e	$⊢ E = (x \in dom F ⟼ J^{-1} (N [I (F (x))]))$
7		upgrimpths.p	$⊢ φ \to F Paths (G) P$
8		pthistrl	$⊢ F Paths (G) P \to F Trails (G) P$
9	7 8	syl	$⊢ φ \to F Trails (G) P$
10	1 2 3 4 5 6 9	upgrimtrls	$⊢ φ \to E Trails (H) (N \circ P)$
11	1 2 3 4 5 6 7	upgrimpthslem1	$⊢ φ \to Fun {({(N \circ P) ↾}_{(1 ..^\|F\|)})}^{-1}$
12		pthiswlk	$⊢ F Paths (G) P \to F Walks (G) P$
13	1	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
14	7 12 13	3syl	$⊢ φ \to F \in Word dom I$
15		eqid	$⊢ Vtx (G) = Vtx (G)$
16	15	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
17	7 12 16	3syl	$⊢ φ \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
18	1 2 3 4 5 6 14 17	upgrimwlklem4	$⊢ φ \to (N \circ P) : (0 \dots \|E\|) ⟶ Vtx (H)$
19	18	ffnd	$⊢ φ \to (N \circ P) Fn (0 \dots \|E\|)$
20	1 2 3 4 5 6 14	upgrimwlklem1	$⊢ φ \to \|E\| = \|F\|$
21		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
22	7 12 21	3syl	$⊢ φ \to \|F\| \in ℕ_{0}$
23	20 22	eqeltrd	$⊢ φ \to \|E\| \in ℕ_{0}$
24		0elfz	$⊢ \|E\| \in ℕ_{0} \to 0 \in (0 \dots \|E\|)$
25	23 24	syl	$⊢ φ \to 0 \in (0 \dots \|E\|)$
26		nn0fz0	$⊢ \|F\| \in ℕ_{0} \leftrightarrow \|F\| \in (0 \dots \|F\|)$
27	22 26	sylib	$⊢ φ \to \|F\| \in (0 \dots \|F\|)$
28	20	oveq2d	$⊢ φ \to (0 \dots \|E\|) = (0 \dots \|F\|)$
29	27 28	eleqtrrd	$⊢ φ \to \|F\| \in (0 \dots \|E\|)$
30		fnimapr	$⊢ ((N \circ P) Fn (0 \dots \|E\|) \land 0 \in (0 \dots \|E\|) \land \|F\| \in (0 \dots \|E\|)) \to (N \circ P) [\{0, \|F\|\}] = \{(N \circ P) (0), (N \circ P) (\|F\|)\}$
31	19 25 29 30	syl3anc	$⊢ φ \to (N \circ P) [\{0, \|F\|\}] = \{(N \circ P) (0), (N \circ P) (\|F\|)\}$
32	31	eleq2d	$⊢ φ \to (x \in (N \circ P) [\{0, \|F\|\}] \leftrightarrow x \in \{(N \circ P) (0), (N \circ P) (\|F\|)\})$
33		vex	$⊢ x \in V$
34	33	elpr	$⊢ x \in \{(N \circ P) (0), (N \circ P) (\|F\|)\} \leftrightarrow (x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|))$
35	32 34	bitrdi	$⊢ φ \to (x \in (N \circ P) [\{0, \|F\|\}] \leftrightarrow (x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|)))$
36	1 2 3 4 5 6 7	upgrimpthslem2	$⊢ (φ \land y \in (1 ..^\|F\|)) \to (\neg (N \circ P) (y) = (N \circ P) (0) \land \neg (N \circ P) (y) = (N \circ P) (\|F\|))$
37	36	simpld	$⊢ (φ \land y \in (1 ..^\|F\|)) \to \neg (N \circ P) (y) = (N \circ P) (0)$
38		eqeq2	$⊢ x = (N \circ P) (0) \to ((N \circ P) (y) = x \leftrightarrow (N \circ P) (y) = (N \circ P) (0))$
39	38	notbid	$⊢ x = (N \circ P) (0) \to (\neg (N \circ P) (y) = x \leftrightarrow \neg (N \circ P) (y) = (N \circ P) (0))$
40	37 39	syl5ibrcom	$⊢ (φ \land y \in (1 ..^\|F\|)) \to (x = (N \circ P) (0) \to \neg (N \circ P) (y) = x)$
41	36	simprd	$⊢ (φ \land y \in (1 ..^\|F\|)) \to \neg (N \circ P) (y) = (N \circ P) (\|F\|)$
42		eqeq2	$⊢ x = (N \circ P) (\|F\|) \to ((N \circ P) (y) = x \leftrightarrow (N \circ P) (y) = (N \circ P) (\|F\|))$
43	42	notbid	$⊢ x = (N \circ P) (\|F\|) \to (\neg (N \circ P) (y) = x \leftrightarrow \neg (N \circ P) (y) = (N \circ P) (\|F\|))$
44	41 43	syl5ibrcom	$⊢ (φ \land y \in (1 ..^\|F\|)) \to (x = (N \circ P) (\|F\|) \to \neg (N \circ P) (y) = x)$
45	40 44	jaod	$⊢ (φ \land y \in (1 ..^\|F\|)) \to ((x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|)) \to \neg (N \circ P) (y) = x)$
46	45	impancom	$⊢ (φ \land (x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|))) \to (y \in (1 ..^\|F\|) \to \neg (N \circ P) (y) = x)$
47	46	imp	$⊢ ((φ \land (x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|))) \land y \in (1 ..^\|F\|)) \to \neg (N \circ P) (y) = x$
48	47	nrexdv	$⊢ (φ \land (x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|))) \to \neg \exists y \in (1 ..^\|F\|) (N \circ P) (y) = x$
49	20	eqcomd	$⊢ φ \to \|F\| = \|E\|$
50	49	oveq2d	$⊢ φ \to (0 \dots \|F\|) = (0 \dots \|E\|)$
51	50	feq2d	$⊢ φ \to ((N \circ P) : (0 \dots \|F\|) ⟶ Vtx (H) \leftrightarrow (N \circ P) : (0 \dots \|E\|) ⟶ Vtx (H))$
52	18 51	mpbird	$⊢ φ \to (N \circ P) : (0 \dots \|F\|) ⟶ Vtx (H)$
53	52	ffnd	$⊢ φ \to (N \circ P) Fn (0 \dots \|F\|)$
54	53	adantr	$⊢ (φ \land (x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|))) \to (N \circ P) Fn (0 \dots \|F\|)$
55		fzo0ss1	$⊢ (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
56		fzossfz	$⊢ (0 ..^\|F\|) \subseteq (0 \dots \|F\|)$
57	55 56	sstri	$⊢ (1 ..^\|F\|) \subseteq (0 \dots \|F\|)$
58	57	a1i	$⊢ (φ \land (x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|))) \to (1 ..^\|F\|) \subseteq (0 \dots \|F\|)$
59	54 58	fvelimabd	$⊢ (φ \land (x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|))) \to (x \in (N \circ P) [(1 ..^\|F\|)] \leftrightarrow \exists y \in (1 ..^\|F\|) (N \circ P) (y) = x)$
60	48 59	mtbird	$⊢ (φ \land (x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|))) \to \neg x \in (N \circ P) [(1 ..^\|F\|)]$
61	60	ex	$⊢ φ \to ((x = (N \circ P) (0) \lor x = (N \circ P) (\|F\|)) \to \neg x \in (N \circ P) [(1 ..^\|F\|)])$
62	35 61	sylbid	$⊢ φ \to (x \in (N \circ P) [\{0, \|F\|\}] \to \neg x \in (N \circ P) [(1 ..^\|F\|)])$
63	62	ralrimiv	$⊢ φ \to \forall x \in (N \circ P) [\{0, \|F\|\}] \neg x \in (N \circ P) [(1 ..^\|F\|)]$
64		disj	$⊢ (N \circ P) [\{0, \|F\|\}] \cap (N \circ P) [(1 ..^\|F\|)] = \emptyset \leftrightarrow \forall x \in (N \circ P) [\{0, \|F\|\}] \neg x \in (N \circ P) [(1 ..^\|F\|)]$
65	63 64	sylibr	$⊢ φ \to (N \circ P) [\{0, \|F\|\}] \cap (N \circ P) [(1 ..^\|F\|)] = \emptyset$
66	20	oveq2d	$⊢ φ \to (1 ..^\|E\|) = (1 ..^\|F\|)$
67	66	reseq2d	$⊢ φ \to {(N \circ P) ↾}_{(1 ..^\|E\|)} = {(N \circ P) ↾}_{(1 ..^\|F\|)}$
68	67	cnveqd	$⊢ φ \to {({(N \circ P) ↾}_{(1 ..^\|E\|)})}^{-1} = {({(N \circ P) ↾}_{(1 ..^\|F\|)})}^{-1}$
69	68	funeqd	$⊢ φ \to (Fun {({(N \circ P) ↾}_{(1 ..^\|E\|)})}^{-1} \leftrightarrow Fun {({(N \circ P) ↾}_{(1 ..^\|F\|)})}^{-1})$
70		preq2	$⊢ \|E\| = \|F\| \to \{0, \|E\|\} = \{0, \|F\|\}$
71	70	imaeq2d	$⊢ \|E\| = \|F\| \to (N \circ P) [\{0, \|E\|\}] = (N \circ P) [\{0, \|F\|\}]$
72		oveq2	$⊢ \|E\| = \|F\| \to (1 ..^\|E\|) = (1 ..^\|F\|)$
73	72	imaeq2d	$⊢ \|E\| = \|F\| \to (N \circ P) [(1 ..^\|E\|)] = (N \circ P) [(1 ..^\|F\|)]$
74	71 73	ineq12d	$⊢ \|E\| = \|F\| \to (N \circ P) [\{0, \|E\|\}] \cap (N \circ P) [(1 ..^\|E\|)] = (N \circ P) [\{0, \|F\|\}] \cap (N \circ P) [(1 ..^\|F\|)]$
75	74	eqeq1d	$⊢ \|E\| = \|F\| \to ((N \circ P) [\{0, \|E\|\}] \cap (N \circ P) [(1 ..^\|E\|)] = \emptyset \leftrightarrow (N \circ P) [\{0, \|F\|\}] \cap (N \circ P) [(1 ..^\|F\|)] = \emptyset)$
76	20 75	syl	$⊢ φ \to ((N \circ P) [\{0, \|E\|\}] \cap (N \circ P) [(1 ..^\|E\|)] = \emptyset \leftrightarrow (N \circ P) [\{0, \|F\|\}] \cap (N \circ P) [(1 ..^\|F\|)] = \emptyset)$
77	69 76	3anbi23d	$⊢ φ \to ((E Trails (H) (N \circ P) \land Fun {({(N \circ P) ↾}_{(1 ..^\|E\|)})}^{-1} \land (N \circ P) [\{0, \|E\|\}] \cap (N \circ P) [(1 ..^\|E\|)] = \emptyset) \leftrightarrow (E Trails (H) (N \circ P) \land Fun {({(N \circ P) ↾}_{(1 ..^\|F\|)})}^{-1} \land (N \circ P) [\{0, \|F\|\}] \cap (N \circ P) [(1 ..^\|F\|)] = \emptyset))$
78	10 11 65 77	mpbir3and	$⊢ φ \to (E Trails (H) (N \circ P) \land Fun {({(N \circ P) ↾}_{(1 ..^\|E\|)})}^{-1} \land (N \circ P) [\{0, \|E\|\}] \cap (N \circ P) [(1 ..^\|E\|)] = \emptyset)$
79		ispth	$⊢ E Paths (H) (N \circ P) \leftrightarrow (E Trails (H) (N \circ P) \land Fun {({(N \circ P) ↾}_{(1 ..^\|E\|)})}^{-1} \land (N \circ P) [\{0, \|E\|\}] \cap (N \circ P) [(1 ..^\|E\|)] = \emptyset)$
80	78 79	sylibr	$⊢ φ \to E Paths (H) (N \circ P)$

Metamath Proof Explorer

Theorem upgrimpths

Proof