Step |
Hyp |
Ref |
Expression |
1 |
|
wlkson.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
1
|
1vgrex |
⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ V ) |
3 |
2
|
adantr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐺 ∈ V ) |
4 |
|
simpl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 ) |
5 |
4 1
|
eleqtrdi |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) |
6 |
|
simpr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 ) |
7 |
6 1
|
eleqtrdi |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) |
8 |
|
wksv |
⊢ { 〈 𝑓 , 𝑝 〉 ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V |
9 |
8
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → { 〈 𝑓 , 𝑝 〉 ∣ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 } ∈ V ) |
10 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) |
11 |
|
eqeq2 |
⊢ ( 𝑎 = 𝐴 → ( ( 𝑝 ‘ 0 ) = 𝑎 ↔ ( 𝑝 ‘ 0 ) = 𝐴 ) ) |
12 |
|
eqeq2 |
⊢ ( 𝑏 = 𝐵 → ( ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ↔ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) |
13 |
11 12
|
bi2anan9 |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) ) |
14 |
|
biidd |
⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) ) |
15 |
|
df-wlkson |
⊢ WalksOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) ) |
16 |
|
eqid |
⊢ ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝑔 ) |
17 |
|
3anass |
⊢ ( ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ) ) |
18 |
17
|
biancomi |
⊢ ( ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ↔ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) ) |
19 |
18
|
opabbii |
⊢ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } = { 〈 𝑓 , 𝑝 〉 ∣ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) } |
20 |
16 16 19
|
mpoeq123i |
⊢ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) = ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) } ) |
21 |
20
|
mpteq2i |
⊢ ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) } ) ) = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) } ) ) |
22 |
15 21
|
eqtri |
⊢ WalksOn = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 〈 𝑓 , 𝑝 〉 ∣ ( ( ( 𝑝 ‘ 0 ) = 𝑎 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝑏 ) ∧ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ) } ) ) |
23 |
3 5 7 9 10 13 14 22
|
mptmpoopabbrd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) = { 〈 𝑓 , 𝑝 〉 ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) } ) |
24 |
|
ancom |
⊢ ( ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) ) |
25 |
|
3anass |
⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) ) |
26 |
24 25
|
bitr4i |
⊢ ( ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) |
27 |
26
|
opabbii |
⊢ { 〈 𝑓 , 𝑝 〉 ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ∧ 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ) } = { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) } |
28 |
23 27
|
eqtrdi |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) = { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) } ) |