eupath2 - Metamath Proof Explorer

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

Theorem eupath2 26507

Description: The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (Contributed by Mario Carneiro, 8-Apr-2015.)

**Hypotheses**
Ref	Expression
eupath2.1	⊢ (𝜑 → 𝐸 Fn 𝐴)
eupath2.3	⊢ (𝜑 → 𝐹(𝑉 EulPaths 𝐸)𝑃)

**Assertion**
Ref	Expression
eupath2	⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))}))

Distinct variable groups: 𝑥,𝐸 𝑥,𝐹 𝑥,𝑉 𝜑,𝑥 Allowed substitution hints: 𝐴(𝑥) 𝑃(𝑥)

Proof of Theorem eupath2 Dummy variables 𝑚 𝑛 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eupath2.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹(𝑉 EulPaths 𝐸)𝑃)
2		eupath2.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 Fn 𝐴)
3		eupaf1o 26497	. . . . . . . . . . 11 ⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴)
4	1, 2, 3	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴)
5		f1ofo 6057	. . . . . . . . . 10 ⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 → 𝐹:(1...(#‘𝐹))–onto→𝐴)
6		foima 6033	. . . . . . . . . 10 ⊢ (𝐹:(1...(#‘𝐹))–onto→𝐴 → (𝐹 “ (1...(#‘𝐹))) = 𝐴)
7	4, 5, 6	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 “ (1...(#‘𝐹))) = 𝐴)
8	7	reseq2d 5317	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))) = (𝐸 ↾ 𝐴))
9		fnresdm 5914	. . . . . . . . 9 ⊢ (𝐸 Fn 𝐴 → (𝐸 ↾ 𝐴) = 𝐸)
10	2, 9	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾ 𝐴) = 𝐸)
11	8, 10	eqtrd 2644	. . . . . . 7 ⊢ (𝜑 → (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))) = 𝐸)
12	11	oveq2d 6565	. . . . . 6 ⊢ (𝜑 → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹))))) = (𝑉 VDeg 𝐸))
13	12	fveq1d 6105	. . . . 5 ⊢ (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑥))
14	13	breq2d 4595	. . . 4 ⊢ (𝜑 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥) ↔ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)))
15	14	notbid 307	. . 3 ⊢ (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥) ↔ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)))
16	15	rabbidv 3164	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)} = {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)})
17		eupacl 26496	. . . . 5 ⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → (#‘𝐹) ∈ ℕ₀)
18		nn0re 11178	. . . . 5 ⊢ ((#‘𝐹) ∈ ℕ₀ → (#‘𝐹) ∈ ℝ)
19	1, 17, 18	3syl 18	. . . 4 ⊢ (𝜑 → (#‘𝐹) ∈ ℝ)
20	19	leidd 10473	. . 3 ⊢ (𝜑 → (#‘𝐹) ≤ (#‘𝐹))
21	1, 17	syl 17	. . . 4 ⊢ (𝜑 → (#‘𝐹) ∈ ℕ₀)
22		breq1 4586	. . . . . . 7 ⊢ (𝑚 = 0 → (𝑚 ≤ (#‘𝐹) ↔ 0 ≤ (#‘𝐹)))
23		oveq2 6557	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 0 → (1...𝑚) = (1...0))
24		fz10 12233	. . . . . . . . . . . . . . . . . 18 ⊢ (1...0) = ∅
25	23, 24	syl6eq 2660	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 0 → (1...𝑚) = ∅)
26	25	imaeq2d 5385	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 0 → (𝐹 “ (1...𝑚)) = (𝐹 “ ∅))
27		ima0 5400	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 “ ∅) = ∅
28	26, 27	syl6eq 2660	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 0 → (𝐹 “ (1...𝑚)) = ∅)
29	28	reseq2d 5317	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 0 → (𝐸 ↾ (𝐹 “ (1...𝑚))) = (𝐸 ↾ ∅))
30		res0 5321	. . . . . . . . . . . . . 14 ⊢ (𝐸 ↾ ∅) = ∅
31	29, 30	syl6eq 2660	. . . . . . . . . . . . 13 ⊢ (𝑚 = 0 → (𝐸 ↾ (𝐹 “ (1...𝑚))) = ∅)
32	31	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑚 = 0 → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚)))) = (𝑉 VDeg ∅))
33	32	fveq1d 6105	. . . . . . . . . . 11 ⊢ (𝑚 = 0 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) = ((𝑉 VDeg ∅)‘𝑥))
34	33	breq2d 4595	. . . . . . . . . 10 ⊢ (𝑚 = 0 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) ↔ 2 ∥ ((𝑉 VDeg ∅)‘𝑥)))
35	34	notbid 307	. . . . . . . . 9 ⊢ (𝑚 = 0 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) ↔ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥)))
36	35	rabbidv 3164	. . . . . . . 8 ⊢ (𝑚 = 0 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥)})
37		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑚 = 0 → (𝑃‘𝑚) = (𝑃‘0))
38	37	eqcomd 2616	. . . . . . . . 9 ⊢ (𝑚 = 0 → (𝑃‘0) = (𝑃‘𝑚))
39	38	iftrued 4044	. . . . . . . 8 ⊢ (𝑚 = 0 → if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}) = ∅)
40	36, 39	eqeq12d 2625	. . . . . . 7 ⊢ (𝑚 = 0 → ({𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}) ↔ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥)} = ∅))
41	22, 40	imbi12d 333	. . . . . 6 ⊢ (𝑚 = 0 → ((𝑚 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)})) ↔ (0 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥)} = ∅)))
42	41	imbi2d 329	. . . . 5 ⊢ (𝑚 = 0 → ((𝜑 → (𝑚 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}))) ↔ (𝜑 → (0 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥)} = ∅))))
43		breq1 4586	. . . . . . 7 ⊢ (𝑚 = 𝑛 → (𝑚 ≤ (#‘𝐹) ↔ 𝑛 ≤ (#‘𝐹)))
44		oveq2 6557	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
45	44	imaeq2d 5385	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝐹 “ (1...𝑚)) = (𝐹 “ (1...𝑛)))
46	45	reseq2d 5317	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝐸 ↾ (𝐹 “ (1...𝑚))) = (𝐸 ↾ (𝐹 “ (1...𝑛))))
47	46	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚)))) = (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛)))))
48	47	fveq1d 6105	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥))
49	48	breq2d 4595	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)))
50	49	notbid 307	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)))
51	50	rabbidv 3164	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)})
52		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (𝑃‘𝑚) = (𝑃‘𝑛))
53	52	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → ((𝑃‘0) = (𝑃‘𝑚) ↔ (𝑃‘0) = (𝑃‘𝑛)))
54	52	preq2d 4219	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → {(𝑃‘0), (𝑃‘𝑚)} = {(𝑃‘0), (𝑃‘𝑛)})
55	53, 54	ifbieq2d 4061	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}) = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))
56	51, 55	eqeq12d 2625	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ({𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}) ↔ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)})))
57	43, 56	imbi12d 333	. . . . . 6 ⊢ (𝑚 = 𝑛 → ((𝑚 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)})) ↔ (𝑛 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))))
58	57	imbi2d 329	. . . . 5 ⊢ (𝑚 = 𝑛 → ((𝜑 → (𝑚 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}))) ↔ (𝜑 → (𝑛 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)})))))
59		breq1 4586	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → (𝑚 ≤ (#‘𝐹) ↔ (𝑛 + 1) ≤ (#‘𝐹)))
60		oveq2 6557	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑛 + 1) → (1...𝑚) = (1...(𝑛 + 1)))
61	60	imaeq2d 5385	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑛 + 1) → (𝐹 “ (1...𝑚)) = (𝐹 “ (1...(𝑛 + 1))))
62	61	reseq2d 5317	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (𝐸 ↾ (𝐹 “ (1...𝑚))) = (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))
63	62	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚)))) = (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1))))))
64	63	fveq1d 6105	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥))
65	64	breq2d 4595	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)))
66	65	notbid 307	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)))
67	66	rabbidv 3164	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)})
68		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → (𝑃‘𝑚) = (𝑃‘(𝑛 + 1)))
69	68	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → ((𝑃‘0) = (𝑃‘𝑚) ↔ (𝑃‘0) = (𝑃‘(𝑛 + 1))))
70	68	preq2d 4219	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 + 1) → {(𝑃‘0), (𝑃‘𝑚)} = {(𝑃‘0), (𝑃‘(𝑛 + 1))})
71	69, 70	ifbieq2d 4061	. . . . . . . 8 ⊢ (𝑚 = (𝑛 + 1) → if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}) = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}))
72	67, 71	eqeq12d 2625	. . . . . . 7 ⊢ (𝑚 = (𝑛 + 1) → ({𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}) ↔ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))})))
73	59, 72	imbi12d 333	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → ((𝑚 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)})) ↔ ((𝑛 + 1) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}))))
74	73	imbi2d 329	. . . . 5 ⊢ (𝑚 = (𝑛 + 1) → ((𝜑 → (𝑚 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}))) ↔ (𝜑 → ((𝑛 + 1) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))})))))
75		breq1 4586	. . . . . . 7 ⊢ (𝑚 = (#‘𝐹) → (𝑚 ≤ (#‘𝐹) ↔ (#‘𝐹) ≤ (#‘𝐹)))
76		oveq2 6557	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (#‘𝐹) → (1...𝑚) = (1...(#‘𝐹)))
77	76	imaeq2d 5385	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (#‘𝐹) → (𝐹 “ (1...𝑚)) = (𝐹 “ (1...(#‘𝐹))))
78	77	reseq2d 5317	. . . . . . . . . . . . 13 ⊢ (𝑚 = (#‘𝐹) → (𝐸 ↾ (𝐹 “ (1...𝑚))) = (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))
79	78	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑚 = (#‘𝐹) → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚)))) = (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹))))))
80	79	fveq1d 6105	. . . . . . . . . . 11 ⊢ (𝑚 = (#‘𝐹) → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥))
81	80	breq2d 4595	. . . . . . . . . 10 ⊢ (𝑚 = (#‘𝐹) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)))
82	81	notbid 307	. . . . . . . . 9 ⊢ (𝑚 = (#‘𝐹) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)))
83	82	rabbidv 3164	. . . . . . . 8 ⊢ (𝑚 = (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)})
84		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑚 = (#‘𝐹) → (𝑃‘𝑚) = (𝑃‘(#‘𝐹)))
85	84	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑚 = (#‘𝐹) → ((𝑃‘0) = (𝑃‘𝑚) ↔ (𝑃‘0) = (𝑃‘(#‘𝐹))))
86	84	preq2d 4219	. . . . . . . . 9 ⊢ (𝑚 = (#‘𝐹) → {(𝑃‘0), (𝑃‘𝑚)} = {(𝑃‘0), (𝑃‘(#‘𝐹))})
87	85, 86	ifbieq2d 4061	. . . . . . . 8 ⊢ (𝑚 = (#‘𝐹) → if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}) = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))}))
88	83, 87	eqeq12d 2625	. . . . . . 7 ⊢ (𝑚 = (#‘𝐹) → ({𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}) ↔ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))})))
89	75, 88	imbi12d 333	. . . . . 6 ⊢ (𝑚 = (#‘𝐹) → ((𝑚 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)})) ↔ ((#‘𝐹) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))}))))
90	89	imbi2d 329	. . . . 5 ⊢ (𝑚 = (#‘𝐹) → ((𝜑 → (𝑚 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑚))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑚), ∅, {(𝑃‘0), (𝑃‘𝑚)}))) ↔ (𝜑 → ((#‘𝐹) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))})))))
91		2z 11286	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
92		dvds0 14835	. . . . . . . . . . 11 ⊢ (2 ∈ ℤ → 2 ∥ 0)
93	91, 92	ax-mp 5	. . . . . . . . . 10 ⊢ 2 ∥ 0
94		eupagra 26493	. . . . . . . . . . . 12 ⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → 𝑉 UMGrph 𝐸)
95		relumgra 25843	. . . . . . . . . . . . 13 ⊢ Rel UMGrph
96	95	brrelexi 5082	. . . . . . . . . . . 12 ⊢ (𝑉 UMGrph 𝐸 → 𝑉 ∈ V)
97	1, 94, 96	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ V)
98		vdgr0 26427	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ 𝑥 ∈ 𝑉) → ((𝑉 VDeg ∅)‘𝑥) = 0)
99	97, 98	sylan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝑉 VDeg ∅)‘𝑥) = 0)
100	93, 99	syl5breqr 4621	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 2 ∥ ((𝑉 VDeg ∅)‘𝑥))
101		notnot 135	. . . . . . . . 9 ⊢ (2 ∥ ((𝑉 VDeg ∅)‘𝑥) → ¬ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥))
102	100, 101	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ¬ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥))
103	102	ralrimiva 2949	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝑉 ¬ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥))
104		rabeq0 3911	. . . . . . 7 ⊢ ({𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥)} = ∅ ↔ ∀𝑥 ∈ 𝑉 ¬ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥))
105	103, 104	sylibr 223	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥)} = ∅)
106	105	a1d 25	. . . . 5 ⊢ (𝜑 → (0 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg ∅)‘𝑥)} = ∅))
107		nn0re 11178	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
108	107	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ ℝ)
109	108	lep1d 10834	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ≤ (𝑛 + 1))
110		peano2re 10088	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℝ → (𝑛 + 1) ∈ ℝ)
111	108, 110	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑛 + 1) ∈ ℝ)
112	19	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (#‘𝐹) ∈ ℝ)
113		letr 10010	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (#‘𝐹) ∈ ℝ) → ((𝑛 ≤ (𝑛 + 1) ∧ (𝑛 + 1) ≤ (#‘𝐹)) → 𝑛 ≤ (#‘𝐹)))
114	108, 111, 112, 113	syl3anc 1318	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 ≤ (𝑛 + 1) ∧ (𝑛 + 1) ≤ (#‘𝐹)) → 𝑛 ≤ (#‘𝐹)))
115	109, 114	mpand 707	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 + 1) ≤ (#‘𝐹) → 𝑛 ≤ (#‘𝐹)))
116	115	imim1d 80	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)})) → ((𝑛 + 1) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))))
117		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑦))
118	117	breq2d 4595	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑦)))
119	118	notbid 307	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑦)))
120	119	elrab 3331	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} ↔ (𝑦 ∈ 𝑉 ∧ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑦)))
121	2	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) ∧ 𝑦 ∈ 𝑉) → 𝐸 Fn 𝐴)
122	1	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) ∧ 𝑦 ∈ 𝑉) → 𝐹(𝑉 EulPaths 𝐸)𝑃)
123		simpllr 795	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) ∧ 𝑦 ∈ 𝑉) → 𝑛 ∈ ℕ₀)
124		simplrl 796	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) ∧ 𝑦 ∈ 𝑉) → (𝑛 + 1) ≤ (#‘𝐹))
125		simpr 476	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉)
126		simplrr 797	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) ∧ 𝑦 ∈ 𝑉) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))
127	121, 122, 123, 124, 125, 126	eupath2lem3 26506	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) ∧ 𝑦 ∈ 𝑉) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑦) ↔ 𝑦 ∈ if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))})))
128	127	pm5.32da 671	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → ((𝑦 ∈ 𝑉 ∧ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑦)) ↔ (𝑦 ∈ 𝑉 ∧ 𝑦 ∈ if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}))))
129		0elpw 4760	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ 𝒫 𝑉
130		eupapf 26499	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉)
131	1, 130	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶𝑉)
132	131	ad2antrr 758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → 𝑃:(0...(#‘𝐹))⟶𝑉)
133	21	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (#‘𝐹) ∈ ℕ₀)
134		nn0uz 11598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ₀ = (ℤ_≥‘0)
135	133, 134	syl6eleq 2698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (#‘𝐹) ∈ (ℤ_≥‘0))
136		eluzfz1 12219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝐹) ∈ (ℤ_≥‘0) → 0 ∈ (0...(#‘𝐹)))
137	135, 136	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → 0 ∈ (0...(#‘𝐹)))
138	132, 137	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝑃‘0) ∈ 𝑉)
139		simprl 790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝑛 + 1) ≤ (#‘𝐹))
140		peano2nn0 11210	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ ℕ₀ → (𝑛 + 1) ∈ ℕ₀)
141	140	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝑛 + 1) ∈ ℕ₀)
142	141, 134	syl6eleq 2698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝑛 + 1) ∈ (ℤ_≥‘0))
143	133	nn0zd 11356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (#‘𝐹) ∈ ℤ)
144		elfz5 12205	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 + 1) ∈ (ℤ_≥‘0) ∧ (#‘𝐹) ∈ ℤ) → ((𝑛 + 1) ∈ (0...(#‘𝐹)) ↔ (𝑛 + 1) ≤ (#‘𝐹)))
145	142, 143, 144	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → ((𝑛 + 1) ∈ (0...(#‘𝐹)) ↔ (𝑛 + 1) ≤ (#‘𝐹)))
146	139, 145	mpbird 246	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝑛 + 1) ∈ (0...(#‘𝐹)))
147	132, 146	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝑃‘(𝑛 + 1)) ∈ 𝑉)
148		prssi 4293	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘(𝑛 + 1)) ∈ 𝑉) → {(𝑃‘0), (𝑃‘(𝑛 + 1))} ⊆ 𝑉)
149	138, 147, 148	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → {(𝑃‘0), (𝑃‘(𝑛 + 1))} ⊆ 𝑉)
150		prex 4836	. . . . . . . . . . . . . . . . . . 19 ⊢ {(𝑃‘0), (𝑃‘(𝑛 + 1))} ∈ V
151	150	elpw 4114	. . . . . . . . . . . . . . . . . 18 ⊢ ({(𝑃‘0), (𝑃‘(𝑛 + 1))} ∈ 𝒫 𝑉 ↔ {(𝑃‘0), (𝑃‘(𝑛 + 1))} ⊆ 𝑉)
152	149, 151	sylibr 223	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → {(𝑃‘0), (𝑃‘(𝑛 + 1))} ∈ 𝒫 𝑉)
153		ifcl 4080	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ∈ 𝒫 𝑉 ∧ {(𝑃‘0), (𝑃‘(𝑛 + 1))} ∈ 𝒫 𝑉) → if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}) ∈ 𝒫 𝑉)
154	129, 152, 153	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}) ∈ 𝒫 𝑉)
155	154	elpwid 4118	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}) ⊆ 𝑉)
156	155	sseld 3567	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝑦 ∈ if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}) → 𝑦 ∈ 𝑉))
157	156	pm4.71rd 665	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝑦 ∈ if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}) ↔ (𝑦 ∈ 𝑉 ∧ 𝑦 ∈ if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}))))
158	128, 157	bitr4d 270	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → ((𝑦 ∈ 𝑉 ∧ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑦)) ↔ 𝑦 ∈ if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))})))
159	120, 158	syl5bb 271	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝑦 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} ↔ 𝑦 ∈ if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))})))
160	159	eqrdv 2608	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ ((𝑛 + 1) ≤ (#‘𝐹) ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}))
161	160	exp32 629	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 + 1) ≤ (#‘𝐹) → ({𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}))))
162	161	a2d 29	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (((𝑛 + 1) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)})) → ((𝑛 + 1) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}))))
163	116, 162	syld 46	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑛 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)})) → ((𝑛 + 1) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}))))
164	163	expcom 450	. . . . . 6 ⊢ (𝑛 ∈ ℕ₀ → (𝜑 → ((𝑛 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)})) → ((𝑛 + 1) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))})))))
165	164	a2d 29	. . . . 5 ⊢ (𝑛 ∈ ℕ₀ → ((𝜑 → (𝑛 ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑛))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)}))) → (𝜑 → ((𝑛 + 1) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑛 + 1)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))})))))
166	42, 58, 74, 90, 106, 165	nn0ind 11348	. . . 4 ⊢ ((#‘𝐹) ∈ ℕ₀ → (𝜑 → ((#‘𝐹) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))}))))
167	21, 166	mpcom 37	. . 3 ⊢ (𝜑 → ((#‘𝐹) ≤ (#‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))})))
168	20, 167	mpd 15	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(#‘𝐹)))))‘𝑥)} = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))}))
169	16, 168	eqtr3d 2646	1 ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 {crab 2900 Vcvv 3173 ⊆ wss 3540 ∅c0 3874 ifcif 4036 𝒫 cpw 4108 {cpr 4127 class class class wbr 4583 ↾ cres 5040 “ cima 5041 Fn wfn 5799 ⟶wf 5800 –onto→wfo 5802 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 ≤ cle 9954 2c2 10947 ℕ₀cn0 11169 ℤcz 11254 ℤ_≥cuz 11563 ...cfz 12197 #chash 12979 ∥ cdvds 14821 UMGrph cumg 25841 VDeg cvdg 26420 EulPaths ceup 26489

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-sup 8231 df-inf 8232 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-rp 11709 df-xadd 11823 df-fz 12198 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-dvds 14822 df-umgra 25842 df-vdgr 26421 df-eupa 26490

This theorem is referenced by: eupath 26508

W3C validator