Step | Hyp | Ref
| Expression |
1 | | 2spthsot 26395 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 2SPathsOt 𝐸) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)}) |
2 | 1 | eleq2d 2673 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑇 ∈ (𝑉 2SPathsOt 𝐸) ↔ 𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)})) |
3 | | eleq1 2676 |
. . . . 5
⊢ (𝑡 = 𝑇 → (𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ↔ 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |
4 | 3 | 2rexbidv 3039 |
. . . 4
⊢ (𝑡 = 𝑇 → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |
5 | 4 | elrab 3331 |
. . 3
⊢ (𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)} ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |
6 | 5 | a1i 11 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)} ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)))) |
7 | | simpr 476 |
. . 3
⊢ ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
8 | | simpr 476 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
9 | | 2spthonot3v 26403 |
. . . . . . . 8
⊢ (𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))) |
10 | 9 | simp3d 1068 |
. . . . . . 7
⊢ (𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))) |
12 | 11 | rexlimivv 3018 |
. . . . 5
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)) |
13 | 8, 12 | jccil 561 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |
14 | 13 | ex 449 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)))) |
15 | 7, 14 | impbid2 215 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |
16 | 2, 6, 15 | 3bitrd 293 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑇 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |