Step |
Hyp |
Ref |
Expression |
1 |
|
eupth2.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
eupth2.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
3 |
|
eupth2.g |
⊢ ( 𝜑 → 𝐺 ∈ UPGraph ) |
4 |
|
eupth2.f |
⊢ ( 𝜑 → Fun 𝐼 ) |
5 |
|
eupth2.p |
⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) |
6 |
|
nn0re |
⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ ) |
7 |
6
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℝ ) |
8 |
7
|
lep1d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ≤ ( 𝑛 + 1 ) ) |
9 |
|
peano2re |
⊢ ( 𝑛 ∈ ℝ → ( 𝑛 + 1 ) ∈ ℝ ) |
10 |
7 9
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + 1 ) ∈ ℝ ) |
11 |
|
eupthiswlk |
⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) |
12 |
|
wlkcl |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) |
13 |
5 11 12
|
3syl |
⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) |
14 |
13
|
nn0red |
⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℝ ) |
15 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ♯ ‘ 𝐹 ) ∈ ℝ ) |
16 |
|
letr |
⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑛 + 1 ) ∈ ℝ ∧ ( ♯ ‘ 𝐹 ) ∈ ℝ ) → ( ( 𝑛 ≤ ( 𝑛 + 1 ) ∧ ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ) → 𝑛 ≤ ( ♯ ‘ 𝐹 ) ) ) |
17 |
7 10 15 16
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ≤ ( 𝑛 + 1 ) ∧ ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ) → 𝑛 ≤ ( ♯ ‘ 𝐹 ) ) ) |
18 |
8 17
|
mpand |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → 𝑛 ≤ ( ♯ ‘ 𝐹 ) ) ) |
19 |
18
|
imim1d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ) |
20 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑥 ) = ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑦 ) ) |
21 |
20
|
breq2d |
⊢ ( 𝑥 = 𝑦 → ( 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑥 ) ↔ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑦 ) ) ) |
22 |
21
|
notbid |
⊢ ( 𝑥 = 𝑦 → ( ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑥 ) ↔ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑦 ) ) ) |
23 |
22
|
elrab |
⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑥 ) } ↔ ( 𝑦 ∈ 𝑉 ∧ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑦 ) ) ) |
24 |
3
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ∧ 𝑦 ∈ 𝑉 ) → 𝐺 ∈ UPGraph ) |
25 |
4
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ∧ 𝑦 ∈ 𝑉 ) → Fun 𝐼 ) |
26 |
5
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ∧ 𝑦 ∈ 𝑉 ) → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) |
27 |
|
eqid |
⊢ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 = 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 |
28 |
|
eqid |
⊢ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 = 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 |
29 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 ) |
30 |
29
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ∧ 𝑦 ∈ 𝑉 ) → 𝑛 ∈ ℕ0 ) |
31 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ) |
32 |
31
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ) |
33 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ 𝑉 ) |
34 |
|
simplrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ∧ 𝑦 ∈ 𝑉 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) |
35 |
1 2 24 25 26 27 28 30 32 33 34
|
eupth2lem3 |
⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) ∧ 𝑦 ∈ 𝑉 ) → ( ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑦 ) ↔ 𝑦 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) |
36 |
35
|
pm5.32da |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( ( 𝑦 ∈ 𝑉 ∧ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑦 ) ) ↔ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) ) |
37 |
|
0elpw |
⊢ ∅ ∈ 𝒫 𝑉 |
38 |
1
|
wlkepvtx |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ 𝑉 ) ) |
39 |
38
|
simpld |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) ∈ 𝑉 ) |
40 |
5 11 39
|
3syl |
⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) ∈ 𝑉 ) |
41 |
40
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 ) |
42 |
1
|
wlkp |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) |
43 |
5 11 42
|
3syl |
⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) |
44 |
43
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ) |
45 |
|
peano2nn0 |
⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 ) |
46 |
45
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + 1 ) ∈ ℕ0 ) |
47 |
46
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝑛 + 1 ) ∈ ℕ0 ) |
48 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
49 |
47 48
|
eleqtrdi |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ) |
50 |
13
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) |
51 |
50
|
nn0zd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℤ ) |
52 |
|
elfz5 |
⊢ ( ( ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ 𝐹 ) ∈ ℤ ) → ( ( 𝑛 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ) ) |
53 |
49 51 52
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( ( 𝑛 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ) ) |
54 |
31 53
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝑛 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) |
55 |
44 54
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝑃 ‘ ( 𝑛 + 1 ) ) ∈ 𝑉 ) |
56 |
41 55
|
prssd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ⊆ 𝑉 ) |
57 |
|
prex |
⊢ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ∈ V |
58 |
57
|
elpw |
⊢ ( { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ∈ 𝒫 𝑉 ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ⊆ 𝑉 ) |
59 |
56 58
|
sylibr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ∈ 𝒫 𝑉 ) |
60 |
|
ifcl |
⊢ ( ( ∅ ∈ 𝒫 𝑉 ∧ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ∈ 𝒫 𝑉 ) → if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ∈ 𝒫 𝑉 ) |
61 |
37 59 60
|
sylancr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ∈ 𝒫 𝑉 ) |
62 |
61
|
elpwid |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ⊆ 𝑉 ) |
63 |
62
|
sseld |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝑦 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) → 𝑦 ∈ 𝑉 ) ) |
64 |
63
|
pm4.71rd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝑦 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ↔ ( 𝑦 ∈ 𝑉 ∧ 𝑦 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) ) |
65 |
36 64
|
bitr4d |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( ( 𝑦 ∈ 𝑉 ∧ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑦 ) ) ↔ 𝑦 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) |
66 |
23 65
|
syl5bb |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → ( 𝑦 ∈ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑥 ) } ↔ 𝑦 ∈ if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) |
67 |
66
|
eqrdv |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) ∧ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) |
68 |
67
|
exp32 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) ) |
69 |
68
|
a2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) ) |
70 |
19 69
|
syld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 𝑛 ) } ) ) → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 〈 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) 〉 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) ) |