Proof of Theorem usg2spthonot
Step | Hyp | Ref
| Expression |
1 | | ne0i 3880 |
. . . . 5
⊢
(〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ≠ ∅) |
2 | | 2spontn0vne 26414 |
. . . . 5
⊢ ((𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ≠ ∅ → 𝐴 ≠ 𝐶) |
3 | 1, 2 | syl 17 |
. . . 4
⊢
(〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → 𝐴 ≠ 𝐶) |
4 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑉 USGrph 𝐸) |
5 | 4 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → 𝑉 USGrph 𝐸) |
6 | | 3simpb 1052 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
7 | 6 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
8 | 7 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
9 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → 𝐴 ≠ 𝐶) |
10 | | 2pthwlkonot 26412 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) = (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) |
11 | 5, 8, 9, 10 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) = (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) |
12 | 11 | eleq2d 2673 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶))) |
13 | 9 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) → 𝐴 ≠ 𝐶) |
14 | | usg2wlkonot 26410 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
15 | 14 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
16 | 15 | biimpa 500 |
. . . . . . . . 9
⊢ (((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) → ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
17 | | 3anass 1035 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ (𝐴 ≠ 𝐶 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
18 | 13, 16, 17 | sylanbrc 695 |
. . . . . . . 8
⊢ (((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) → (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
19 | 18 | ex 449 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) → (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
20 | 12, 19 | sylbid 229 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐶 ∧ (𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
21 | 20 | ex 449 |
. . . . 5
⊢ (𝐴 ≠ 𝐶 → ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))) |
22 | 21 | com23 84 |
. . . 4
⊢ (𝐴 ≠ 𝐶 → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))) |
23 | 3, 22 | mpcom 37 |
. . 3
⊢
(〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
24 | 23 | com12 32 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
25 | 14 | bicomd 212 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶))) |
26 | 25 | anbi2d 736 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐶 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (𝐴 ≠ 𝐶 ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)))) |
27 | 17, 26 | syl5bb 271 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ (𝐴 ≠ 𝐶 ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)))) |
28 | 4 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → 𝑉 USGrph 𝐸) |
29 | 7 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
30 | | simpr 476 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → 𝐴 ≠ 𝐶) |
31 | 10 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) = (𝐴(𝑉 2SPathOnOt 𝐸)𝐶)) |
32 | 28, 29, 30, 31 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) = (𝐴(𝑉 2SPathOnOt 𝐸)𝐶)) |
33 | 32 | eleq2d 2673 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶))) |
34 | 33 | biimpd 218 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝐴 ≠ 𝐶) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) → 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶))) |
35 | 34 | expimpd 627 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐶 ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) → 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶))) |
36 | 27, 35 | sylbid 229 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶))) |
37 | 24, 36 | impbid 201 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |