dfpth2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dfpth2		Structured version Visualization version GIF version

Theorem dfpth2 30044

Description: Alternate definition for a pair of classes/functions to be a path (in an undirected graph). (Contributed by AV, 4-Oct-2025.)

**Assertion**
Ref	Expression
dfpth2	⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))))

Proof of Theorem dfpth2 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ispth 30036	. 2 ⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅))
2		istrl 30010	. . . . . . . . . . 11 ⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ^◡𝐹))
3		wlkcl 29931	. . . . . . . . . . . . 13 ⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ₀)
4		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
5	4	wlkp 29932	. . . . . . . . . . . . 13 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺))
6		ffn 6705	. . . . . . . . . . . . . . 15 ⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → 𝑃 Fn (0...(♯‘𝐹)))
7	6	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → 𝑃 Fn (0...(♯‘𝐹)))
8		0elfz 13651	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) ∈ ℕ₀ → 0 ∈ (0...(♯‘𝐹)))
9	8	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → 0 ∈ (0...(♯‘𝐹)))
10		nn0fz0 13652	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) ∈ ℕ₀ ↔ (♯‘𝐹) ∈ (0...(♯‘𝐹)))
11	10	birani 508	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (♯‘𝐹) ∈ (0...(♯‘𝐹)))
12	7, 9, 11	3jca 1144	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (𝑃 Fn (0...(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ (♯‘𝐹) ∈ (0...(♯‘𝐹))))
13	3, 5, 12	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝑃 Fn (0...(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ (♯‘𝐹) ∈ (0...(♯‘𝐹))))
14	13	adantr 485	. . . . . . . . . . 11 ⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ Fun ^◡𝐹) → (𝑃 Fn (0...(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ (♯‘𝐹) ∈ (0...(♯‘𝐹))))
15	2, 14	sylbi 220	. . . . . . . . . 10 ⊢ (𝐹(Trails‘𝐺)𝑃 → (𝑃 Fn (0...(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ (♯‘𝐹) ∈ (0...(♯‘𝐹))))
16		fnimapr 6964	. . . . . . . . . 10 ⊢ ((𝑃 Fn (0...(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹)) ∧ (♯‘𝐹) ∈ (0...(♯‘𝐹))) → (𝑃 “ {0, (♯‘𝐹)}) = {(𝑃‘0), (𝑃‘(♯‘𝐹))})
17	15, 16	syl 18	. . . . . . . . 9 ⊢ (𝐹(Trails‘𝐺)𝑃 → (𝑃 “ {0, (♯‘𝐹)}) = {(𝑃‘0), (𝑃‘(♯‘𝐹))})
18	17	ineq1d 4171	. . . . . . . 8 ⊢ (𝐹(Trails‘𝐺)𝑃 → ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ({(𝑃‘0), (𝑃‘(♯‘𝐹))} ∩ (𝑃 “ (1..^(♯‘𝐹)))))
19	18	eqeq1d 2763	. . . . . . 7 ⊢ (𝐹(Trails‘𝐺)𝑃 → (((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅ ↔ ({(𝑃‘0), (𝑃‘(♯‘𝐹))} ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅))
20		disj 4409	. . . . . . . 8 ⊢ (({(𝑃‘0), (𝑃‘(♯‘𝐹))} ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅ ↔ ∀𝑥 ∈ {(𝑃‘0), (𝑃‘(♯‘𝐹))} ¬ 𝑥 ∈ (𝑃 “ (1..^(♯‘𝐹))))
21		fvex 6894	. . . . . . . . . 10 ⊢ (𝑃‘0) ∈ V
22		fvex 6894	. . . . . . . . . 10 ⊢ (𝑃‘(♯‘𝐹)) ∈ V
23		eleq1 2849	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑃‘0) → (𝑥 ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ (𝑃‘0) ∈ (𝑃 “ (1..^(♯‘𝐹)))))
24	23	notbid 321	. . . . . . . . . 10 ⊢ (𝑥 = (𝑃‘0) → (¬ 𝑥 ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ ¬ (𝑃‘0) ∈ (𝑃 “ (1..^(♯‘𝐹)))))
25		eleq1 2849	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑃‘(♯‘𝐹)) → (𝑥 ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))))
26	25	notbid 321	. . . . . . . . . 10 ⊢ (𝑥 = (𝑃‘(♯‘𝐹)) → (¬ 𝑥 ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))))
27	21, 22, 24, 26	ralpr 4665	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {(𝑃‘0), (𝑃‘(♯‘𝐹))} ¬ 𝑥 ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ (¬ (𝑃‘0) ∈ (𝑃 “ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))))
28		df-nel 3063	. . . . . . . . . 10 ⊢ ((𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))) ↔ ¬ (𝑃‘0) ∈ (𝑃 “ (1..^(♯‘𝐹))))
29	28	bicomi 227	. . . . . . . . 9 ⊢ (¬ (𝑃‘0) ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))))
30	27, 29	bianbi 638	. . . . . . . 8 ⊢ (∀𝑥 ∈ {(𝑃‘0), (𝑃‘(♯‘𝐹))} ¬ 𝑥 ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))))
31	20, 30	bitri 278	. . . . . . 7 ⊢ (({(𝑃‘0), (𝑃‘(♯‘𝐹))} ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅ ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))))
32	19, 31	bitrdi 290	. . . . . 6 ⊢ (𝐹(Trails‘𝐺)𝑃 → (((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅ ↔ ((𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹))))))
33	32	anbi2d 641	. . . . 5 ⊢ (𝐹(Trails‘𝐺)𝑃 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅) ↔ (Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))))))
34		ancom 465	. . . . . . 7 ⊢ (((𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ (¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))))
35	34	bianass 654	. . . . . 6 ⊢ ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹))))) ↔ ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))))
36	35	a1i 11	. . . . 5 ⊢ (𝐹(Trails‘𝐺)𝑃 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹))))) ↔ ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))))))
37		noel 4290	. . . . . . . . . . . 12 ⊢ ¬ (𝑃‘(♯‘𝐹)) ∈ ∅
38	37	biantru 538	. . . . . . . . . . 11 ⊢ (Fun ^◡(𝑃 ↾ ∅) ↔ (Fun ^◡(𝑃 ↾ ∅) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ ∅))
39	38	bicomi 227	. . . . . . . . . 10 ⊢ ((Fun ^◡(𝑃 ↾ ∅) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ ∅) ↔ Fun ^◡(𝑃 ↾ ∅))
40	39	a1i 11	. . . . . . . . 9 ⊢ ((♯‘𝐹) = 0 → ((Fun ^◡(𝑃 ↾ ∅) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ ∅) ↔ Fun ^◡(𝑃 ↾ ∅)))
41		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) = 0 → (1..^(♯‘𝐹)) = (1..^0))
42		0le1 11736	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
43		1z 12623	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℤ
44		0z 12601	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℤ
45		fzon 13708	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℤ ∧ 0 ∈ ℤ) → (0 ≤ 1 ↔ (1..^0) = ∅))
46	43, 44, 45	mp2an 704	. . . . . . . . . . . . . . 15 ⊢ (0 ≤ 1 ↔ (1..^0) = ∅)
47	42, 46	mpbi 233	. . . . . . . . . . . . . 14 ⊢ (1..^0) = ∅
48	41, 47	eqtrdi 2812	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 0 → (1..^(♯‘𝐹)) = ∅)
49	48	reseq2d 5978	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 0 → (𝑃 ↾ (1..^(♯‘𝐹))) = (𝑃 ↾ ∅))
50	49	cnveqd 5861	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 0 → ^◡(𝑃 ↾ (1..^(♯‘𝐹))) = ^◡(𝑃 ↾ ∅))
51	50	funeqd 6558	. . . . . . . . . 10 ⊢ ((♯‘𝐹) = 0 → (Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ↔ Fun ^◡(𝑃 ↾ ∅)))
52	48	imaeq2d 6062	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 0 → (𝑃 “ (1..^(♯‘𝐹))) = (𝑃 “ ∅))
53		ima0 6079	. . . . . . . . . . . . 13 ⊢ (𝑃 “ ∅) = ∅
54	52, 53	eqtrdi 2812	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 0 → (𝑃 “ (1..^(♯‘𝐹))) = ∅)
55	54	eleq2d 2847	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 0 → ((𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ (𝑃‘(♯‘𝐹)) ∈ ∅))
56	55	notbid 321	. . . . . . . . . 10 ⊢ ((♯‘𝐹) = 0 → (¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ ¬ (𝑃‘(♯‘𝐹)) ∈ ∅))
57	51, 56	anbi12d 643	. . . . . . . . 9 ⊢ ((♯‘𝐹) = 0 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ (Fun ^◡(𝑃 ↾ ∅) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ ∅)))
58		oveq2 7418	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) = 0 → (1...(♯‘𝐹)) = (1...0))
59		fz10 13572	. . . . . . . . . . . . 13 ⊢ (1...0) = ∅
60	58, 59	eqtrdi 2812	. . . . . . . . . . . 12 ⊢ ((♯‘𝐹) = 0 → (1...(♯‘𝐹)) = ∅)
61	60	reseq2d 5978	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) = 0 → (𝑃 ↾ (1...(♯‘𝐹))) = (𝑃 ↾ ∅))
62	61	cnveqd 5861	. . . . . . . . . 10 ⊢ ((♯‘𝐹) = 0 → ^◡(𝑃 ↾ (1...(♯‘𝐹))) = ^◡(𝑃 ↾ ∅))
63	62	funeqd 6558	. . . . . . . . 9 ⊢ ((♯‘𝐹) = 0 → (Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))) ↔ Fun ^◡(𝑃 ↾ ∅)))
64	40, 57, 63	3bitr4d 314	. . . . . . . 8 ⊢ ((♯‘𝐹) = 0 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹)))))
65	64	a1d 26	. . . . . . 7 ⊢ ((♯‘𝐹) = 0 → (𝐹(Trails‘𝐺)𝑃 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))))))
66		df-nel 3063	. . . . . . . . . . . . 13 ⊢ ((𝑃‘(♯‘𝐹)) ∉ (𝑃 “ (1..^(♯‘𝐹))) ↔ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹))))
67	66	bicomi 227	. . . . . . . . . . . 12 ⊢ (¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹))) ↔ (𝑃‘(♯‘𝐹)) ∉ (𝑃 “ (1..^(♯‘𝐹))))
68	67	anbi2i 634	. . . . . . . . . . 11 ⊢ ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ (Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ (𝑃‘(♯‘𝐹)) ∉ (𝑃 “ (1..^(♯‘𝐹)))))
69		trliswlk 30011	. . . . . . . . . . . 12 ⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
70	3, 10	sylib 221	. . . . . . . . . . . . . 14 ⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ (0...(♯‘𝐹)))
71		fzonel 13701	. . . . . . . . . . . . . . 15 ⊢ ¬ (♯‘𝐹) ∈ (1..^(♯‘𝐹))
72	71	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐹(Walks‘𝐺)𝑃 → ¬ (♯‘𝐹) ∈ (1..^(♯‘𝐹)))
73	70, 72	eldifd 3915	. . . . . . . . . . . . 13 ⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ((0...(♯‘𝐹)) ∖ (1..^(♯‘𝐹))))
74		1eluzge0 12903	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ (ℤ_≥‘0)
75		fzoss1 13714	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (ℤ_≥‘0) → (1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹)))
76	74, 75	mp1i 14	. . . . . . . . . . . . . 14 ⊢ (𝐹(Walks‘𝐺)𝑃 → (1..^(♯‘𝐹)) ⊆ (0..^(♯‘𝐹)))
77		fzossfz 13706	. . . . . . . . . . . . . 14 ⊢ (0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
78	76, 77	sstrdi 3948	. . . . . . . . . . . . 13 ⊢ (𝐹(Walks‘𝐺)𝑃 → (1..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹)))
79	5, 73, 78	3jca 1144	. . . . . . . . . . . 12 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ((0...(♯‘𝐹)) ∖ (1..^(♯‘𝐹))) ∧ (1..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))))
80		resf1ext2b 7931	. . . . . . . . . . . 12 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ((0...(♯‘𝐹)) ∖ (1..^(♯‘𝐹))) ∧ (1..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))) → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ (𝑃‘(♯‘𝐹)) ∉ (𝑃 “ (1..^(♯‘𝐹)))) ↔ Fun ^◡(𝑃 ↾ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))))
81	69, 79, 80	3syl 19	. . . . . . . . . . 11 ⊢ (𝐹(Trails‘𝐺)𝑃 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ (𝑃‘(♯‘𝐹)) ∉ (𝑃 “ (1..^(♯‘𝐹)))) ↔ Fun ^◡(𝑃 ↾ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))))
82	68, 81	bitrid 286	. . . . . . . . . 10 ⊢ (𝐹(Trails‘𝐺)𝑃 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ Fun ^◡(𝑃 ↾ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))))
83	82	adantl 486	. . . . . . . . 9 ⊢ (((♯‘𝐹) ≠ 0 ∧ 𝐹(Trails‘𝐺)𝑃) → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ Fun ^◡(𝑃 ↾ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))))
84		elnnne0 12517	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐹) ∈ ℕ ↔ ((♯‘𝐹) ∈ ℕ₀ ∧ (♯‘𝐹) ≠ 0))
85		elnnuz 12901	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐹) ∈ ℕ ↔ (♯‘𝐹) ∈ (ℤ_≥‘1))
86	84, 85	sylbb1 240	. . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ (♯‘𝐹) ≠ 0) → (♯‘𝐹) ∈ (ℤ_≥‘1))
87	86	ex 417	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐹) ∈ ℕ₀ → ((♯‘𝐹) ≠ 0 → (♯‘𝐹) ∈ (ℤ_≥‘1)))
88	69, 3, 87	3syl 19	. . . . . . . . . . . . . . 15 ⊢ (𝐹(Trails‘𝐺)𝑃 → ((♯‘𝐹) ≠ 0 → (♯‘𝐹) ∈ (ℤ_≥‘1)))
89	88	impcom 412	. . . . . . . . . . . . . 14 ⊢ (((♯‘𝐹) ≠ 0 ∧ 𝐹(Trails‘𝐺)𝑃) → (♯‘𝐹) ∈ (ℤ_≥‘1))
90		fzisfzounsn 13808	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) ∈ (ℤ_≥‘1) → (1...(♯‘𝐹)) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
91	89, 90	syl 18	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐹) ≠ 0 ∧ 𝐹(Trails‘𝐺)𝑃) → (1...(♯‘𝐹)) = ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}))
92	91	eqcomd 2767	. . . . . . . . . . . 12 ⊢ (((♯‘𝐹) ≠ 0 ∧ 𝐹(Trails‘𝐺)𝑃) → ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)}) = (1...(♯‘𝐹)))
93	92	reseq2d 5978	. . . . . . . . . . 11 ⊢ (((♯‘𝐹) ≠ 0 ∧ 𝐹(Trails‘𝐺)𝑃) → (𝑃 ↾ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})) = (𝑃 ↾ (1...(♯‘𝐹))))
94	93	cnveqd 5861	. . . . . . . . . 10 ⊢ (((♯‘𝐹) ≠ 0 ∧ 𝐹(Trails‘𝐺)𝑃) → ^◡(𝑃 ↾ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})) = ^◡(𝑃 ↾ (1...(♯‘𝐹))))
95	94	funeqd 6558	. . . . . . . . 9 ⊢ (((♯‘𝐹) ≠ 0 ∧ 𝐹(Trails‘𝐺)𝑃) → (Fun ^◡(𝑃 ↾ ((1..^(♯‘𝐹)) ∪ {(♯‘𝐹)})) ↔ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹)))))
96	83, 95	bitrd 282	. . . . . . . 8 ⊢ (((♯‘𝐹) ≠ 0 ∧ 𝐹(Trails‘𝐺)𝑃) → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹)))))
97	96	ex 417	. . . . . . 7 ⊢ ((♯‘𝐹) ≠ 0 → (𝐹(Trails‘𝐺)𝑃 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))))))
98	65, 97	pm2.61ine 3039	. . . . . 6 ⊢ (𝐹(Trails‘𝐺)𝑃 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ↔ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹)))))
99	98	anbi1d 642	. . . . 5 ⊢ (𝐹(Trails‘𝐺)𝑃 → (((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ¬ (𝑃‘(♯‘𝐹)) ∈ (𝑃 “ (1..^(♯‘𝐹)))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))) ↔ (Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))))))
100	33, 36, 99	3bitrd 308	. . . 4 ⊢ (𝐹(Trails‘𝐺)𝑃 → ((Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅) ↔ (Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))))))
101	100	pm5.32i 584	. . 3 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅)) ↔ (𝐹(Trails‘𝐺)𝑃 ∧ (Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))))))
102		3anass 1109	. . 3 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅) ↔ (𝐹(Trails‘𝐺)𝑃 ∧ (Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅)))
103		3anass 1109	. . 3 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))) ↔ (𝐹(Trails‘𝐺)𝑃 ∧ (Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹))))))
104	101, 102, 103	3bitr4i 306	. 2 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅) ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))))
105	1, 104	bitri 278	1 ⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ^◡(𝑃 ↾ (1...(♯‘𝐹))) ∧ (𝑃‘0) ∉ (𝑃 “ (1..^(♯‘𝐹)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1568 ∈ wcel 2141 ≠ wne 2956 ∉ wnel 3062 ∀wral 3077 ∖ cdif 3901 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 {csn 4588 {cpr 4590 class class class wbr 5108 ^◡ccnv 5660 ↾ cres 5663 “ cima 5664 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 0cc0 11099 1c1 11100 ≤ cle 11243 ℕcn 12232 ℕ₀cn0 12503 ℤcz 12590 ℤ_≥cuz 12861 ...cfz 13534 ..^cfzo 13681 ♯chash 14365 Vtxcvtx 29312 Walkscwlks 29912 Trailsctrls 30004 Pathscpths 30025

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-ifp 1077 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-er 8693 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-n0 12504 df-z 12591 df-uz 12862 df-fz 13535 df-fzo 13682 df-hash 14366 df-word 14550 df-wlks 29915 df-trls 30006 df-pths 30029

This theorem is referenced by: pthdifv 30045

W3C validator