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 (𝜑𝑁 ∈ ℕ0)
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
StepHypRef Expression
1 imaundi 5464 . . . . . . . . . . 11 (𝐹 “ ((1...𝑁) ∪ {(𝑁 + 1)})) = ((𝐹 “ (1...𝑁)) ∪ (𝐹 “ {(𝑁 + 1)}))
2 1z 11284 . . . . . . . . . . . . 13 1 ∈ ℤ
3 eupath2.5 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ0)
4 nn0uz 11598 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
5 1m1e0 10966 . . . . . . . . . . . . . . . 16 (1 − 1) = 0
65fveq2i 6106 . . . . . . . . . . . . . . 15 (ℤ‘(1 − 1)) = (ℤ‘0)
74, 6eqtr4i 2635 . . . . . . . . . . . . . 14 0 = (ℤ‘(1 − 1))
83, 7syl6eleq 2698 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘(1 − 1)))
9 fzsuc2 12268 . . . . . . . . . . . . 13 ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ‘(1 − 1))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
102, 8, 9sylancr 694 . . . . . . . . . . . 12 (𝜑 → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
1110imaeq2d 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𝐴)
1512, 13, 14syl2anc 691 . . . . . . . . . . . . . 14 (𝜑𝐹:(1...(#‘𝐹))–1-1-onto𝐴)
16 f1ofn 6051 . . . . . . . . . . . . . 14 (𝐹:(1...(#‘𝐹))–1-1-onto𝐴𝐹 Fn (1...(#‘𝐹)))
1715, 16syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 Fn (1...(#‘𝐹)))
18 eupath2.6 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ≤ (#‘𝐹))
19 nn0p1nn 11209 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)
203, 19syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ ℕ)
21 nnuz 11599 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
2220, 21syl6eleq 2698 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
23 eupacl 26496 . . . . . . . . . . . . . . . . 17 (𝐹(𝑉 EulPaths 𝐸)𝑃 → (#‘𝐹) ∈ ℕ0)
2412, 23syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘𝐹) ∈ ℕ0)
2524nn0zd 11356 . . . . . . . . . . . . . . 15 (𝜑 → (#‘𝐹) ∈ ℤ)
26 elfz5 12205 . . . . . . . . . . . . . . 15 (((𝑁 + 1) ∈ (ℤ‘1) ∧ (#‘𝐹) ∈ ℤ) → ((𝑁 + 1) ∈ (1...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
2722, 25, 26syl2anc 691 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 + 1) ∈ (1...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
2818, 27mpbird 246 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ (1...(#‘𝐹)))
29 fnsnfv 6168 . . . . . . . . . . . . 13 ((𝐹 Fn (1...(#‘𝐹)) ∧ (𝑁 + 1) ∈ (1...(#‘𝐹))) → {(𝐹‘(𝑁 + 1))} = (𝐹 “ {(𝑁 + 1)}))
3017, 28, 29syl2anc 691 . . . . . . . . . . . 12 (𝜑 → {(𝐹‘(𝑁 + 1))} = (𝐹 “ {(𝑁 + 1)}))
3130uneq2d 3729 . . . . . . . . . . 11 (𝜑 → ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))}) = ((𝐹 “ (1...𝑁)) ∪ (𝐹 “ {(𝑁 + 1)})))
321, 11, 313eqtr4a 2670 . . . . . . . . . 10 (𝜑 → (𝐹 “ (1...(𝑁 + 1))) = ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))}))
3332reseq2d 5317 . . . . . . . . 9 (𝜑 → (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))) = (𝐸 ↾ ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))})))
34 resundi 5330 . . . . . . . . 9 (𝐸 ↾ ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))})) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ (𝐸 ↾ {(𝐹‘(𝑁 + 1))}))
3533, 34syl6eq 2660 . . . . . . . 8 (𝜑 → (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ (𝐸 ↾ {(𝐹‘(𝑁 + 1))})))
36 f1of 6050 . . . . . . . . . . . . 13 (𝐹:(1...(#‘𝐹))–1-1-onto𝐴𝐹:(1...(#‘𝐹))⟶𝐴)
3715, 36syl 17 . . . . . . . . . . . 12 (𝜑𝐹:(1...(#‘𝐹))⟶𝐴)
3837, 28ffvelrnd 6268 . . . . . . . . . . 11 (𝜑 → (𝐹‘(𝑁 + 1)) ∈ 𝐴)
39 fnressn 6330 . . . . . . . . . . 11 ((𝐸 Fn 𝐴 ∧ (𝐹‘(𝑁 + 1)) ∈ 𝐴) → (𝐸 ↾ {(𝐹‘(𝑁 + 1))}) = {⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩})
4013, 38, 39syl2anc 691 . . . . . . . . . 10 (𝜑 → (𝐸 ↾ {(𝐹‘(𝑁 + 1))}) = {⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩})
41 eupaseg 26500 . . . . . . . . . . . . . 14 ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ (𝑁 + 1) ∈ (1...(#‘𝐹))) → (𝐸‘(𝐹‘(𝑁 + 1))) = {(𝑃‘((𝑁 + 1) − 1)), (𝑃‘(𝑁 + 1))})
4212, 28, 41syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (𝐸‘(𝐹‘(𝑁 + 1))) = {(𝑃‘((𝑁 + 1) − 1)), (𝑃‘(𝑁 + 1))})
433nn0cnd 11230 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℂ)
44 ax-1cn 9873 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
45 pncan 10166 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
4643, 44, 45sylancl 693 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
4746fveq2d 6107 . . . . . . . . . . . . . 14 (𝜑 → (𝑃‘((𝑁 + 1) − 1)) = (𝑃𝑁))
4847preq1d 4218 . . . . . . . . . . . . 13 (𝜑 → {(𝑃‘((𝑁 + 1) − 1)), (𝑃‘(𝑁 + 1))} = {(𝑃𝑁), (𝑃‘(𝑁 + 1))})
4942, 48eqtrd 2644 . . . . . . . . . . . 12 (𝜑 → (𝐸‘(𝐹‘(𝑁 + 1))) = {(𝑃𝑁), (𝑃‘(𝑁 + 1))})
5049opeq2d 4347 . . . . . . . . . . 11 (𝜑 → ⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩ = ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩)
5150sneqd 4137 . . . . . . . . . 10 (𝜑 → {⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩} = {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})
5240, 51eqtrd 2644 . . . . . . . . 9 (𝜑 → (𝐸 ↾ {(𝐹‘(𝑁 + 1))}) = {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})
5352uneq2d 3729 . . . . . . . 8 (𝜑 → ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ (𝐸 ↾ {(𝐹‘(𝑁 + 1))})) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}))
5435, 53eqtrd 2644 . . . . . . 7 (𝜑 → (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}))
5554oveq2d 6565 . . . . . 6 (𝜑 → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1))))) = (𝑉 VDeg ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})))
5655fveq1d 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 𝐹 = 𝐴)
6015, 58, 593syl 18 . . . . . . . 8 (𝜑 → ran 𝐹 = 𝐴)
6157, 60syl5sseq 3616 . . . . . . 7 (𝜑 → (𝐹 “ (1...𝑁)) ⊆ 𝐴)
62 fnssres 5918 . . . . . . 7 ((𝐸 Fn 𝐴 ∧ (𝐹 “ (1...𝑁)) ⊆ 𝐴) → (𝐸 ↾ (𝐹 “ (1...𝑁))) Fn (𝐹 “ (1...𝑁)))
6313, 61, 62syl2anc 691 . . . . . 6 (𝜑 → (𝐸 ↾ (𝐹 “ (1...𝑁))) Fn (𝐹 “ (1...𝑁)))
64 fvex 6113 . . . . . . . 8 (𝐹‘(𝑁 + 1)) ∈ V
65 prex 4836 . . . . . . . 8 {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ∈ V
6664, 65fnsn 5860 . . . . . . 7 {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} Fn {(𝐹‘(𝑁 + 1))}
6766a1i 11 . . . . . 6 (𝜑 → {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} Fn {(𝐹‘(𝑁 + 1))})
68 eupafi 26498 . . . . . . . 8 ((𝐹(𝑉 EulPaths 𝐸)𝑃𝐸 Fn 𝐴) → 𝐴 ∈ Fin)
6912, 13, 68syl2anc 691 . . . . . . 7 (𝜑𝐴 ∈ Fin)
70 ssfi 8065 . . . . . . 7 ((𝐴 ∈ Fin ∧ (𝐹 “ (1...𝑁)) ⊆ 𝐴) → (𝐹 “ (1...𝑁)) ∈ Fin)
7169, 61, 70syl2anc 691 . . . . . 6 (𝜑 → (𝐹 “ (1...𝑁)) ∈ Fin)
72 snfi 7923 . . . . . . 7 {(𝐹‘(𝑁 + 1))} ∈ Fin
7372a1i 11 . . . . . 6 (𝜑 → {(𝐹‘(𝑁 + 1))} ∈ Fin)
743nn0red 11229 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ)
7574ltp1d 10833 . . . . . . . . 9 (𝜑𝑁 < (𝑁 + 1))
76 peano2re 10088 . . . . . . . . . . 11 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
7774, 76syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 + 1) ∈ ℝ)
7874, 77ltnled 10063 . . . . . . . . 9 (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
7975, 78mpbid 221 . . . . . . . 8 (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁)
80 f1of1 6049 . . . . . . . . . . 11 (𝐹:(1...(#‘𝐹))–1-1-onto𝐴𝐹:(1...(#‘𝐹))–1-1𝐴)
8115, 80syl 17 . . . . . . . . . 10 (𝜑𝐹:(1...(#‘𝐹))–1-1𝐴)
823nn0zd 11356 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
8382peano2zd 11361 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ ℤ)
84 eluz2 11569 . . . . . . . . . . . . 13 ((#‘𝐹) ∈ (ℤ‘(𝑁 + 1)) ↔ ((𝑁 + 1) ∈ ℤ ∧ (#‘𝐹) ∈ ℤ ∧ (𝑁 + 1) ≤ (#‘𝐹)))
8583, 25, 18, 84syl3anbrc 1239 . . . . . . . . . . . 12 (𝜑 → (#‘𝐹) ∈ (ℤ‘(𝑁 + 1)))
86 peano2uzr 11619 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ (#‘𝐹) ∈ (ℤ‘(𝑁 + 1))) → (#‘𝐹) ∈ (ℤ𝑁))
8782, 85, 86syl2anc 691 . . . . . . . . . . 11 (𝜑 → (#‘𝐹) ∈ (ℤ𝑁))
88 fzss2 12252 . . . . . . . . . . 11 ((#‘𝐹) ∈ (ℤ𝑁) → (1...𝑁) ⊆ (1...(#‘𝐹)))
8987, 88syl 17 . . . . . . . . . 10 (𝜑 → (1...𝑁) ⊆ (1...(#‘𝐹)))
90 f1elima 6421 . . . . . . . . . 10 ((𝐹:(1...(#‘𝐹))–1-1𝐴 ∧ (𝑁 + 1) ∈ (1...(#‘𝐹)) ∧ (1...𝑁) ⊆ (1...(#‘𝐹))) → ((𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)) ↔ (𝑁 + 1) ∈ (1...𝑁)))
9181, 28, 89, 90syl3anc 1318 . . . . . . . . 9 (𝜑 → ((𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)) ↔ (𝑁 + 1) ∈ (1...𝑁)))
92 elfz5 12205 . . . . . . . . . 10 (((𝑁 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((𝑁 + 1) ∈ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
9322, 82, 92syl2anc 691 . . . . . . . . 9 (𝜑 → ((𝑁 + 1) ∈ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
9491, 93bitrd 267 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁))
9579, 94mtbird 314 . . . . . . 7 (𝜑 → ¬ (𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)))
96 disjsn 4192 . . . . . . 7 (((𝐹 “ (1...𝑁)) ∩ {(𝐹‘(𝑁 + 1))}) = ∅ ↔ ¬ (𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)))
9795, 96sylibr 223 . . . . . 6 (𝜑 → ((𝐹 “ (1...𝑁)) ∩ {(𝐹‘(𝑁 + 1))}) = ∅)
98 eupagra 26493 . . . . . . 7 (𝐹(𝑉 EulPaths 𝐸)𝑃𝑉 UMGrph 𝐸)
99 umgrares 25853 . . . . . . 7 (𝑉 UMGrph 𝐸𝑉 UMGrph (𝐸 ↾ (𝐹 “ (1...𝑁))))
10012, 98, 993syl 18 . . . . . 6 (𝜑𝑉 UMGrph (𝐸 ↾ (𝐹 “ (1...𝑁))))
101 relumgra 25843 . . . . . . . . 9 Rel UMGrph
102101brrelexi 5082 . . . . . . . 8 (𝑉 UMGrph 𝐸𝑉 ∈ V)
10312, 98, 1023syl 18 . . . . . . 7 (𝜑𝑉 ∈ V)
104 eupapf 26499 . . . . . . . . 9 (𝐹(𝑉 EulPaths 𝐸)𝑃𝑃:(0...(#‘𝐹))⟶𝑉)
10512, 104syl 17 . . . . . . . 8 (𝜑𝑃:(0...(#‘𝐹))⟶𝑉)
1063, 4syl6eleq 2698 . . . . . . . . 9 (𝜑𝑁 ∈ (ℤ‘0))
107 elfzuzb 12207 . . . . . . . . 9 (𝑁 ∈ (0...(#‘𝐹)) ↔ (𝑁 ∈ (ℤ‘0) ∧ (#‘𝐹) ∈ (ℤ𝑁)))
108106, 87, 107sylanbrc 695 . . . . . . . 8 (𝜑𝑁 ∈ (0...(#‘𝐹)))
109105, 108ffvelrnd 6268 . . . . . . 7 (𝜑 → (𝑃𝑁) ∈ 𝑉)
110 peano2nn0 11210 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
1113, 110syl 17 . . . . . . . . . . 11 (𝜑 → (𝑁 + 1) ∈ ℕ0)
112111, 4syl6eleq 2698 . . . . . . . . . 10 (𝜑 → (𝑁 + 1) ∈ (ℤ‘0))
113 elfz5 12205 . . . . . . . . . 10 (((𝑁 + 1) ∈ (ℤ‘0) ∧ (#‘𝐹) ∈ ℤ) → ((𝑁 + 1) ∈ (0...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
114112, 25, 113syl2anc 691 . . . . . . . . 9 (𝜑 → ((𝑁 + 1) ∈ (0...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
11518, 114mpbird 246 . . . . . . . 8 (𝜑 → (𝑁 + 1) ∈ (0...(#‘𝐹)))
116105, 115ffvelrnd 6268 . . . . . . 7 (𝜑 → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
117 umgra1 25855 . . . . . . 7 (((𝑉 ∈ V ∧ (𝐹‘(𝑁 + 1)) ∈ 𝐴) ∧ ((𝑃𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉)) → 𝑉 UMGrph {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})
118103, 38, 109, 116, 117syl22anc 1319 . . . . . 6 (𝜑𝑉 UMGrph {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})
119 eupath2.7 . . . . . 6 (𝜑𝑈𝑉)
12063, 67, 71, 73, 97, 100, 118, 119vdgrfiun 26429 . . . . 5 (𝜑 → ((𝑉 VDeg ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}))‘𝑈) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)))
12156, 120eqtrd 2644 . . . 4 (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)))
122121breq2d 4595 . . 3 (𝜑 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
123122notbid 307 . 2 (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
124 fveq2 6103 . . . . . . . . . 10 (𝑥 = 𝑈 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
125124breq2d 4595 . . . . . . . . 9 (𝑥 = 𝑈 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
126125notbid 307 . . . . . . . 8 (𝑥 = 𝑈 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
127126elrab3 3332 . . . . . . 7 (𝑈𝑉 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
128119, 127syl 17 . . . . . 6 (𝜑 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
129 eupath2.8 . . . . . . 7 (𝜑 → {𝑥𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} = if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}))
130129eleq2d 2673 . . . . . 6 (𝜑 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
131128, 130bitr3d 269 . . . . 5 (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
132131adantr 480 . . . 4 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
133 2z 11286 . . . . . . . 8 2 ∈ ℤ
134133a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → 2 ∈ ℤ)
135 vdgrfif 26426 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ (𝐸 ↾ (𝐹 “ (1...𝑁))) Fn (𝐹 “ (1...𝑁)) ∧ (𝐹 “ (1...𝑁)) ∈ Fin) → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁)))):𝑉⟶ℕ0)
136103, 63, 71, 135syl3anc 1318 . . . . . . . . . 10 (𝜑 → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁)))):𝑉⟶ℕ0)
137136, 119ffvelrnd 6268 . . . . . . . . 9 (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℕ0)
138137nn0zd 11356 . . . . . . . 8 (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ)
139138adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ)
140 vdgrfif 26426 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} Fn {(𝐹‘(𝑁 + 1))} ∧ {(𝐹‘(𝑁 + 1))} ∈ Fin) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}):𝑉⟶ℕ0)
141103, 67, 73, 140syl3anc 1318 . . . . . . . . . 10 (𝜑 → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}):𝑉⟶ℕ0)
142141, 119ffvelrnd 6268 . . . . . . . . 9 (𝜑 → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℕ0)
143142nn0zd 11356 . . . . . . . 8 (𝜑 → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℤ)
144143adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℤ)
145 iddvds 14833 . . . . . . . . . 10 (2 ∈ ℤ → 2 ∥ 2)
146133, 145ax-mp 5 . . . . . . . . 9 2 ∥ 2
147 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃𝑁) = 𝑈)
148 simplr 788 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃𝑁) = (𝑃‘(𝑁 + 1)))
149148, 147eqtr3d 2646 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) = 𝑈)
150147, 149preq12d 4220 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, 𝑈})
151 dfsn2 4138 . . . . . . . . . . . . . . 15 {𝑈} = {𝑈, 𝑈}
152150, 151syl6eqr 2662 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {𝑈})
153152opeq2d 4347 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩ = ⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩)
154153sneqd 4137 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} = {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩})
155154oveq2d 6565 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}) = (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩}))
156155fveq1d 6105 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩})‘𝑈))
157103ad2antrr 758 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑉 ∈ V)
15864a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
159119ad2antrr 758 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈𝑉)
160157, 158, 159vdgr1d 26430 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩})‘𝑈) = 2)
161156, 160eqtrd 2644 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 2)
162146, 161syl5breqr 4621 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 2 ∥ ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
163 dvds0 14835 . . . . . . . . . 10 (2 ∈ ℤ → 2 ∥ 0)
164133, 163ax-mp 5 . . . . . . . . 9 2 ∥ 0
165103ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → 𝑉 ∈ V)
16664a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
167119ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → 𝑈𝑉)
168109ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃𝑁) ∈ 𝑉)
169 simpr 476 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃𝑁) ≠ 𝑈)
170116ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
171 simplr 788 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃𝑁) = (𝑃‘(𝑁 + 1)))
172171, 169eqnetrrd 2850 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃‘(𝑁 + 1)) ≠ 𝑈)
173165, 166, 167, 168, 169, 170, 172vdgr1a 26433 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 0)
174164, 173syl5breqr 4621 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → 2 ∥ ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
175162, 174pm2.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...𝑁))))‘𝑈))))
177134, 139, 144, 175, 176syl112anc 1322 . . . . . 6 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))))
178142nn0cnd 11230 . . . . . . . . 9 (𝜑 → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℂ)
179137nn0cnd 11230 . . . . . . . . 9 (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℂ)
180178, 179addcomd 10117 . . . . . . . 8 (𝜑 → (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)))
181180breq2d 4595 . . . . . . 7 (𝜑 → (2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
182181adantr 480 . . . . . 6 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
183177, 182bitrd 267 . . . . 5 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
184183notbid 307 . . . 4 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
185 simpr 476 . . . . . . 7 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (𝑃𝑁) = (𝑃‘(𝑁 + 1)))
186185eqeq2d 2620 . . . . . 6 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑃‘0) = (𝑃𝑁) ↔ (𝑃‘0) = (𝑃‘(𝑁 + 1))))
187185preq2d 4219 . . . . . 6 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → {(𝑃‘0), (𝑃𝑁)} = {(𝑃‘0), (𝑃‘(𝑁 + 1))})
188186, 187ifbieq2d 4061 . . . . 5 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) = if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))
189188eleq2d 2673 . . . 4 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
190132, 184, 1893bitr3d 297 . . 3 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
191 simpr 476 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃𝑁) = 𝑈)
192191preq1d 4218 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, (𝑃‘(𝑁 + 1))})
193192opeq2d 4347 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩ = ⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩)
194193sneqd 4137 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} = {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩})
195194oveq2d 6565 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}) = (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩}))
196195fveq1d 6105 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
197103ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑉 ∈ V)
19864a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
199119ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈𝑉)
200116ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
201 simplr 788 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)))
202191, 201eqnetrrd 2850 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈 ≠ (𝑃‘(𝑁 + 1)))
203202necomd 2837 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ≠ 𝑈)
204197, 198, 199, 200, 203vdgr1b 26431 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 1)
205196, 204eqtrd 2644 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 1)
206205oveq2d 6565 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
207206breq2d 4595 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
208207notbid 307 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
209 2nn 11062 . . . . . . . . . . . 12 2 ∈ ℕ
210209a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℕ)
211 1lt2 11071 . . . . . . . . . . . 12 1 < 2
212211a1i 11 . . . . . . . . . . 11 (𝜑 → 1 < 2)
213 ndvdsp1 14973 . . . . . . . . . . 11 ((((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
214138, 210, 212, 213syl3anc 1318 . . . . . . . . . 10 (𝜑 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
215214con2d 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))
2182, 216, 217mpanr12 717 . . . . . . . . . . 11 ((((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ ∧ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
219218ex 449 . . . . . . . . . 10 (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
220138, 219syl 17 . . . . . . . . 9 (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
221215, 220impbid 201 . . . . . . . 8 (𝜑 → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
222221, 131bitrd 267 . . . . . . 7 (𝜑 → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
223222notbid 307 . . . . . 6 (𝜑 → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
224223ad2antrr 758 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
225 fvex 6113 . . . . . . 7 (𝑃𝑁) ∈ V
226225eupath2lem2 26505 . . . . . 6 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
227226adantll 746 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
228208, 224, 2273bitrd 293 . . . 4 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
229 simpr 476 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘(𝑁 + 1)) = 𝑈)
230229preq2d 4219 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {(𝑃𝑁), 𝑈})
231230opeq2d 4347 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩ = ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩)
232231sneqd 4137 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} = {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩})
233232oveq2d 6565 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}) = (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩}))
234233fveq1d 6105 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩})‘𝑈))
235103ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑉 ∈ V)
23664a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
237119ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑈𝑉)
238109ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ∈ 𝑉)
239 simplr 788 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)))
240239, 229neeqtrd 2851 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ≠ 𝑈)
241235, 236, 237, 238, 240vdgr1c 26432 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩})‘𝑈) = 1)
242234, 241eqtrd 2644 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 1)
243242oveq2d 6565 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
244243breq2d 4595 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
245244notbid 307 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
246223ad2antrr 758 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
247 necom 2835 . . . . . . . 8 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘(𝑁 + 1)) ≠ (𝑃𝑁))
248 fvex 6113 . . . . . . . . 9 (𝑃‘(𝑁 + 1)) ∈ V
249248eupath2lem2 26505 . . . . . . . 8 (((𝑃‘(𝑁 + 1)) ≠ (𝑃𝑁) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
250247, 249sylanb 488 . . . . . . 7 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
251250con1bid 344 . . . . . 6 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
252251adantll 746 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
253245, 246, 2523bitrd 293 . . . 4 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
254103ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑉 ∈ V)
25564a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝐹‘(𝑁 + 1)) ∈ V)
256119ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑈𝑉)
257109ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃𝑁) ∈ 𝑉)
258 simprl 790 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃𝑁) ≠ 𝑈)
259116ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
260 simprr 792 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃‘(𝑁 + 1)) ≠ 𝑈)
261254, 255, 256, 257, 258, 259, 260vdgr1a 26433 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 0)
262261oveq2d 6565 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 0))
263179addid1d 10115 . . . . . . . . 9 (𝜑 → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 0) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
264263ad2antrr 758 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 0) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
265262, 264eqtrd 2644 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
266265breq2d 4595 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
267266notbid 307 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
268131ad2antrr 758 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
269258necomd 2837 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑈 ≠ (𝑃𝑁))
270260necomd 2837 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑈 ≠ (𝑃‘(𝑁 + 1)))
271269, 2702thd 254 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ≠ (𝑃𝑁) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1))))
272 neeq1 2844 . . . . . . . . . 10 (𝑈 = (𝑃‘0) → (𝑈 ≠ (𝑃𝑁) ↔ (𝑃‘0) ≠ (𝑃𝑁)))
273 neeq1 2844 . . . . . . . . . 10 (𝑈 = (𝑃‘0) → (𝑈 ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘0) ≠ (𝑃‘(𝑁 + 1))))
274272, 273bibi12d 334 . . . . . . . . 9 (𝑈 = (𝑃‘0) → ((𝑈 ≠ (𝑃𝑁) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1))) ↔ ((𝑃‘0) ≠ (𝑃𝑁) ↔ (𝑃‘0) ≠ (𝑃‘(𝑁 + 1)))))
275271, 274syl5ibcom 234 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) → ((𝑃‘0) ≠ (𝑃𝑁) ↔ (𝑃‘0) ≠ (𝑃‘(𝑁 + 1)))))
276275pm5.32rd 670 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃𝑁) ∧ 𝑈 = (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ 𝑈 = (𝑃‘0))))
277269neneqd 2787 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → ¬ 𝑈 = (𝑃𝑁))
278 biorf 419 . . . . . . . . . 10 𝑈 = (𝑃𝑁) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘0))))
279277, 278syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘0))))
280 orcom 401 . . . . . . . . 9 ((𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘0)) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁)))
281279, 280syl6bb 275 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁))))
282281anbi2d 736 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃𝑁) ∧ 𝑈 = (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁)))))
283270neneqd 2787 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → ¬ 𝑈 = (𝑃‘(𝑁 + 1)))
284 biorf 419 . . . . . . . . . 10 𝑈 = (𝑃‘(𝑁 + 1)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘(𝑁 + 1)) ∨ 𝑈 = (𝑃‘0))))
285283, 284syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘(𝑁 + 1)) ∨ 𝑈 = (𝑃‘0))))
286 orcom 401 . . . . . . . . 9 ((𝑈 = (𝑃‘(𝑁 + 1)) ∨ 𝑈 = (𝑃‘0)) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))
287285, 286syl6bb 275 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))))
288287anbi2d 736 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ 𝑈 = (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
289276, 282, 2883bitr3d 297 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁))) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
290 eupath2lem1 26504 . . . . . . 7 (𝑈𝑉 → (𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ ((𝑃‘0) ≠ (𝑃𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁)))))
291256, 290syl 17 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ ((𝑃‘0) ≠ (𝑃𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁)))))
292 eupath2lem1 26504 . . . . . . 7 (𝑈𝑉 → (𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
293256, 292syl 17 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
294289, 291, 2933bitr4d 299 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
295267, 268, 2943bitrd 293 . . . 4 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
296228, 253, 295pm2.61da2ne 2870 . . 3 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
297190, 296pm2.61dane 2869 . 2 (𝜑 → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
298123, 297bitrd 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  ℕ0cn0 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
 Copyright terms: Public domain W3C validator