Metamath Proof Explorer


Theorem eupth2lems

Description: Lemma for eupth2 (induction step): The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct, if the Eulerian path shortened by one edge has this property. Formerly part of proof for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

Ref Expression
Hypotheses eupth2.v 𝑉 = ( Vtx ‘ 𝐺 )
eupth2.i 𝐼 = ( iEdg ‘ 𝐺 )
eupth2.g ( 𝜑𝐺 ∈ UPGraph )
eupth2.f ( 𝜑 → Fun 𝐼 )
eupth2.p ( 𝜑𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
Assertion eupth2lems ( ( 𝜑𝑛 ∈ ℕ0 ) → ( ( 𝑛 ≤ ( ♯ ‘ 𝐹 ) → { 𝑥𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ 𝑛 ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃𝑛 ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃𝑛 ) } ) ) → ( ( 𝑛 + 1 ) ≤ ( ♯ ‘ 𝐹 ) → { 𝑥𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( 𝑛 + 1 ) ) ) ) ⟩ ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( 𝑛 + 1 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) ) )

Proof

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 ) ) } ) ) ) )