eupath2lem3 - Metamath Proof Explorer

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

Theorem eupath2lem3 26506

Description: Lemma for eupath2 26507. (Contributed by Mario Carneiro, 8-Apr-2015.)

**Hypotheses**
Ref	Expression
eupath2.1	⊢ (𝜑 → 𝐸 Fn 𝐴)
eupath2.3	⊢ (𝜑 → 𝐹(𝑉 EulPaths 𝐸)𝑃)
eupath2.5	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
eupath2.6	⊢ (𝜑 → (𝑁 + 1) ≤ (#‘𝐹))
eupath2.7	⊢ (𝜑 → 𝑈 ∈ 𝑉)
eupath2.8	⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))

**Assertion**
Ref	Expression
eupath2lem3	⊢ (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))

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

**Proof of Theorem eupath2lem3**
Step	Hyp	Ref	Expression
1		imaundi 5464	. . . . . . . . . . 11 ⊢ (𝐹 “ ((1...𝑁) ∪ {(𝑁 + 1)})) = ((𝐹 “ (1...𝑁)) ∪ (𝐹 “ {(𝑁 + 1)}))
2		1z 11284	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℤ
3		eupath2.5	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
4		nn0uz 11598	. . . . . . . . . . . . . . 15 ⊢ ℕ₀ = (ℤ_≥‘0)
5		1m1e0 10966	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
6	5	fveq2i 6106	. . . . . . . . . . . . . . 15 ⊢ (ℤ_≥‘(1 − 1)) = (ℤ_≥‘0)
7	4, 6	eqtr4i 2635	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘(1 − 1))
8	3, 7	syl6eleq 2698	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
9		fzsuc2 12268	. . . . . . . . . . . . 13 ⊢ ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ_≥‘(1 − 1))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
10	2, 8, 9	sylancr 694	. . . . . . . . . . . 12 ⊢ (𝜑 → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
11	10	imaeq2d 5385	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 “ (1...(𝑁 + 1))) = (𝐹 “ ((1...𝑁) ∪ {(𝑁 + 1)})))
12		eupath2.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹(𝑉 EulPaths 𝐸)𝑃)
13		eupath2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 Fn 𝐴)
14		eupaf1o 26497	. . . . . . . . . . . . . . 15 ⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴)
15	12, 13, 14	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴)
16		f1ofn 6051	. . . . . . . . . . . . . 14 ⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 → 𝐹 Fn (1...(#‘𝐹)))
17	15, 16	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 Fn (1...(#‘𝐹)))
18		eupath2.6	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 + 1) ≤ (#‘𝐹))
19		nn0p1nn 11209	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
20	3, 19	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
21		nnuz 11599	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
22	20, 21	syl6eleq 2698	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
23		eupacl 26496	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → (#‘𝐹) ∈ ℕ₀)
24	12, 23	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (#‘𝐹) ∈ ℕ₀)
25	24	nn0zd 11356	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (#‘𝐹) ∈ ℤ)
26		elfz5 12205	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 + 1) ∈ (ℤ_≥‘1) ∧ (#‘𝐹) ∈ ℤ) → ((𝑁 + 1) ∈ (1...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
27	22, 25, 26	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑁 + 1) ∈ (1...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
28	18, 27	mpbird 246	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + 1) ∈ (1...(#‘𝐹)))
29		fnsnfv 6168	. . . . . . . . . . . . 13 ⊢ ((𝐹 Fn (1...(#‘𝐹)) ∧ (𝑁 + 1) ∈ (1...(#‘𝐹))) → {(𝐹‘(𝑁 + 1))} = (𝐹 “ {(𝑁 + 1)}))
30	17, 28, 29	syl2anc 691	. . . . . . . . . . . 12 ⊢ (𝜑 → {(𝐹‘(𝑁 + 1))} = (𝐹 “ {(𝑁 + 1)}))
31	30	uneq2d 3729	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))}) = ((𝐹 “ (1...𝑁)) ∪ (𝐹 “ {(𝑁 + 1)})))
32	1, 11, 31	3eqtr4a 2670	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 “ (1...(𝑁 + 1))) = ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))}))
33	32	reseq2d 5317	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))) = (𝐸 ↾ ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))})))
34		resundi 5330	. . . . . . . . 9 ⊢ (𝐸 ↾ ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))})) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ (𝐸 ↾ {(𝐹‘(𝑁 + 1))}))
35	33, 34	syl6eq 2660	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ (𝐸 ↾ {(𝐹‘(𝑁 + 1))})))
36		f1of 6050	. . . . . . . . . . . . 13 ⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 → 𝐹:(1...(#‘𝐹))⟶𝐴)
37	15, 36	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:(1...(#‘𝐹))⟶𝐴)
38	37, 28	ffvelrnd 6268	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘(𝑁 + 1)) ∈ 𝐴)
39		fnressn 6330	. . . . . . . . . . 11 ⊢ ((𝐸 Fn 𝐴 ∧ (𝐹‘(𝑁 + 1)) ∈ 𝐴) → (𝐸 ↾ {(𝐹‘(𝑁 + 1))}) = {⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩})
40	13, 38, 39	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 ↾ {(𝐹‘(𝑁 + 1))}) = {⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩})
41		eupaseg 26500	. . . . . . . . . . . . . 14 ⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ (𝑁 + 1) ∈ (1...(#‘𝐹))) → (𝐸‘(𝐹‘(𝑁 + 1))) = {(𝑃‘((𝑁 + 1) − 1)), (𝑃‘(𝑁 + 1))})
42	12, 28, 41	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸‘(𝐹‘(𝑁 + 1))) = {(𝑃‘((𝑁 + 1) − 1)), (𝑃‘(𝑁 + 1))})
43	3	nn0cnd 11230	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℂ)
44		ax-1cn 9873	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
45		pncan 10166	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
46	43, 44, 45	sylancl 693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
47	46	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃‘((𝑁 + 1) − 1)) = (𝑃‘𝑁))
48	47	preq1d 4218	. . . . . . . . . . . . 13 ⊢ (𝜑 → {(𝑃‘((𝑁 + 1) − 1)), (𝑃‘(𝑁 + 1))} = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))})
49	42, 48	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘(𝐹‘(𝑁 + 1))) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))})
50	49	opeq2d 4347	. . . . . . . . . . 11 ⊢ (𝜑 → ⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩ = ⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩)
51	50	sneqd 4137	. . . . . . . . . 10 ⊢ (𝜑 → {⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩} = {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})
52	40, 51	eqtrd 2644	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 ↾ {(𝐹‘(𝑁 + 1))}) = {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})
53	52	uneq2d 3729	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ (𝐸 ↾ {(𝐹‘(𝑁 + 1))})) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩}))
54	35, 53	eqtrd 2644	. . . . . . 7 ⊢ (𝜑 → (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩}))
55	54	oveq2d 6565	. . . . . 6 ⊢ (𝜑 → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1))))) = (𝑉 VDeg ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})))
56	55	fveq1d 6105	. . . . 5 ⊢ (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) = ((𝑉 VDeg ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩}))‘𝑈))
57		imassrn 5396	. . . . . . . 8 ⊢ (𝐹 “ (1...𝑁)) ⊆ ran 𝐹
58		f1ofo 6057	. . . . . . . . 9 ⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 → 𝐹:(1...(#‘𝐹))–onto→𝐴)
59		forn 6031	. . . . . . . . 9 ⊢ (𝐹:(1...(#‘𝐹))–onto→𝐴 → ran 𝐹 = 𝐴)
60	15, 58, 59	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 = 𝐴)
61	57, 60	syl5sseq 3616	. . . . . . 7 ⊢ (𝜑 → (𝐹 “ (1...𝑁)) ⊆ 𝐴)
62		fnssres 5918	. . . . . . 7 ⊢ ((𝐸 Fn 𝐴 ∧ (𝐹 “ (1...𝑁)) ⊆ 𝐴) → (𝐸 ↾ (𝐹 “ (1...𝑁))) Fn (𝐹 “ (1...𝑁)))
63	13, 61, 62	syl2anc 691	. . . . . 6 ⊢ (𝜑 → (𝐸 ↾ (𝐹 “ (1...𝑁))) Fn (𝐹 “ (1...𝑁)))
64		fvex 6113	. . . . . . . 8 ⊢ (𝐹‘(𝑁 + 1)) ∈ V
65		prex 4836	. . . . . . . 8 ⊢ {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ∈ V
66	64, 65	fnsn 5860	. . . . . . 7 ⊢ {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩} Fn {(𝐹‘(𝑁 + 1))}
67	66	a1i 11	. . . . . 6 ⊢ (𝜑 → {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩} Fn {(𝐹‘(𝑁 + 1))})
68		eupafi 26498	. . . . . . . 8 ⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → 𝐴 ∈ Fin)
69	12, 13, 68	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ Fin)
70		ssfi 8065	. . . . . . 7 ⊢ ((𝐴 ∈ Fin ∧ (𝐹 “ (1...𝑁)) ⊆ 𝐴) → (𝐹 “ (1...𝑁)) ∈ Fin)
71	69, 61, 70	syl2anc 691	. . . . . 6 ⊢ (𝜑 → (𝐹 “ (1...𝑁)) ∈ Fin)
72		snfi 7923	. . . . . . 7 ⊢ {(𝐹‘(𝑁 + 1))} ∈ Fin
73	72	a1i 11	. . . . . 6 ⊢ (𝜑 → {(𝐹‘(𝑁 + 1))} ∈ Fin)
74	3	nn0red 11229	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ)
75	74	ltp1d 10833	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
76		peano2re 10088	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
77	74, 76	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
78	74, 77	ltnled 10063	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
79	75, 78	mpbid 221	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁)
80		f1of1 6049	. . . . . . . . . . 11 ⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 → 𝐹:(1...(#‘𝐹))–1-1→𝐴)
81	15, 80	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(1...(#‘𝐹))–1-1→𝐴)
82	3	nn0zd 11356	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
83	82	peano2zd 11361	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
84		eluz2 11569	. . . . . . . . . . . . 13 ⊢ ((#‘𝐹) ∈ (ℤ_≥‘(𝑁 + 1)) ↔ ((𝑁 + 1) ∈ ℤ ∧ (#‘𝐹) ∈ ℤ ∧ (𝑁 + 1) ≤ (#‘𝐹)))
85	83, 25, 18, 84	syl3anbrc 1239	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝐹) ∈ (ℤ_≥‘(𝑁 + 1)))
86		peano2uzr 11619	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ (#‘𝐹) ∈ (ℤ_≥‘(𝑁 + 1))) → (#‘𝐹) ∈ (ℤ_≥‘𝑁))
87	82, 85, 86	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝐹) ∈ (ℤ_≥‘𝑁))
88		fzss2 12252	. . . . . . . . . . 11 ⊢ ((#‘𝐹) ∈ (ℤ_≥‘𝑁) → (1...𝑁) ⊆ (1...(#‘𝐹)))
89	87, 88	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1...𝑁) ⊆ (1...(#‘𝐹)))
90		f1elima 6421	. . . . . . . . . 10 ⊢ ((𝐹:(1...(#‘𝐹))–1-1→𝐴 ∧ (𝑁 + 1) ∈ (1...(#‘𝐹)) ∧ (1...𝑁) ⊆ (1...(#‘𝐹))) → ((𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)) ↔ (𝑁 + 1) ∈ (1...𝑁)))
91	81, 28, 89, 90	syl3anc 1318	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)) ↔ (𝑁 + 1) ∈ (1...𝑁)))
92		elfz5 12205	. . . . . . . . . 10 ⊢ (((𝑁 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑁 + 1) ∈ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
93	22, 82, 92	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 1) ∈ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
94	91, 93	bitrd 267	. . . . . . . 8 ⊢ (𝜑 → ((𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁))
95	79, 94	mtbird 314	. . . . . . 7 ⊢ (𝜑 → ¬ (𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)))
96		disjsn 4192	. . . . . . 7 ⊢ (((𝐹 “ (1...𝑁)) ∩ {(𝐹‘(𝑁 + 1))}) = ∅ ↔ ¬ (𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)))
97	95, 96	sylibr 223	. . . . . 6 ⊢ (𝜑 → ((𝐹 “ (1...𝑁)) ∩ {(𝐹‘(𝑁 + 1))}) = ∅)
98		eupagra 26493	. . . . . . 7 ⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → 𝑉 UMGrph 𝐸)
99		umgrares 25853	. . . . . . 7 ⊢ (𝑉 UMGrph 𝐸 → 𝑉 UMGrph (𝐸 ↾ (𝐹 “ (1...𝑁))))
100	12, 98, 99	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑉 UMGrph (𝐸 ↾ (𝐹 “ (1...𝑁))))
101		relumgra 25843	. . . . . . . . 9 ⊢ Rel UMGrph
102	101	brrelexi 5082	. . . . . . . 8 ⊢ (𝑉 UMGrph 𝐸 → 𝑉 ∈ V)
103	12, 98, 102	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ V)
104		eupapf 26499	. . . . . . . . 9 ⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉)
105	12, 104	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶𝑉)
106	3, 4	syl6eleq 2698	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
107		elfzuzb 12207	. . . . . . . . 9 ⊢ (𝑁 ∈ (0...(#‘𝐹)) ↔ (𝑁 ∈ (ℤ_≥‘0) ∧ (#‘𝐹) ∈ (ℤ_≥‘𝑁)))
108	106, 87, 107	sylanbrc 695	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0...(#‘𝐹)))
109	105, 108	ffvelrnd 6268	. . . . . . 7 ⊢ (𝜑 → (𝑃‘𝑁) ∈ 𝑉)
110		peano2nn0 11210	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
111	3, 110	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ₀)
112	111, 4	syl6eleq 2698	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘0))
113		elfz5 12205	. . . . . . . . . 10 ⊢ (((𝑁 + 1) ∈ (ℤ_≥‘0) ∧ (#‘𝐹) ∈ ℤ) → ((𝑁 + 1) ∈ (0...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
114	112, 25, 113	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 1) ∈ (0...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
115	18, 114	mpbird 246	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ (0...(#‘𝐹)))
116	105, 115	ffvelrnd 6268	. . . . . . 7 ⊢ (𝜑 → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
117		umgra1 25855	. . . . . . 7 ⊢ (((𝑉 ∈ V ∧ (𝐹‘(𝑁 + 1)) ∈ 𝐴) ∧ ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉)) → 𝑉 UMGrph {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})
118	103, 38, 109, 116, 117	syl22anc 1319	. . . . . 6 ⊢ (𝜑 → 𝑉 UMGrph {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})
119		eupath2.7	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
120	63, 67, 71, 73, 97, 100, 118, 119	vdgrfiun 26429	. . . . 5 ⊢ (𝜑 → ((𝑉 VDeg ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩}))‘𝑈) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)))
121	56, 120	eqtrd 2644	. . . 4 ⊢ (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)))
122	121	breq2d 4595	. . 3 ⊢ (𝜑 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
123	122	notbid 307	. 2 ⊢ (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
124		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑥 = 𝑈 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
125	124	breq2d 4595	. . . . . . . . 9 ⊢ (𝑥 = 𝑈 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
126	125	notbid 307	. . . . . . . 8 ⊢ (𝑥 = 𝑈 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
127	126	elrab3 3332	. . . . . . 7 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
128	119, 127	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
129		eupath2.8	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))
130	129	eleq2d 2673	. . . . . 6 ⊢ (𝜑 → (𝑈 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
131	128, 130	bitr3d 269	. . . . 5 ⊢ (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
132	131	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
133		2z 11286	. . . . . . . 8 ⊢ 2 ∈ ℤ
134	133	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 2 ∈ ℤ)
135		vdgrfif 26426	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ (𝐸 ↾ (𝐹 “ (1...𝑁))) Fn (𝐹 “ (1...𝑁)) ∧ (𝐹 “ (1...𝑁)) ∈ Fin) → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁)))):𝑉⟶ℕ₀)
136	103, 63, 71, 135	syl3anc 1318	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁)))):𝑉⟶ℕ₀)
137	136, 119	ffvelrnd 6268	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℕ₀)
138	137	nn0zd 11356	. . . . . . . 8 ⊢ (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ)
139	138	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ)
140		vdgrfif 26426	. . . . . . . . . . 11 ⊢ ((𝑉 ∈ V ∧ {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩} Fn {(𝐹‘(𝑁 + 1))} ∧ {(𝐹‘(𝑁 + 1))} ∈ Fin) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩}):𝑉⟶ℕ₀)
141	103, 67, 73, 140	syl3anc 1318	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩}):𝑉⟶ℕ₀)
142	141, 119	ffvelrnd 6268	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℕ₀)
143	142	nn0zd 11356	. . . . . . . 8 ⊢ (𝜑 → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℤ)
144	143	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℤ)
145		iddvds 14833	. . . . . . . . . 10 ⊢ (2 ∈ ℤ → 2 ∥ 2)
146	133, 145	ax-mp 5	. . . . . . . . 9 ⊢ 2 ∥ 2
147		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑃‘𝑁) = 𝑈)
148		simplr 788	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑃‘𝑁) = (𝑃‘(𝑁 + 1)))
149	148, 147	eqtr3d 2646	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) = 𝑈)
150	147, 149	preq12d 4220	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, 𝑈})
151		dfsn2 4138	. . . . . . . . . . . . . . 15 ⊢ {𝑈} = {𝑈, 𝑈}
152	150, 151	syl6eqr 2662	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} = {𝑈})
153	152	opeq2d 4347	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩ = ⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩)
154	153	sneqd 4137	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩} = {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩})
155	154	oveq2d 6565	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩}) = (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩}))
156	155	fveq1d 6105	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩})‘𝑈))
157	103	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → 𝑉 ∈ V)
158	64	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
159	119	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → 𝑈 ∈ 𝑉)
160	157, 158, 159	vdgr1d 26430	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩})‘𝑈) = 2)
161	156, 160	eqtrd 2644	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 2)
162	146, 161	syl5breqr 4621	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → 2 ∥ ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
163		dvds0 14835	. . . . . . . . . 10 ⊢ (2 ∈ ℤ → 2 ∥ 0)
164	133, 163	ax-mp 5	. . . . . . . . 9 ⊢ 2 ∥ 0
165	103	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → 𝑉 ∈ V)
166	64	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
167	119	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → 𝑈 ∈ 𝑉)
168	109	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → (𝑃‘𝑁) ∈ 𝑉)
169		simpr 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → (𝑃‘𝑁) ≠ 𝑈)
170	116	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
171		simplr 788	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → (𝑃‘𝑁) = (𝑃‘(𝑁 + 1)))
172	171, 169	eqnetrrd 2850	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → (𝑃‘(𝑁 + 1)) ≠ 𝑈)
173	165, 166, 167, 168, 169, 170, 172	vdgr1a 26433	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 0)
174	164, 173	syl5breqr 4621	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) ≠ 𝑈) → 2 ∥ ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
175	162, 174	pm2.61dane 2869	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → 2 ∥ ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
176		dvdsadd2b 14866	. . . . . . 7 ⊢ ((2 ∈ ℤ ∧ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ ∧ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℤ ∧ 2 ∥ ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))))
177	134, 139, 144, 175, 176	syl112anc 1322	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))))
178	142	nn0cnd 11230	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℂ)
179	137	nn0cnd 11230	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℂ)
180	178, 179	addcomd 10117	. . . . . . . 8 ⊢ (𝜑 → (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)))
181	180	breq2d 4595	. . . . . . 7 ⊢ (𝜑 → (2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
182	181	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
183	177, 182	bitrd 267	. . . . 5 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
184	183	notbid 307	. . . 4 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
185		simpr 476	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝑃‘𝑁) = (𝑃‘(𝑁 + 1)))
186	185	eqeq2d 2620	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑃‘0) = (𝑃‘𝑁) ↔ (𝑃‘0) = (𝑃‘(𝑁 + 1))))
187	185	preq2d 4219	. . . . . 6 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → {(𝑃‘0), (𝑃‘𝑁)} = {(𝑃‘0), (𝑃‘(𝑁 + 1))})
188	186, 187	ifbieq2d 4061	. . . . 5 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) = if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))
189	188	eleq2d 2673	. . . 4 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
190	132, 184, 189	3bitr3d 297	. . 3 ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
191		simpr 476	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑃‘𝑁) = 𝑈)
192	191	preq1d 4218	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, (𝑃‘(𝑁 + 1))})
193	192	opeq2d 4347	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩ = ⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩)
194	193	sneqd 4137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩} = {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩})
195	194	oveq2d 6565	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩}) = (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩}))
196	195	fveq1d 6105	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
197	103	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → 𝑉 ∈ V)
198	64	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
199	119	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → 𝑈 ∈ 𝑉)
200	116	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
201		simplr 788	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)))
202	191, 201	eqnetrrd 2850	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → 𝑈 ≠ (𝑃‘(𝑁 + 1)))
203	202	necomd 2837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ≠ 𝑈)
204	197, 198, 199, 200, 203	vdgr1b 26431	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 1)
205	196, 204	eqtrd 2644	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 1)
206	205	oveq2d 6565	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
207	206	breq2d 4595	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
208	207	notbid 307	. . . . 5 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
209		2nn 11062	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
210	209	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ)
211		1lt2 11071	. . . . . . . . . . . 12 ⊢ 1 < 2
212	211	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 1 < 2)
213		ndvdsp1 14973	. . . . . . . . . . 11 ⊢ ((((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
214	138, 210, 212, 213	syl3anc 1318	. . . . . . . . . 10 ⊢ (𝜑 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
215	214	con2d 128	. . . . . . . . 9 ⊢ (𝜑 → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) → ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
216		n2dvds1 14942	. . . . . . . . . . . 12 ⊢ ¬ 2 ∥ 1
217		opoe 14925	. . . . . . . . . . . 12 ⊢ (((((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ ∧ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
218	2, 216, 217	mpanr12 717	. . . . . . . . . . 11 ⊢ ((((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ ∧ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
219	218	ex 449	. . . . . . . . . 10 ⊢ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
220	138, 219	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
221	215, 220	impbid 201	. . . . . . . 8 ⊢ (𝜑 → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
222	221, 131	bitrd 267	. . . . . . 7 ⊢ (𝜑 → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
223	222	notbid 307	. . . . . 6 ⊢ (𝜑 → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
224	223	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
225		fvex 6113	. . . . . . 7 ⊢ (𝑃‘𝑁) ∈ V
226	225	eupath2lem2 26505	. . . . . 6 ⊢ (((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
227	226	adantll 746	. . . . 5 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
228	208, 224, 227	3bitrd 293	. . . 4 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘𝑁) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
229		simpr 476	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘(𝑁 + 1)) = 𝑈)
230	229	preq2d 4219	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} = {(𝑃‘𝑁), 𝑈})
231	230	opeq2d 4347	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩ = ⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), 𝑈}⟩)
232	231	sneqd 4137	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩} = {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), 𝑈}⟩})
233	232	oveq2d 6565	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩}) = (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), 𝑈}⟩}))
234	233	fveq1d 6105	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), 𝑈}⟩})‘𝑈))
235	103	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑉 ∈ V)
236	64	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
237	119	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑈 ∈ 𝑉)
238	109	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘𝑁) ∈ 𝑉)
239		simplr 788	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)))
240	239, 229	neeqtrd 2851	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘𝑁) ≠ 𝑈)
241	235, 236, 237, 238, 240	vdgr1c 26432	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), 𝑈}⟩})‘𝑈) = 1)
242	234, 241	eqtrd 2644	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 1)
243	242	oveq2d 6565	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
244	243	breq2d 4595	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
245	244	notbid 307	. . . . 5 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
246	223	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
247		necom 2835	. . . . . . . 8 ⊢ ((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘(𝑁 + 1)) ≠ (𝑃‘𝑁))
248		fvex 6113	. . . . . . . . 9 ⊢ (𝑃‘(𝑁 + 1)) ∈ V
249	248	eupath2lem2 26505	. . . . . . . 8 ⊢ (((𝑃‘(𝑁 + 1)) ≠ (𝑃‘𝑁) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
250	247, 249	sylanb 488	. . . . . . 7 ⊢ (((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
251	250	con1bid 344	. . . . . 6 ⊢ (((𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
252	251	adantll 746	. . . . 5 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
253	245, 246, 252	3bitrd 293	. . . 4 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
254	103	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑉 ∈ V)
255	64	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝐹‘(𝑁 + 1)) ∈ V)
256	119	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑈 ∈ 𝑉)
257	109	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃‘𝑁) ∈ 𝑉)
258		simprl 790	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃‘𝑁) ≠ 𝑈)
259	116	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
260		simprr 792	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃‘(𝑁 + 1)) ≠ 𝑈)
261	254, 255, 256, 257, 258, 259, 260	vdgr1a 26433	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 0)
262	261	oveq2d 6565	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 0))
263	179	addid1d 10115	. . . . . . . . 9 ⊢ (𝜑 → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 0) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
264	263	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 0) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
265	262, 264	eqtrd 2644	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
266	265	breq2d 4595	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
267	266	notbid 307	. . . . 5 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
268	131	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})))
269	258	necomd 2837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑈 ≠ (𝑃‘𝑁))
270	260	necomd 2837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑈 ≠ (𝑃‘(𝑁 + 1)))
271	269, 270	2thd 254	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ≠ (𝑃‘𝑁) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1))))
272		neeq1 2844	. . . . . . . . . 10 ⊢ (𝑈 = (𝑃‘0) → (𝑈 ≠ (𝑃‘𝑁) ↔ (𝑃‘0) ≠ (𝑃‘𝑁)))
273		neeq1 2844	. . . . . . . . . 10 ⊢ (𝑈 = (𝑃‘0) → (𝑈 ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘0) ≠ (𝑃‘(𝑁 + 1))))
274	272, 273	bibi12d 334	. . . . . . . . 9 ⊢ (𝑈 = (𝑃‘0) → ((𝑈 ≠ (𝑃‘𝑁) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1))) ↔ ((𝑃‘0) ≠ (𝑃‘𝑁) ↔ (𝑃‘0) ≠ (𝑃‘(𝑁 + 1)))))
275	271, 274	syl5ibcom 234	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) → ((𝑃‘0) ≠ (𝑃‘𝑁) ↔ (𝑃‘0) ≠ (𝑃‘(𝑁 + 1)))))
276	275	pm5.32rd 670	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃‘𝑁) ∧ 𝑈 = (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ 𝑈 = (𝑃‘0))))
277	269	neneqd 2787	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → ¬ 𝑈 = (𝑃‘𝑁))
278		biorf 419	. . . . . . . . . 10 ⊢ (¬ 𝑈 = (𝑃‘𝑁) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘0))))
279	277, 278	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘0))))
280		orcom 401	. . . . . . . . 9 ⊢ ((𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘0)) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘𝑁)))
281	279, 280	syl6bb 275	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘𝑁))))
282	281	anbi2d 736	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃‘𝑁) ∧ 𝑈 = (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘𝑁)))))
283	270	neneqd 2787	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → ¬ 𝑈 = (𝑃‘(𝑁 + 1)))
284		biorf 419	. . . . . . . . . 10 ⊢ (¬ 𝑈 = (𝑃‘(𝑁 + 1)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘(𝑁 + 1)) ∨ 𝑈 = (𝑃‘0))))
285	283, 284	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘(𝑁 + 1)) ∨ 𝑈 = (𝑃‘0))))
286		orcom 401	. . . . . . . . 9 ⊢ ((𝑈 = (𝑃‘(𝑁 + 1)) ∨ 𝑈 = (𝑃‘0)) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))
287	285, 286	syl6bb 275	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))))
288	287	anbi2d 736	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ 𝑈 = (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
289	276, 282, 288	3bitr3d 297	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃‘𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘𝑁))) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
290		eupath2lem1 26504	. . . . . . 7 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ ((𝑃‘0) ≠ (𝑃‘𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘𝑁)))))
291	256, 290	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ ((𝑃‘0) ≠ (𝑃‘𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘𝑁)))))
292		eupath2lem1 26504	. . . . . . 7 ⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
293	256, 292	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
294	289, 291, 293	3bitr4d 299	. . . . 5 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ∈ if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
295	267, 268, 294	3bitrd 293	. . . 4 ⊢ (((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃‘𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
296	228, 253, 295	pm2.61da2ne 2870	. . 3 ⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
297	190, 296	pm2.61dane 2869	. 2 ⊢ (𝜑 → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
298	123, 297	bitrd 267	1 ⊢ (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 {crab 2900 Vcvv 3173 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 ifcif 4036 {csn 4125 {cpr 4127 ⟨cop 4131 class class class wbr 4583 ran crn 5039 ↾ cres 5040 “ cima 5041 Fn wfn 5799 ⟶wf 5800 –1-1→wf1 5801 –onto→wfo 5802 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 Fincfn 7841 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 < clt 9953 ≤ cle 9954 − cmin 10145 ℕcn 10897 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: eupath2 26507

W3C validator