Proof of Theorem 2pthon3v
Step | Hyp | Ref
| Expression |
1 | | prex 4836 |
. . 3
⊢ {〈0,
(◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∈ V |
2 | | tpex 6855 |
. . 3
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈
V |
3 | 1, 2 | pm3.2i 470 |
. 2
⊢
({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈
V) |
4 | | fvex 6113 |
. . . . 5
⊢ (◡𝐸‘{𝐴, 𝐵}) ∈ V |
5 | | fvex 6113 |
. . . . 5
⊢ (◡𝐸‘{𝐵, 𝐶}) ∈ V |
6 | 4, 5 | pm3.2i 470 |
. . . 4
⊢ ((◡𝐸‘{𝐴, 𝐵}) ∈ V ∧ (◡𝐸‘{𝐵, 𝐶}) ∈ V) |
7 | | 2pthoncl 26133 |
. . . 4
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ((◡𝐸‘{𝐴, 𝐵}) ∈ V ∧ (◡𝐸‘{𝐵, 𝐶}) ∈ V) ∧ ((◡𝐸‘{𝐴, 𝐵}) ≠ (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) → {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) |
8 | 6, 7 | mp3an2 1404 |
. . 3
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ((◡𝐸‘{𝐴, 𝐵}) ≠ (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) → {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) |
9 | | ax-1ne0 9884 |
. . . . . 6
⊢ 1 ≠
0 |
10 | 9 | nesymi 2839 |
. . . . 5
⊢ ¬ 0
= 1 |
11 | | c0ex 9913 |
. . . . . . 7
⊢ 0 ∈
V |
12 | 11, 4 | opth1 4870 |
. . . . . 6
⊢ (〈0,
(◡𝐸‘{𝐴, 𝐵})〉 = 〈1, (◡𝐸‘{𝐵, 𝐶})〉 → 0 = 1) |
13 | 12 | necon3bi 2808 |
. . . . 5
⊢ (¬ 0
= 1 → 〈0, (◡𝐸‘{𝐴, 𝐵})〉 ≠ 〈1, (◡𝐸‘{𝐵, 𝐶})〉) |
14 | 10, 13 | ax-mp 5 |
. . . 4
⊢ 〈0,
(◡𝐸‘{𝐴, 𝐵})〉 ≠ 〈1, (◡𝐸‘{𝐵, 𝐶})〉 |
15 | | opex 4859 |
. . . . 5
⊢ 〈0,
(◡𝐸‘{𝐴, 𝐵})〉 ∈ V |
16 | | opex 4859 |
. . . . 5
⊢ 〈1,
(◡𝐸‘{𝐵, 𝐶})〉 ∈ V |
17 | | hashprgOLD 13044 |
. . . . 5
⊢
((〈0, (◡𝐸‘{𝐴, 𝐵})〉 ∈ V ∧ 〈1, (◡𝐸‘{𝐵, 𝐶})〉 ∈ V) → (〈0, (◡𝐸‘{𝐴, 𝐵})〉 ≠ 〈1, (◡𝐸‘{𝐵, 𝐶})〉 ↔ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2)) |
18 | 15, 16, 17 | mp2an 704 |
. . . 4
⊢ (〈0,
(◡𝐸‘{𝐴, 𝐵})〉 ≠ 〈1, (◡𝐸‘{𝐵, 𝐶})〉 ↔ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2) |
19 | 14, 18 | mpbi 219 |
. . 3
⊢
(#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2 |
20 | 8, 19 | jctir 559 |
. 2
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ((◡𝐸‘{𝐴, 𝐵}) ≠ (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) → ({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2)) |
21 | | breq12 4588 |
. . . 4
⊢ ((𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∧ 𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) → (𝑓(𝐴(𝑉 PathOn 𝐸)𝐶)𝑝 ↔ {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉})) |
22 | | fveq2 6103 |
. . . . . 6
⊢ (𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} → (#‘𝑓) = (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉})) |
23 | 22 | eqeq1d 2612 |
. . . . 5
⊢ (𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} → ((#‘𝑓) = 2 ↔ (#‘{〈0,
(◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2)) |
24 | 23 | adantr 480 |
. . . 4
⊢ ((𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∧ 𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) → ((#‘𝑓) = 2 ↔ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2)) |
25 | 21, 24 | anbi12d 743 |
. . 3
⊢ ((𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∧ 𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) → ((𝑓(𝐴(𝑉 PathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2) ↔ ({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2))) |
26 | 25 | spc2egv 3268 |
. 2
⊢
(({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈ V) →
(({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝐴(𝑉 PathOn 𝐸)𝐶){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2) → ∃𝑓∃𝑝(𝑓(𝐴(𝑉 PathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2))) |
27 | 3, 20, 26 | mpsyl 66 |
1
⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ((◡𝐸‘{𝐴, 𝐵}) ≠ (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) → ∃𝑓∃𝑝(𝑓(𝐴(𝑉 PathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2)) |