Step | Hyp | Ref
| Expression |
1 | | orc 399 |
. . . . 5
⊢ (𝑎 = 𝑐 → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) = ∅)) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝑎 = 𝑐 → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) = ∅))) |
3 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ↔ ∃𝑏 ∈ (𝑉 ∖ {𝑎})𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
4 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) |
5 | 4 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) → (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) |
6 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) |
7 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) → 𝑎 ∈ 𝑉) |
8 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → 𝑎 ∈ 𝑉) |
9 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → 𝑏 ∈ 𝑉) |
10 | 9 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → 𝑏 ∈ 𝑉) |
11 | | el2spthonot 26397 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ↔ ∃𝑚 ∈ 𝑉 (𝑡 = 〈𝑎, 𝑚, 𝑏〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑚 = (𝑝‘1) ∧ 𝑏 = (𝑝‘2)))))) |
12 | 6, 8, 10, 11 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ↔ ∃𝑚 ∈ 𝑉 (𝑡 = 〈𝑎, 𝑚, 𝑏〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑚 = (𝑝‘1) ∧ 𝑏 = (𝑝‘2)))))) |
13 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑎 ∈ V |
14 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑚 ∈ V |
15 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 𝑏 ∈ V |
16 | 13, 14, 15 | otth 4879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈𝑎, 𝑚, 𝑏〉 = 〈𝑐, 𝑛, 𝑑〉 ↔ (𝑎 = 𝑐 ∧ 𝑚 = 𝑛 ∧ 𝑏 = 𝑑)) |
17 | 16 | simp1bi 1069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(〈𝑎, 𝑚, 𝑏〉 = 〈𝑐, 𝑛, 𝑑〉 → 𝑎 = 𝑐) |
18 | 17 | con3i 149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (¬
𝑎 = 𝑐 → ¬ 〈𝑎, 𝑚, 𝑏〉 = 〈𝑐, 𝑛, 𝑑〉) |
19 | 18 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → ¬ 〈𝑎, 𝑚, 𝑏〉 = 〈𝑐, 𝑛, 𝑑〉) |
20 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 = 〈𝑎, 𝑚, 𝑏〉 → (𝑡 = 〈𝑐, 𝑛, 𝑑〉 ↔ 〈𝑎, 𝑚, 𝑏〉 = 〈𝑐, 𝑛, 𝑑〉)) |
21 | 20 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 = 〈𝑎, 𝑚, 𝑏〉 → (¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉 ↔ ¬ 〈𝑎, 𝑚, 𝑏〉 = 〈𝑐, 𝑛, 𝑑〉)) |
22 | 19, 21 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 〈𝑎, 𝑚, 𝑏〉 → ((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → ¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 = 〈𝑎, 𝑚, 𝑏〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑚 = (𝑝‘1) ∧ 𝑏 = (𝑝‘2)))) → ((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → ¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉)) |
24 | 23 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) ∧ (𝑡 = 〈𝑎, 𝑚, 𝑏〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑚 = (𝑝‘1) ∧ 𝑏 = (𝑝‘2))))) → ¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉) |
25 | 24 | orcd 406 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) ∧ (𝑡 = 〈𝑎, 𝑚, 𝑏〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑚 = (𝑝‘1) ∧ 𝑏 = (𝑝‘2))))) → (¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∨ ¬ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2))))) |
26 | 25 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) ∧ (𝑡 = 〈𝑎, 𝑚, 𝑏〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑚 = (𝑝‘1) ∧ 𝑏 = (𝑝‘2))))) → (𝑛 ∈ 𝑉 → (¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∨ ¬ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2)))))) |
27 | 26 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) ∧ (𝑡 = 〈𝑎, 𝑚, 𝑏〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑚 = (𝑝‘1) ∧ 𝑏 = (𝑝‘2))))) → (𝑑 ∈ (𝑉 ∖ {𝑐}) → (𝑛 ∈ 𝑉 → (¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∨ ¬ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2))))))) |
28 | 27 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑚 ∈ 𝑉) → ((𝑡 = 〈𝑎, 𝑚, 𝑏〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑚 = (𝑝‘1) ∧ 𝑏 = (𝑝‘2)))) → (𝑑 ∈ (𝑉 ∖ {𝑐}) → (𝑛 ∈ 𝑉 → (¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∨ ¬ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2)))))))) |
29 | 28 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (∃𝑚 ∈ 𝑉 (𝑡 = 〈𝑎, 𝑚, 𝑏〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑚 = (𝑝‘1) ∧ 𝑏 = (𝑝‘2)))) → (𝑑 ∈ (𝑉 ∖ {𝑐}) → (𝑛 ∈ 𝑉 → (¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∨ ¬ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2)))))))) |
30 | 12, 29 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ (((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) → (𝑑 ∈ (𝑉 ∖ {𝑐}) → (𝑛 ∈ 𝑉 → (¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∨ ¬ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2)))))))) |
31 | 30 | imp41 617 |
. . . . . . . . . . . . . . . . 17
⊢
((((((¬ 𝑎 =
𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) ∧ 𝑛 ∈ 𝑉) → (¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∨ ¬ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2))))) |
32 | | ianor 508 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2)))) ↔ (¬ 𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∨ ¬ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2))))) |
33 | 31, 32 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢
((((((¬ 𝑎 =
𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) ∧ 𝑛 ∈ 𝑉) → ¬ (𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2))))) |
34 | 33 | nrexdv 2984 |
. . . . . . . . . . . . . . 15
⊢
(((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) → ¬ ∃𝑛 ∈ 𝑉 (𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2))))) |
35 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) → (𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌)) |
36 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑐 ∈ 𝑉) |
37 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 ∈ (𝑉 ∖ {𝑐}) → 𝑑 ∈ 𝑉) |
38 | 36, 37 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) → (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) |
39 | 35, 38 | jca 553 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) |
40 | 39 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑑 ∈ (𝑉 ∖ {𝑐}) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)))) |
41 | 40 | ad3antlr 763 |
. . . . . . . . . . . . . . . . 17
⊢ ((((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) → (𝑑 ∈ (𝑉 ∖ {𝑐}) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)))) |
42 | 41 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢
(((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) → ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) |
43 | | el2spthonot 26397 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑡 ∈ (𝑐(𝑉 2SPathOnOt 𝐸)𝑑) ↔ ∃𝑛 ∈ 𝑉 (𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2)))))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) → (𝑡 ∈ (𝑐(𝑉 2SPathOnOt 𝐸)𝑑) ↔ ∃𝑛 ∈ 𝑉 (𝑡 = 〈𝑐, 𝑛, 𝑑〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑐 = (𝑝‘0) ∧ 𝑛 = (𝑝‘1) ∧ 𝑑 = (𝑝‘2)))))) |
45 | 34, 44 | mtbird 314 |
. . . . . . . . . . . . . 14
⊢
(((((¬ 𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) ∧ 𝑑 ∈ (𝑉 ∖ {𝑐})) → ¬ 𝑡 ∈ (𝑐(𝑉 2SPathOnOt 𝐸)𝑑)) |
46 | 45 | nrexdv 2984 |
. . . . . . . . . . . . 13
⊢ ((((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) → ¬ ∃𝑑 ∈ (𝑉 ∖ {𝑐})𝑡 ∈ (𝑐(𝑉 2SPathOnOt 𝐸)𝑑)) |
47 | | eliun 4460 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑) ↔ ∃𝑑 ∈ (𝑉 ∖ {𝑐})𝑡 ∈ (𝑐(𝑉 2SPathOnOt 𝐸)𝑑)) |
48 | 46, 47 | sylnibr 318 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ∧ 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) → ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑)) |
49 | 48 | ex 449 |
. . . . . . . . . . 11
⊢ (((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) → ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑))) |
50 | 49 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ ((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) → (∃𝑏 ∈ (𝑉 ∖ {𝑎})𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) → ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑))) |
51 | 3, 50 | syl5bi 231 |
. . . . . . . . 9
⊢ ((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) → (𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) → ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑))) |
52 | 51 | ralrimiv 2948 |
. . . . . . . 8
⊢ ((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) → ∀𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑)) |
53 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑑 → (𝑐(𝑉 2SPathOnOt 𝐸)𝑏) = (𝑐(𝑉 2SPathOnOt 𝐸)𝑑)) |
54 | 53 | cbviunv 4495 |
. . . . . . . . . . 11
⊢ ∪ 𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏) = ∪ 𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑) |
55 | 54 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ∪ 𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏) ↔ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑)) |
56 | 55 | notbii 309 |
. . . . . . . . 9
⊢ (¬
𝑡 ∈ ∪ 𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏) ↔ ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑)) |
57 | 56 | ralbii 2963 |
. . . . . . . 8
⊢
(∀𝑡 ∈
∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ¬ 𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏) ↔ ∀𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ¬ 𝑡 ∈ ∪
𝑑 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑑)) |
58 | 52, 57 | sylibr 223 |
. . . . . . 7
⊢ ((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) → ∀𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ¬ 𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) |
59 | | disj 3969 |
. . . . . . 7
⊢
((∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) = ∅ ↔ ∀𝑡 ∈ ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ¬ 𝑡 ∈ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) |
60 | 58, 59 | sylibr 223 |
. . . . . 6
⊢ ((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) → (∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) = ∅) |
61 | 60 | olcd 407 |
. . . . 5
⊢ ((¬
𝑎 = 𝑐 ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))) → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) = ∅)) |
62 | 61 | ex 449 |
. . . 4
⊢ (¬
𝑎 = 𝑐 → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) = ∅))) |
63 | 2, 62 | pm2.61i 175 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) = ∅)) |
64 | 63 | ralrimivva 2954 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ 𝑉 (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) = ∅)) |
65 | | sneq 4135 |
. . . . 5
⊢ (𝑎 = 𝑐 → {𝑎} = {𝑐}) |
66 | 65 | difeq2d 3690 |
. . . 4
⊢ (𝑎 = 𝑐 → (𝑉 ∖ {𝑎}) = (𝑉 ∖ {𝑐})) |
67 | | oveq1 6556 |
. . . 4
⊢ (𝑎 = 𝑐 → (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) = (𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) |
68 | 66, 67 | iuneq12d 4482 |
. . 3
⊢ (𝑎 = 𝑐 → ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) = ∪ 𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) |
69 | 68 | disjor 4567 |
. 2
⊢
(Disj 𝑎
∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ↔ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ 𝑉 (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∩ ∪
𝑏 ∈ (𝑉 ∖ {𝑐})(𝑐(𝑉 2SPathOnOt 𝐸)𝑏)) = ∅)) |
70 | 64, 69 | sylibr 223 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |