Proof of Theorem usg2wlk
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 | | eqid 2610 |
. . . 4
⊢ {〈0,
(◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} |
5 | | eqid 2610 |
. . . 4
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
6 | 4, 5 | usgra2adedgwlk 26142 |
. . 3
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2 ∧ (𝐴 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) ∧ 𝐵 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘1) ∧ 𝐶 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2))))) |
7 | 6 | 3impib 1254 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2 ∧ (𝐴 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) ∧ 𝐵 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘1) ∧ 𝐶 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2)))) |
8 | | breq12 4588 |
. . . 4
⊢ ((𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∧ 𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) → (𝑓(𝑉 Walks 𝐸)𝑝 ↔ {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉})) |
9 | | fveq2 6103 |
. . . . . 6
⊢ (𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} → (#‘𝑓) = (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉})) |
10 | 9 | eqeq1d 2612 |
. . . . 5
⊢ (𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} → ((#‘𝑓) = 2 ↔ (#‘{〈0,
(◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2)) |
11 | 10 | adantr 480 |
. . . 4
⊢ ((𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∧ 𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) → ((#‘𝑓) = 2 ↔ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2)) |
12 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} → (𝑝‘0) = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0)) |
13 | 12 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} → (𝐴 = (𝑝‘0) ↔ 𝐴 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0))) |
14 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} → (𝑝‘1) = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘1)) |
15 | 14 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} → (𝐵 = (𝑝‘1) ↔ 𝐵 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘1))) |
16 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} → (𝑝‘2) = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2)) |
17 | 16 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} → (𝐶 = (𝑝‘2) ↔ 𝐶 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2))) |
18 | 13, 15, 17 | 3anbi123d 1391 |
. . . . 5
⊢ (𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) ↔ (𝐴 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) ∧ 𝐵 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘1) ∧ 𝐶 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2)))) |
19 | 18 | adantl 481 |
. . . 4
⊢ ((𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∧ 𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) → ((𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) ↔ (𝐴 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) ∧ 𝐵 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘1) ∧ 𝐶 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2)))) |
20 | 8, 11, 19 | 3anbi123d 1391 |
. . 3
⊢ ((𝑓 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∧ 𝑝 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) ↔ ({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2 ∧ (𝐴 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) ∧ 𝐵 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘1) ∧ 𝐶 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2))))) |
21 | 20 | spc2egv 3268 |
. 2
⊢
(({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} ∈ V ∧ {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∈ V) →
(({〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉} (𝑉 Walks 𝐸){〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ∧ (#‘{〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉}) = 2 ∧ (𝐴 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘0) ∧ 𝐵 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘1) ∧ 𝐶 = ({〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}‘2))) → ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
22 | 3, 7, 21 | mpsyl 66 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) |