Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. . 3
⊢ (𝑉 ∈ 𝑋 → 𝑉 ∈ V) |
2 | 1 | adantr 480 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝑉 ∈ V) |
3 | | elex 3185 |
. . 3
⊢ (𝐸 ∈ 𝑌 → 𝐸 ∈ V) |
4 | 3 | adantl 481 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐸 ∈ V) |
5 | | mpt2exga 7135 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))}) ∈ V) |
6 | 5 | anidms 675 |
. . 3
⊢ (𝑉 ∈ 𝑋 → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))}) ∈ V) |
7 | 6 | adantr 480 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))}) ∈ V) |
8 | | simpl 472 |
. . . 4
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 𝑣 = 𝑉) |
9 | | id 22 |
. . . . . . . 8
⊢ (𝑣 = 𝑉 → 𝑣 = 𝑉) |
10 | 9, 9 | xpeq12d 5064 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → (𝑣 × 𝑣) = (𝑉 × 𝑉)) |
11 | 10, 9 | xpeq12d 5064 |
. . . . . 6
⊢ (𝑣 = 𝑉 → ((𝑣 × 𝑣) × 𝑣) = ((𝑉 × 𝑉) × 𝑉)) |
12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑣 × 𝑣) × 𝑣) = ((𝑉 × 𝑉) × 𝑉)) |
13 | | oveq12 6558 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 SPathOn 𝑒) = (𝑉 SPathOn 𝐸)) |
14 | 13 | oveqd 6566 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎(𝑣 SPathOn 𝑒)𝑏) = (𝑎(𝑉 SPathOn 𝐸)𝑏)) |
15 | 14 | breqd 4594 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ↔ 𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝)) |
16 | 15 | 3anbi1d 1395 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏)) ↔ (𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏)))) |
17 | 16 | 2exbidv 1839 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏)) ↔ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏)))) |
18 | 12, 17 | rabeqbidv 3168 |
. . . 4
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))}) |
19 | 8, 8, 18 | mpt2eq123dv 6615 |
. . 3
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))}) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))})) |
20 | | df-2spthonot 26387 |
. . 3
⊢
2SPathOnOt = (𝑣 ∈ V,
𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))})) |
21 | 19, 20 | ovmpt2ga 6688 |
. 2
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))}) ∈ V) → (𝑉 2SPathOnOt 𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))})) |
22 | 2, 4, 7, 21 | syl3anc 1318 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 2SPathOnOt 𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st
‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st
‘𝑡)) = (𝑝‘1) ∧ (2nd
‘𝑡) = 𝑏))})) |