Step | Hyp | Ref
| Expression |
1 | | 2wlksot 26394 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 2WalksOt 𝐸) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)}) |
2 | 1 | adantr 480 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑉 2WalksOt 𝐸) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)}) |
3 | 2 | eleq2d 2673 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝑉 2WalksOt 𝐸) ↔ 〈𝐴, 𝐵, 𝐶〉 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)})) |
4 | | eleq1 2676 |
. . . . . 6
⊢ (𝑡 = 〈𝐴, 𝐵, 𝐶〉 → (𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) ↔ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏))) |
5 | 4 | 2rexbidv 3039 |
. . . . 5
⊢ (𝑡 = 〈𝐴, 𝐵, 𝐶〉 → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏))) |
6 | 5 | elrab 3331 |
. . . 4
⊢
(〈𝐴, 𝐵, 𝐶〉 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)} ↔ (〈𝐴, 𝐵, 𝐶〉 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏))) |
7 | 6 | a1i 11 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)} ↔ (〈𝐴, 𝐵, 𝐶〉 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)))) |
8 | | eqid 2610 |
. . . . . 6
⊢
〈𝐴, 𝐵, 𝐶〉 = 〈𝐴, 𝐵, 𝐶〉 |
9 | | otel3xp 5077 |
. . . . . 6
⊢
((〈𝐴, 𝐵, 𝐶〉 = 〈𝐴, 𝐵, 𝐶〉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 〈𝐴, 𝐵, 𝐶〉 ∈ ((𝑉 × 𝑉) × 𝑉)) |
10 | 8, 9 | mpan 702 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 〈𝐴, 𝐵, 𝐶〉 ∈ ((𝑉 × 𝑉) × 𝑉)) |
11 | 10 | adantl 481 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 〈𝐴, 𝐵, 𝐶〉 ∈ ((𝑉 × 𝑉) × 𝑉)) |
12 | 11 | biantrurd 528 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) ↔ (〈𝐴, 𝐵, 𝐶〉 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)))) |
13 | | el2wlkonotot0 26399 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) ↔ (𝐴 = 𝑎 ∧ 𝐶 = 𝑏 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
14 | 13 | adantlr 747 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) ↔ (𝐴 = 𝑎 ∧ 𝐶 = 𝑏 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) |
15 | | simp3 1056 |
. . . . . 6
⊢ ((𝐴 = 𝑎 ∧ 𝐶 = 𝑏 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |
16 | 14, 15 | syl6bi 242 |
. . . . 5
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) → ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
17 | 16 | rexlimdvva 3020 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) → ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
18 | | el2wlkonotot 26400 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
19 | 18 | bicomd 212 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ↔ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶))) |
20 | 19 | 3adantr2 1214 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ↔ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶))) |
21 | | simplr1 1096 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) → 𝐴 ∈ 𝑉) |
22 | | simplr3 1098 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) → 𝐶 ∈ 𝑉) |
23 | | simpr 476 |
. . . . . . 7
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) → 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) |
24 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) = (𝐴(𝑉 2WalksOnOt 𝐸)𝑏)) |
25 | 24 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) ↔ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝑏))) |
26 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑏 = 𝐶 → (𝐴(𝑉 2WalksOnOt 𝐸)𝑏) = (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) |
27 | 26 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑏 = 𝐶 → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝑏) ↔ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶))) |
28 | 25, 27 | rspc2ev 3295 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)) |
29 | 21, 22, 23, 28 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)) |
30 | 29 | ex 449 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏))) |
31 | 20, 30 | sylbid 229 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏))) |
32 | 17, 31 | impbid 201 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 〈𝐴, 𝐵, 𝐶〉 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
33 | 7, 12, 32 | 3bitr2d 295 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)} ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
34 | 3, 33 | bitrd 267 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝑉 2WalksOt 𝐸) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |