Step | Hyp | Ref
| Expression |
1 | | n0 3890 |
. 2
⊢ ((𝑋(𝑉 2SPathOnOt 𝐸)𝑌) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ (𝑋(𝑉 2SPathOnOt 𝐸)𝑌)) |
2 | | 2spthonot3v 26403 |
. . . 4
⊢ (𝑡 ∈ (𝑋(𝑉 2SPathOnOt 𝐸)𝑌) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉))) |
3 | | el2spthonot 26397 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑡 ∈ (𝑋(𝑉 2SPathOnOt 𝐸)𝑌) ↔ ∃𝑏 ∈ 𝑉 (𝑡 = 〈𝑋, 𝑏, 𝑌〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2)))))) |
4 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
5 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑝 ∈ V |
6 | | isspth 26099 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑝 ∈ V)) → (𝑓(𝑉 SPaths 𝐸)𝑝 ↔ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡𝑝))) |
7 | | istrl2 26068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑝 ∈ V)) → (𝑓(𝑉 Trails 𝐸)𝑝 ↔ (𝑓:(0..^(#‘𝑓))–1-1→dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑝‘𝑖), (𝑝‘(𝑖 + 1))}))) |
8 | 7 | anbi1d 737 |
. . . . . . . . . . . . . . 15
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑝 ∈ V)) → ((𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡𝑝) ↔ ((𝑓:(0..^(#‘𝑓))–1-1→dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑝‘𝑖), (𝑝‘(𝑖 + 1))}) ∧ Fun ◡𝑝))) |
9 | 6, 8 | bitrd 267 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑓 ∈ V ∧ 𝑝 ∈ V)) → (𝑓(𝑉 SPaths 𝐸)𝑝 ↔ ((𝑓:(0..^(#‘𝑓))–1-1→dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑝‘𝑖), (𝑝‘(𝑖 + 1))}) ∧ Fun ◡𝑝))) |
10 | 4, 5, 9 | mpanr12 717 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑓(𝑉 SPaths 𝐸)𝑝 ↔ ((𝑓:(0..^(#‘𝑓))–1-1→dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑝‘𝑖), (𝑝‘(𝑖 + 1))}) ∧ Fun ◡𝑝))) |
11 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑓(𝑉 SPaths 𝐸)𝑝 ↔ ((𝑓:(0..^(#‘𝑓))–1-1→dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑝‘𝑖), (𝑝‘(𝑖 + 1))}) ∧ Fun ◡𝑝))) |
12 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → (𝑓(𝑉 SPaths 𝐸)𝑝 ↔ ((𝑓:(0..^(#‘𝑓))–1-1→dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑝‘𝑖), (𝑝‘(𝑖 + 1))}) ∧ Fun ◡𝑝))) |
13 | | df-f1 5809 |
. . . . . . . . . . . . . 14
⊢ (𝑝:(0...(#‘𝑓))–1-1→𝑉 ↔ (𝑝:(0...(#‘𝑓))⟶𝑉 ∧ Fun ◡𝑝)) |
14 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑓) = 2
→ 𝑝 = 𝑝) |
15 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑓) = 2
→ (0...(#‘𝑓)) =
(0...2)) |
16 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑓) = 2
→ 𝑉 = 𝑉) |
17 | 14, 15, 16 | f1eq123d 6044 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑓) = 2
→ (𝑝:(0...(#‘𝑓))–1-1→𝑉 ↔ 𝑝:(0...2)–1-1→𝑉)) |
18 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0...2) =
(0...2) |
19 | 18 | f13idfv 12662 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝:(0...2)–1-1→𝑉 ↔ (𝑝:(0...2)⟶𝑉 ∧ ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2)))) |
20 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝:(0...2)⟶𝑉 ∧ ((𝑝‘0) ≠ (𝑝‘1) ∧ (𝑝‘0) ≠ (𝑝‘2) ∧ (𝑝‘1) ≠ (𝑝‘2))) → (𝑝‘0) ≠ (𝑝‘2)) |
21 | 19, 20 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝:(0...2)–1-1→𝑉 → (𝑝‘0) ≠ (𝑝‘2)) |
22 | 21 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝:(0...2)–1-1→𝑉 → ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → (𝑝‘0) ≠ (𝑝‘2))) |
23 | 17, 22 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑓) = 2
→ (𝑝:(0...(#‘𝑓))–1-1→𝑉 → ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → (𝑝‘0) ≠ (𝑝‘2)))) |
24 | 23 | com3l 87 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝:(0...(#‘𝑓))–1-1→𝑉 → ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((#‘𝑓) = 2 → (𝑝‘0) ≠ (𝑝‘2)))) |
25 | 24 | imp31 447 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝:(0...(#‘𝑓))–1-1→𝑉 ∧ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉)) ∧ (#‘𝑓) = 2) → (𝑝‘0) ≠ (𝑝‘2)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑝:(0...(#‘𝑓))–1-1→𝑉 ∧ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉)) ∧ (#‘𝑓) = 2) ∧ (𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2))) → (𝑝‘0) ≠ (𝑝‘2)) |
27 | | simpl 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 = (𝑝‘0) ∧ 𝑌 = (𝑝‘2)) → 𝑋 = (𝑝‘0)) |
28 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 = (𝑝‘0) ∧ 𝑌 = (𝑝‘2)) → 𝑌 = (𝑝‘2)) |
29 | 27, 28 | neeq12d 2843 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 = (𝑝‘0) ∧ 𝑌 = (𝑝‘2)) → (𝑋 ≠ 𝑌 ↔ (𝑝‘0) ≠ (𝑝‘2))) |
30 | 29 | 3adant2 1073 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2)) → (𝑋 ≠ 𝑌 ↔ (𝑝‘0) ≠ (𝑝‘2))) |
31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑝:(0...(#‘𝑓))–1-1→𝑉 ∧ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉)) ∧ (#‘𝑓) = 2) ∧ (𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2))) → (𝑋 ≠ 𝑌 ↔ (𝑝‘0) ≠ (𝑝‘2))) |
32 | 26, 31 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑝:(0...(#‘𝑓))–1-1→𝑉 ∧ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉)) ∧ (#‘𝑓) = 2) ∧ (𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2))) → 𝑋 ≠ 𝑌) |
33 | 32 | exp41 636 |
. . . . . . . . . . . . . 14
⊢ (𝑝:(0...(#‘𝑓))–1-1→𝑉 → ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((#‘𝑓) = 2 → ((𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2)) → 𝑋 ≠ 𝑌)))) |
34 | 13, 33 | sylbir 224 |
. . . . . . . . . . . . 13
⊢ ((𝑝:(0...(#‘𝑓))⟶𝑉 ∧ Fun ◡𝑝) → ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((#‘𝑓) = 2 → ((𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2)) → 𝑋 ≠ 𝑌)))) |
35 | 34 | 3ad2antl2 1217 |
. . . . . . . . . . . 12
⊢ (((𝑓:(0..^(#‘𝑓))–1-1→dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑝‘𝑖), (𝑝‘(𝑖 + 1))}) ∧ Fun ◡𝑝) → ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((#‘𝑓) = 2 → ((𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2)) → 𝑋 ≠ 𝑌)))) |
36 | 35 | com12 32 |
. . . . . . . . . . 11
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → (((𝑓:(0..^(#‘𝑓))–1-1→dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑝‘𝑖), (𝑝‘(𝑖 + 1))}) ∧ Fun ◡𝑝) → ((#‘𝑓) = 2 → ((𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2)) → 𝑋 ≠ 𝑌)))) |
37 | 12, 36 | sylbid 229 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → (𝑓(𝑉 SPaths 𝐸)𝑝 → ((#‘𝑓) = 2 → ((𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2)) → 𝑋 ≠ 𝑌)))) |
38 | 37 | 3impd 1273 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2))) → 𝑋 ≠ 𝑌)) |
39 | 38 | exlimdvv 1849 |
. . . . . . . 8
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → (∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2))) → 𝑋 ≠ 𝑌)) |
40 | 39 | adantld 482 |
. . . . . . 7
⊢ ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((𝑡 = 〈𝑋, 𝑏, 𝑌〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2)))) → 𝑋 ≠ 𝑌)) |
41 | 40 | rexlimdva 3013 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (∃𝑏 ∈ 𝑉 (𝑡 = 〈𝑋, 𝑏, 𝑌〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑋 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑌 = (𝑝‘2)))) → 𝑋 ≠ 𝑌)) |
42 | 3, 41 | sylbid 229 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (𝑡 ∈ (𝑋(𝑉 2SPathOnOt 𝐸)𝑌) → 𝑋 ≠ 𝑌)) |
43 | 42 | 3adant3 1074 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑡 ∈ ((𝑉 × 𝑉) × 𝑉)) → (𝑡 ∈ (𝑋(𝑉 2SPathOnOt 𝐸)𝑌) → 𝑋 ≠ 𝑌)) |
44 | 2, 43 | mpcom 37 |
. . 3
⊢ (𝑡 ∈ (𝑋(𝑉 2SPathOnOt 𝐸)𝑌) → 𝑋 ≠ 𝑌) |
45 | 44 | exlimiv 1845 |
. 2
⊢
(∃𝑡 𝑡 ∈ (𝑋(𝑉 2SPathOnOt 𝐸)𝑌) → 𝑋 ≠ 𝑌) |
46 | 1, 45 | sylbi 206 |
1
⊢ ((𝑋(𝑉 2SPathOnOt 𝐸)𝑌) ≠ ∅ → 𝑋 ≠ 𝑌) |