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

Theorem eupath2lem3 26269
Description: Lemma for eupath2 26270. (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 5447 . . . . . . . . . . 11 (𝐹 “ ((1...𝑁) ∪ {(𝑁 + 1)})) = ((𝐹 “ (1...𝑁)) ∪ (𝐹 “ {(𝑁 + 1)}))
2 1z 11237 . . . . . . . . . . . . 13 1 ∈ ℤ
3 eupath2.5 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ0)
4 nn0uz 11551 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
5 1m1e0 10933 . . . . . . . . . . . . . . . 16 (1 − 1) = 0
65fveq2i 6088 . . . . . . . . . . . . . . 15 (ℤ‘(1 − 1)) = (ℤ‘0)
74, 6eqtr4i 2631 . . . . . . . . . . . . . 14 0 = (ℤ‘(1 − 1))
83, 7syl6eleq 2694 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘(1 − 1)))
9 fzsuc2 12220 . . . . . . . . . . . . 13 ((1 ∈ ℤ ∧ 𝑁 ∈ (ℤ‘(1 − 1))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
102, 8, 9sylancr 693 . . . . . . . . . . . 12 (𝜑 → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)}))
1110imaeq2d 5369 . . . . . . . . . . 11 (𝜑 → (𝐹 “ (1...(𝑁 + 1))) = (𝐹 “ ((1...𝑁) ∪ {(𝑁 + 1)})))
12 eupath2.3 . . . . . . . . . . . . . . 15 (𝜑𝐹(𝑉 EulPaths 𝐸)𝑃)
13 eupath2.1 . . . . . . . . . . . . . . 15 (𝜑𝐸 Fn 𝐴)
14 eupaf1o 26260 . . . . . . . . . . . . . . 15 ((𝐹(𝑉 EulPaths 𝐸)𝑃𝐸 Fn 𝐴) → 𝐹:(1...(#‘𝐹))–1-1-onto𝐴)
1512, 13, 14syl2anc 690 . . . . . . . . . . . . . 14 (𝜑𝐹:(1...(#‘𝐹))–1-1-onto𝐴)
16 f1ofn 6033 . . . . . . . . . . . . . 14 (𝐹:(1...(#‘𝐹))–1-1-onto𝐴𝐹 Fn (1...(#‘𝐹)))
1715, 16syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 Fn (1...(#‘𝐹)))
18 eupath2.6 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + 1) ≤ (#‘𝐹))
19 nn0p1nn 11176 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)
203, 19syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ ℕ)
21 nnuz 11552 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
2220, 21syl6eleq 2694 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
23 eupacl 26259 . . . . . . . . . . . . . . . . 17 (𝐹(𝑉 EulPaths 𝐸)𝑃 → (#‘𝐹) ∈ ℕ0)
2412, 23syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘𝐹) ∈ ℕ0)
2524nn0zd 11309 . . . . . . . . . . . . . . 15 (𝜑 → (#‘𝐹) ∈ ℤ)
26 elfz5 12157 . . . . . . . . . . . . . . 15 (((𝑁 + 1) ∈ (ℤ‘1) ∧ (#‘𝐹) ∈ ℤ) → ((𝑁 + 1) ∈ (1...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
2722, 25, 26syl2anc 690 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁 + 1) ∈ (1...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
2818, 27mpbird 245 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ (1...(#‘𝐹)))
29 fnsnfv 6150 . . . . . . . . . . . . 13 ((𝐹 Fn (1...(#‘𝐹)) ∧ (𝑁 + 1) ∈ (1...(#‘𝐹))) → {(𝐹‘(𝑁 + 1))} = (𝐹 “ {(𝑁 + 1)}))
3017, 28, 29syl2anc 690 . . . . . . . . . . . 12 (𝜑 → {(𝐹‘(𝑁 + 1))} = (𝐹 “ {(𝑁 + 1)}))
3130uneq2d 3725 . . . . . . . . . . 11 (𝜑 → ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))}) = ((𝐹 “ (1...𝑁)) ∪ (𝐹 “ {(𝑁 + 1)})))
321, 11, 313eqtr4a 2666 . . . . . . . . . 10 (𝜑 → (𝐹 “ (1...(𝑁 + 1))) = ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))}))
3332reseq2d 5301 . . . . . . . . 9 (𝜑 → (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))) = (𝐸 ↾ ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))})))
34 resundi 5314 . . . . . . . . 9 (𝐸 ↾ ((𝐹 “ (1...𝑁)) ∪ {(𝐹‘(𝑁 + 1))})) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ (𝐸 ↾ {(𝐹‘(𝑁 + 1))}))
3533, 34syl6eq 2656 . . . . . . . 8 (𝜑 → (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ (𝐸 ↾ {(𝐹‘(𝑁 + 1))})))
36 f1of 6032 . . . . . . . . . . . . 13 (𝐹:(1...(#‘𝐹))–1-1-onto𝐴𝐹:(1...(#‘𝐹))⟶𝐴)
3715, 36syl 17 . . . . . . . . . . . 12 (𝜑𝐹:(1...(#‘𝐹))⟶𝐴)
3837, 28ffvelrnd 6250 . . . . . . . . . . 11 (𝜑 → (𝐹‘(𝑁 + 1)) ∈ 𝐴)
39 fnressn 6305 . . . . . . . . . . 11 ((𝐸 Fn 𝐴 ∧ (𝐹‘(𝑁 + 1)) ∈ 𝐴) → (𝐸 ↾ {(𝐹‘(𝑁 + 1))}) = {⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩})
4013, 38, 39syl2anc 690 . . . . . . . . . 10 (𝜑 → (𝐸 ↾ {(𝐹‘(𝑁 + 1))}) = {⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩})
41 eupaseg 26263 . . . . . . . . . . . . . 14 ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ (𝑁 + 1) ∈ (1...(#‘𝐹))) → (𝐸‘(𝐹‘(𝑁 + 1))) = {(𝑃‘((𝑁 + 1) − 1)), (𝑃‘(𝑁 + 1))})
4212, 28, 41syl2anc 690 . . . . . . . . . . . . 13 (𝜑 → (𝐸‘(𝐹‘(𝑁 + 1))) = {(𝑃‘((𝑁 + 1) − 1)), (𝑃‘(𝑁 + 1))})
433nn0cnd 11197 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℂ)
44 ax-1cn 9847 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
45 pncan 10135 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
4643, 44, 45sylancl 692 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
4746fveq2d 6089 . . . . . . . . . . . . . 14 (𝜑 → (𝑃‘((𝑁 + 1) − 1)) = (𝑃𝑁))
4847preq1d 4214 . . . . . . . . . . . . 13 (𝜑 → {(𝑃‘((𝑁 + 1) − 1)), (𝑃‘(𝑁 + 1))} = {(𝑃𝑁), (𝑃‘(𝑁 + 1))})
4942, 48eqtrd 2640 . . . . . . . . . . . 12 (𝜑 → (𝐸‘(𝐹‘(𝑁 + 1))) = {(𝑃𝑁), (𝑃‘(𝑁 + 1))})
5049opeq2d 4338 . . . . . . . . . . 11 (𝜑 → ⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩ = ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩)
5150sneqd 4133 . . . . . . . . . 10 (𝜑 → {⟨(𝐹‘(𝑁 + 1)), (𝐸‘(𝐹‘(𝑁 + 1)))⟩} = {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})
5240, 51eqtrd 2640 . . . . . . . . 9 (𝜑 → (𝐸 ↾ {(𝐹‘(𝑁 + 1))}) = {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})
5352uneq2d 3725 . . . . . . . 8 (𝜑 → ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ (𝐸 ↾ {(𝐹‘(𝑁 + 1))})) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}))
5435, 53eqtrd 2640 . . . . . . 7 (𝜑 → (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))) = ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}))
5554oveq2d 6540 . . . . . 6 (𝜑 → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1))))) = (𝑉 VDeg ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})))
5655fveq1d 6087 . . . . 5 (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) = ((𝑉 VDeg ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}))‘𝑈))
57 imassrn 5380 . . . . . . . 8 (𝐹 “ (1...𝑁)) ⊆ ran 𝐹
58 f1ofo 6039 . . . . . . . . 9 (𝐹:(1...(#‘𝐹))–1-1-onto𝐴𝐹:(1...(#‘𝐹))–onto𝐴)
59 forn 6013 . . . . . . . . 9 (𝐹:(1...(#‘𝐹))–onto𝐴 → ran 𝐹 = 𝐴)
6015, 58, 593syl 18 . . . . . . . 8 (𝜑 → ran 𝐹 = 𝐴)
6157, 60syl5sseq 3612 . . . . . . 7 (𝜑 → (𝐹 “ (1...𝑁)) ⊆ 𝐴)
62 fnssres 5901 . . . . . . 7 ((𝐸 Fn 𝐴 ∧ (𝐹 “ (1...𝑁)) ⊆ 𝐴) → (𝐸 ↾ (𝐹 “ (1...𝑁))) Fn (𝐹 “ (1...𝑁)))
6313, 61, 62syl2anc 690 . . . . . 6 (𝜑 → (𝐸 ↾ (𝐹 “ (1...𝑁))) Fn (𝐹 “ (1...𝑁)))
64 fvex 6095 . . . . . . . 8 (𝐹‘(𝑁 + 1)) ∈ V
65 prex 4828 . . . . . . . 8 {(𝑃𝑁), (𝑃‘(𝑁 + 1))} ∈ V
6664, 65fnsn 5843 . . . . . . 7 {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} Fn {(𝐹‘(𝑁 + 1))}
6766a1i 11 . . . . . 6 (𝜑 → {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} Fn {(𝐹‘(𝑁 + 1))})
68 eupafi 26261 . . . . . . . 8 ((𝐹(𝑉 EulPaths 𝐸)𝑃𝐸 Fn 𝐴) → 𝐴 ∈ Fin)
6912, 13, 68syl2anc 690 . . . . . . 7 (𝜑𝐴 ∈ Fin)
70 ssfi 8039 . . . . . . 7 ((𝐴 ∈ Fin ∧ (𝐹 “ (1...𝑁)) ⊆ 𝐴) → (𝐹 “ (1...𝑁)) ∈ Fin)
7169, 61, 70syl2anc 690 . . . . . 6 (𝜑 → (𝐹 “ (1...𝑁)) ∈ Fin)
72 snfi 7897 . . . . . . 7 {(𝐹‘(𝑁 + 1))} ∈ Fin
7372a1i 11 . . . . . 6 (𝜑 → {(𝐹‘(𝑁 + 1))} ∈ Fin)
743nn0red 11196 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ)
7574ltp1d 10800 . . . . . . . . 9 (𝜑𝑁 < (𝑁 + 1))
76 peano2re 10057 . . . . . . . . . . 11 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
7774, 76syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 + 1) ∈ ℝ)
7874, 77ltnled 10032 . . . . . . . . 9 (𝜑 → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
7975, 78mpbid 220 . . . . . . . 8 (𝜑 → ¬ (𝑁 + 1) ≤ 𝑁)
80 f1of1 6031 . . . . . . . . . . 11 (𝐹:(1...(#‘𝐹))–1-1-onto𝐴𝐹:(1...(#‘𝐹))–1-1𝐴)
8115, 80syl 17 . . . . . . . . . 10 (𝜑𝐹:(1...(#‘𝐹))–1-1𝐴)
823nn0zd 11309 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
8382peano2zd 11314 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ ℤ)
84 eluz2 11522 . . . . . . . . . . . . 13 ((#‘𝐹) ∈ (ℤ‘(𝑁 + 1)) ↔ ((𝑁 + 1) ∈ ℤ ∧ (#‘𝐹) ∈ ℤ ∧ (𝑁 + 1) ≤ (#‘𝐹)))
8583, 25, 18, 84syl3anbrc 1238 . . . . . . . . . . . 12 (𝜑 → (#‘𝐹) ∈ (ℤ‘(𝑁 + 1)))
86 peano2uzr 11572 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ (#‘𝐹) ∈ (ℤ‘(𝑁 + 1))) → (#‘𝐹) ∈ (ℤ𝑁))
8782, 85, 86syl2anc 690 . . . . . . . . . . 11 (𝜑 → (#‘𝐹) ∈ (ℤ𝑁))
88 fzss2 12204 . . . . . . . . . . 11 ((#‘𝐹) ∈ (ℤ𝑁) → (1...𝑁) ⊆ (1...(#‘𝐹)))
8987, 88syl 17 . . . . . . . . . 10 (𝜑 → (1...𝑁) ⊆ (1...(#‘𝐹)))
90 f1elima 6396 . . . . . . . . . 10 ((𝐹:(1...(#‘𝐹))–1-1𝐴 ∧ (𝑁 + 1) ∈ (1...(#‘𝐹)) ∧ (1...𝑁) ⊆ (1...(#‘𝐹))) → ((𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)) ↔ (𝑁 + 1) ∈ (1...𝑁)))
9181, 28, 89, 90syl3anc 1317 . . . . . . . . 9 (𝜑 → ((𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)) ↔ (𝑁 + 1) ∈ (1...𝑁)))
92 elfz5 12157 . . . . . . . . . 10 (((𝑁 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((𝑁 + 1) ∈ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
9322, 82, 92syl2anc 690 . . . . . . . . 9 (𝜑 → ((𝑁 + 1) ∈ (1...𝑁) ↔ (𝑁 + 1) ≤ 𝑁))
9491, 93bitrd 266 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)) ↔ (𝑁 + 1) ≤ 𝑁))
9579, 94mtbird 313 . . . . . . 7 (𝜑 → ¬ (𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)))
96 disjsn 4188 . . . . . . 7 (((𝐹 “ (1...𝑁)) ∩ {(𝐹‘(𝑁 + 1))}) = ∅ ↔ ¬ (𝐹‘(𝑁 + 1)) ∈ (𝐹 “ (1...𝑁)))
9795, 96sylibr 222 . . . . . 6 (𝜑 → ((𝐹 “ (1...𝑁)) ∩ {(𝐹‘(𝑁 + 1))}) = ∅)
98 eupagra 26256 . . . . . . 7 (𝐹(𝑉 EulPaths 𝐸)𝑃𝑉 UMGrph 𝐸)
99 umgrares 25616 . . . . . . 7 (𝑉 UMGrph 𝐸𝑉 UMGrph (𝐸 ↾ (𝐹 “ (1...𝑁))))
10012, 98, 993syl 18 . . . . . 6 (𝜑𝑉 UMGrph (𝐸 ↾ (𝐹 “ (1...𝑁))))
101 relumgra 25606 . . . . . . . . 9 Rel UMGrph
102101brrelexi 5069 . . . . . . . 8 (𝑉 UMGrph 𝐸𝑉 ∈ V)
10312, 98, 1023syl 18 . . . . . . 7 (𝜑𝑉 ∈ V)
104 eupapf 26262 . . . . . . . . 9 (𝐹(𝑉 EulPaths 𝐸)𝑃𝑃:(0...(#‘𝐹))⟶𝑉)
10512, 104syl 17 . . . . . . . 8 (𝜑𝑃:(0...(#‘𝐹))⟶𝑉)
1063, 4syl6eleq 2694 . . . . . . . . 9 (𝜑𝑁 ∈ (ℤ‘0))
107 elfzuzb 12159 . . . . . . . . 9 (𝑁 ∈ (0...(#‘𝐹)) ↔ (𝑁 ∈ (ℤ‘0) ∧ (#‘𝐹) ∈ (ℤ𝑁)))
108106, 87, 107sylanbrc 694 . . . . . . . 8 (𝜑𝑁 ∈ (0...(#‘𝐹)))
109105, 108ffvelrnd 6250 . . . . . . 7 (𝜑 → (𝑃𝑁) ∈ 𝑉)
110 peano2nn0 11177 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
1113, 110syl 17 . . . . . . . . . . 11 (𝜑 → (𝑁 + 1) ∈ ℕ0)
112111, 4syl6eleq 2694 . . . . . . . . . 10 (𝜑 → (𝑁 + 1) ∈ (ℤ‘0))
113 elfz5 12157 . . . . . . . . . 10 (((𝑁 + 1) ∈ (ℤ‘0) ∧ (#‘𝐹) ∈ ℤ) → ((𝑁 + 1) ∈ (0...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
114112, 25, 113syl2anc 690 . . . . . . . . 9 (𝜑 → ((𝑁 + 1) ∈ (0...(#‘𝐹)) ↔ (𝑁 + 1) ≤ (#‘𝐹)))
11518, 114mpbird 245 . . . . . . . 8 (𝜑 → (𝑁 + 1) ∈ (0...(#‘𝐹)))
116105, 115ffvelrnd 6250 . . . . . . 7 (𝜑 → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
117 umgra1 25618 . . . . . . 7 (((𝑉 ∈ V ∧ (𝐹‘(𝑁 + 1)) ∈ 𝐴) ∧ ((𝑃𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉)) → 𝑉 UMGrph {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})
118103, 38, 109, 116, 117syl22anc 1318 . . . . . 6 (𝜑𝑉 UMGrph {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})
119 eupath2.7 . . . . . 6 (𝜑𝑈𝑉)
12063, 67, 71, 73, 97, 100, 118, 119vdgrfiun 26192 . . . . 5 (𝜑 → ((𝑉 VDeg ((𝐸 ↾ (𝐹 “ (1...𝑁))) ∪ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}))‘𝑈) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)))
12156, 120eqtrd 2640 . . . 4 (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)))
122121breq2d 4586 . . 3 (𝜑 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
123122notbid 306 . 2 (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
124 fveq2 6085 . . . . . . . . . 10 (𝑥 = 𝑈 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
125124breq2d 4586 . . . . . . . . 9 (𝑥 = 𝑈 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
126125notbid 306 . . . . . . . 8 (𝑥 = 𝑈 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
127126elrab3 3328 . . . . . . 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 2669 . . . . . 6 (𝜑 → (𝑈 ∈ {𝑥𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
131128, 130bitr3d 268 . . . . 5 (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
132131adantr 479 . . . 4 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
133 2z 11239 . . . . . . . 8 2 ∈ ℤ
134133a1i 11 . . . . . . 7 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → 2 ∈ ℤ)
135 vdgrfif 26189 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ (𝐸 ↾ (𝐹 “ (1...𝑁))) Fn (𝐹 “ (1...𝑁)) ∧ (𝐹 “ (1...𝑁)) ∈ Fin) → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁)))):𝑉⟶ℕ0)
136103, 63, 71, 135syl3anc 1317 . . . . . . . . . 10 (𝜑 → (𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁)))):𝑉⟶ℕ0)
137136, 119ffvelrnd 6250 . . . . . . . . 9 (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℕ0)
138137nn0zd 11309 . . . . . . . 8 (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ)
139138adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ)
140 vdgrfif 26189 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} Fn {(𝐹‘(𝑁 + 1))} ∧ {(𝐹‘(𝑁 + 1))} ∈ Fin) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}):𝑉⟶ℕ0)
141103, 67, 73, 140syl3anc 1317 . . . . . . . . . 10 (𝜑 → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}):𝑉⟶ℕ0)
142141, 119ffvelrnd 6250 . . . . . . . . 9 (𝜑 → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℕ0)
143142nn0zd 11309 . . . . . . . 8 (𝜑 → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℤ)
144143adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℤ)
145 iddvds 14776 . . . . . . . . . 10 (2 ∈ ℤ → 2 ∥ 2)
146133, 145ax-mp 5 . . . . . . . . 9 2 ∥ 2
147 simpr 475 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃𝑁) = 𝑈)
148 simplr 787 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃𝑁) = (𝑃‘(𝑁 + 1)))
149148, 147eqtr3d 2642 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) = 𝑈)
150147, 149preq12d 4216 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, 𝑈})
151 dfsn2 4134 . . . . . . . . . . . . . . 15 {𝑈} = {𝑈, 𝑈}
152150, 151syl6eqr 2658 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {𝑈})
153152opeq2d 4338 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩ = ⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩)
154153sneqd 4133 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} = {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩})
155154oveq2d 6540 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}) = (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩}))
156155fveq1d 6087 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩})‘𝑈))
157103ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑉 ∈ V)
15864a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
159119ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈𝑉)
160157, 158, 159vdgr1d 26193 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈}⟩})‘𝑈) = 2)
161156, 160eqtrd 2640 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 2)
162146, 161syl5breqr 4612 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 2 ∥ ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
163 dvds0 14778 . . . . . . . . . 10 (2 ∈ ℤ → 2 ∥ 0)
164133, 163ax-mp 5 . . . . . . . . 9 2 ∥ 0
165103ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → 𝑉 ∈ V)
16664a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
167119ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → 𝑈𝑉)
168109ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃𝑁) ∈ 𝑉)
169 simpr 475 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃𝑁) ≠ 𝑈)
170116ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
171 simplr 787 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃𝑁) = (𝑃‘(𝑁 + 1)))
172171, 169eqnetrrd 2846 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → (𝑃‘(𝑁 + 1)) ≠ 𝑈)
173165, 166, 167, 168, 169, 170, 172vdgr1a 26196 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 0)
174164, 173syl5breqr 4612 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) ≠ 𝑈) → 2 ∥ ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
175162, 174pm2.61dane 2865 . . . . . . 7 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → 2 ∥ ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
176 dvdsadd2b 14809 . . . . . . 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 1321 . . . . . 6 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))))
178142nn0cnd 11197 . . . . . . . . 9 (𝜑 → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) ∈ ℂ)
179137nn0cnd 11197 . . . . . . . . 9 (𝜑 → ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℂ)
180178, 179addcomd 10086 . . . . . . . 8 (𝜑 → (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)))
181180breq2d 4586 . . . . . . 7 (𝜑 → (2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
182181adantr 479 . . . . . 6 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ (((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) + ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
183177, 182bitrd 266 . . . . 5 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
184183notbid 306 . . . 4 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈))))
185 simpr 475 . . . . . . 7 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (𝑃𝑁) = (𝑃‘(𝑁 + 1)))
186185eqeq2d 2616 . . . . . 6 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → ((𝑃‘0) = (𝑃𝑁) ↔ (𝑃‘0) = (𝑃‘(𝑁 + 1))))
187185preq2d 4215 . . . . . 6 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → {(𝑃‘0), (𝑃𝑁)} = {(𝑃‘0), (𝑃‘(𝑁 + 1))})
188186, 187ifbieq2d 4057 . . . . 5 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) = if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))
189188eleq2d 2669 . . . 4 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
190132, 184, 1893bitr3d 296 . . 3 ((𝜑 ∧ (𝑃𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
191 simpr 475 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃𝑁) = 𝑈)
192191preq1d 4214 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {𝑈, (𝑃‘(𝑁 + 1))})
193192opeq2d 4338 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩ = ⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩)
194193sneqd 4133 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} = {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩})
195194oveq2d 6540 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}) = (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩}))
196195fveq1d 6087 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩})‘𝑈))
197103ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑉 ∈ V)
19864a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
199119ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈𝑉)
200116ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
201 simplr 787 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)))
202191, 201eqnetrrd 2846 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → 𝑈 ≠ (𝑃‘(𝑁 + 1)))
203202necomd 2833 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (𝑃‘(𝑁 + 1)) ≠ 𝑈)
204197, 198, 199, 200, 203vdgr1b 26194 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {𝑈, (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 1)
205196, 204eqtrd 2640 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 1)
206205oveq2d 6540 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
207206breq2d 4586 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
208207notbid 306 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
209 2nn 11029 . . . . . . . . . . . 12 2 ∈ ℕ
210209a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℕ)
211 1lt2 11038 . . . . . . . . . . . 12 1 < 2
212211a1i 11 . . . . . . . . . . 11 (𝜑 → 1 < 2)
213 ndvdsp1 14916 . . . . . . . . . . 11 ((((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2) → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
214138, 210, 212, 213syl3anc 1317 . . . . . . . . . 10 (𝜑 → (2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
215214con2d 127 . . . . . . . . 9 (𝜑 → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) → ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
216 n2dvds1 14885 . . . . . . . . . . . 12 ¬ 2 ∥ 1
217 opoe 14868 . . . . . . . . . . . 12 (((((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ ∧ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) ∧ (1 ∈ ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
2182, 216, 217mpanr12 716 . . . . . . . . . . 11 ((((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ ∧ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
219218ex 448 . . . . . . . . . 10 (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ∈ ℤ → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
220138, 219syl 17 . . . . . . . . 9 (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) → 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
221215, 220impbid 200 . . . . . . . 8 (𝜑 → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
222221, 131bitrd 266 . . . . . . 7 (𝜑 → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
223222notbid 306 . . . . . 6 (𝜑 → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
224223ad2antrr 757 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
225 fvex 6095 . . . . . . 7 (𝑃𝑁) ∈ V
226225eupath2lem2 26268 . . . . . 6 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
227226adantll 745 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
228208, 224, 2273bitrd 292 . . . 4 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃𝑁) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
229 simpr 475 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃‘(𝑁 + 1)) = 𝑈)
230229preq2d 4215 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {(𝑃𝑁), (𝑃‘(𝑁 + 1))} = {(𝑃𝑁), 𝑈})
231230opeq2d 4338 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩ = ⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩)
232231sneqd 4133 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩} = {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩})
233232oveq2d 6540 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩}) = (𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩}))
234233fveq1d 6087 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩})‘𝑈))
235103ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑉 ∈ V)
23664a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝐹‘(𝑁 + 1)) ∈ V)
237119ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → 𝑈𝑉)
238109ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ∈ 𝑉)
239 simplr 787 . . . . . . . . . . 11 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)))
240239, 229neeqtrd 2847 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (𝑃𝑁) ≠ 𝑈)
241235, 236, 237, 238, 240vdgr1c 26195 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), 𝑈}⟩})‘𝑈) = 1)
242234, 241eqtrd 2640 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 1)
243242oveq2d 6540 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1))
244243breq2d 4586 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
245244notbid 306 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ ¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1)))
246223ad2antrr 757 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 1) ↔ ¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
247 necom 2831 . . . . . . . 8 ((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘(𝑁 + 1)) ≠ (𝑃𝑁))
248 fvex 6095 . . . . . . . . 9 (𝑃‘(𝑁 + 1)) ∈ V
249248eupath2lem2 26268 . . . . . . . 8 (((𝑃‘(𝑁 + 1)) ≠ (𝑃𝑁) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
250247, 249sylanb 487 . . . . . . 7 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
251250con1bid 343 . . . . . 6 (((𝑃𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
252251adantll 745 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
253245, 246, 2523bitrd 292 . . . 4 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ (𝑃‘(𝑁 + 1)) = 𝑈) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
254103ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑉 ∈ V)
25564a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝐹‘(𝑁 + 1)) ∈ V)
256119ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑈𝑉)
257109ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃𝑁) ∈ 𝑉)
258 simprl 789 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃𝑁) ≠ 𝑈)
259116ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃‘(𝑁 + 1)) ∈ 𝑉)
260 simprr 791 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑃‘(𝑁 + 1)) ≠ 𝑈)
261254, 255, 256, 257, 258, 259, 260vdgr1a 26196 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈) = 0)
262261oveq2d 6540 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 0))
263179addid1d 10084 . . . . . . . . 9 (𝜑 → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 0) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
264263ad2antrr 757 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + 0) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
265262, 264eqtrd 2640 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) = ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈))
266265breq2d 4586 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
267266notbid 306 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈)))
268131ad2antrr 757 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)})))
269258necomd 2833 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑈 ≠ (𝑃𝑁))
270260necomd 2833 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → 𝑈 ≠ (𝑃‘(𝑁 + 1)))
271269, 2702thd 253 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ≠ (𝑃𝑁) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1))))
272 neeq1 2840 . . . . . . . . . 10 (𝑈 = (𝑃‘0) → (𝑈 ≠ (𝑃𝑁) ↔ (𝑃‘0) ≠ (𝑃𝑁)))
273 neeq1 2840 . . . . . . . . . 10 (𝑈 = (𝑃‘0) → (𝑈 ≠ (𝑃‘(𝑁 + 1)) ↔ (𝑃‘0) ≠ (𝑃‘(𝑁 + 1))))
274272, 273bibi12d 333 . . . . . . . . 9 (𝑈 = (𝑃‘0) → ((𝑈 ≠ (𝑃𝑁) ↔ 𝑈 ≠ (𝑃‘(𝑁 + 1))) ↔ ((𝑃‘0) ≠ (𝑃𝑁) ↔ (𝑃‘0) ≠ (𝑃‘(𝑁 + 1)))))
275271, 274syl5ibcom 233 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) → ((𝑃‘0) ≠ (𝑃𝑁) ↔ (𝑃‘0) ≠ (𝑃‘(𝑁 + 1)))))
276275pm5.32rd 669 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃𝑁) ∧ 𝑈 = (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ 𝑈 = (𝑃‘0))))
277269neneqd 2783 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → ¬ 𝑈 = (𝑃𝑁))
278 biorf 418 . . . . . . . . . 10 𝑈 = (𝑃𝑁) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘0))))
279277, 278syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘0))))
280 orcom 400 . . . . . . . . 9 ((𝑈 = (𝑃𝑁) ∨ 𝑈 = (𝑃‘0)) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁)))
281279, 280syl6bb 274 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁))))
282281anbi2d 735 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃𝑁) ∧ 𝑈 = (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁)))))
283270neneqd 2783 . . . . . . . . . 10 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → ¬ 𝑈 = (𝑃‘(𝑁 + 1)))
284 biorf 418 . . . . . . . . . 10 𝑈 = (𝑃‘(𝑁 + 1)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘(𝑁 + 1)) ∨ 𝑈 = (𝑃‘0))))
285283, 284syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘(𝑁 + 1)) ∨ 𝑈 = (𝑃‘0))))
286 orcom 400 . . . . . . . . 9 ((𝑈 = (𝑃‘(𝑁 + 1)) ∨ 𝑈 = (𝑃‘0)) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))
287285, 286syl6bb 274 . . . . . . . 8 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 = (𝑃‘0) ↔ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))))
288287anbi2d 735 . . . . . . 7 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ 𝑈 = (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
289276, 282, 2883bitr3d 296 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (((𝑃‘0) ≠ (𝑃𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁))) ↔ ((𝑃‘0) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃‘(𝑁 + 1))))))
290 eupath2lem1 26267 . . . . . . 7 (𝑈𝑉 → (𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ ((𝑃‘0) ≠ (𝑃𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁)))))
291256, 290syl 17 . . . . . 6 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ ((𝑃‘0) ≠ (𝑃𝑁) ∧ (𝑈 = (𝑃‘0) ∨ 𝑈 = (𝑃𝑁)))))
292 eupath2lem1 26267 . . . . . . 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 298 . . . . 5 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (𝑈 ∈ if((𝑃‘0) = (𝑃𝑁), ∅, {(𝑃‘0), (𝑃𝑁)}) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
295267, 268, 2943bitrd 292 . . . 4 (((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) ∧ ((𝑃𝑁) ≠ 𝑈 ∧ (𝑃‘(𝑁 + 1)) ≠ 𝑈)) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
296228, 253, 295pm2.61da2ne 2866 . . 3 ((𝜑 ∧ (𝑃𝑁) ≠ (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
297190, 296pm2.61dane 2865 . 2 (𝜑 → (¬ 2 ∥ (((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑈) + ((𝑉 VDeg {⟨(𝐹‘(𝑁 + 1)), {(𝑃𝑁), (𝑃‘(𝑁 + 1))}⟩})‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
298123, 297bitrd 266 1 (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1976  wne 2776  {crab 2896  Vcvv 3169  cun 3534  cin 3535  wss 3536  c0 3870  ifcif 4032  {csn 4121  {cpr 4123  cop 4127   class class class wbr 4574  ran crn 5026  cres 5027  cima 5028   Fn wfn 5782  wf 5783  1-1wf1 5784  ontowfo 5785  1-1-ontowf1o 5786  cfv 5787  (class class class)co 6524  Fincfn 7815  cc 9787  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   < clt 9927  cle 9928  cmin 10114  cn 10864  2c2 10914  0cn0 11136  cz 11207  cuz 11516  ...cfz 12149  #chash 12931  cdvds 14764   UMGrph cumg 25604   VDeg cvdg 26183   EulPaths ceup 26252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-oadd 7425  df-er 7603  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-sup 8205  df-inf 8206  df-card 8622  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-n0 11137  df-z 11208  df-uz 11517  df-rp 11662  df-xadd 11776  df-fz 12150  df-seq 12616  df-exp 12675  df-hash 12932  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-dvds 14765  df-umgra 25605  df-vdgr 26184  df-eupa 26253
This theorem is referenced by:  eupath2  26270
  Copyright terms: Public domain W3C validator