Step |
Hyp |
Ref |
Expression |
1 |
|
upwlksfval.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
upwlksfval.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
3 |
1 2
|
upwlksfval |
⊢ ( 𝐺 ∈ V → ( UPWalks ‘ 𝐺 ) = { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } ) |
4 |
3
|
breqd |
⊢ ( 𝐺 ∈ V → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ 𝐹 { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } 𝑃 ) ) |
5 |
|
brabv |
⊢ ( 𝐹 { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ 𝑝 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = { ( 𝑝 ‘ 𝑘 ) , ( 𝑝 ‘ ( 𝑘 + 1 ) ) } ) } 𝑃 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
6 |
4 5
|
syl6bi |
⊢ ( 𝐺 ∈ V → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
7 |
6
|
imdistani |
⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) → ( 𝐺 ∈ V ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
8 |
|
3anass |
⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ↔ ( 𝐺 ∈ V ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
9 |
7 8
|
sylibr |
⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ) → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
10 |
9
|
ex |
⊢ ( 𝐺 ∈ V → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
11 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( UPWalks ‘ 𝐺 ) = ∅ ) |
12 |
|
breq |
⊢ ( ( UPWalks ‘ 𝐺 ) = ∅ → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 ↔ 𝐹 ∅ 𝑃 ) ) |
13 |
|
br0 |
⊢ ¬ 𝐹 ∅ 𝑃 |
14 |
13
|
pm2.21i |
⊢ ( 𝐹 ∅ 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |
15 |
12 14
|
syl6bi |
⊢ ( ( UPWalks ‘ 𝐺 ) = ∅ → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
16 |
11 15
|
syl |
⊢ ( ¬ 𝐺 ∈ V → ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) |
17 |
10 16
|
pm2.61i |
⊢ ( 𝐹 ( UPWalks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) |