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