Step | Hyp | Ref
| Expression |
1 | | usgraedgrnv 25906 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
2 | 1 | ex 449 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))) |
3 | | usgraedgrnv 25906 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
4 | 3 | ex 449 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → ({𝐵, 𝐶} ∈ ran 𝐸 → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) |
5 | | usgraedgrnv 25906 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
6 | 5 | ex 449 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → ({𝐶, 𝐴} ∈ ran 𝐸 → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) |
7 | 2, 4, 6 | 3anim123d 1398 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)))) |
8 | 7 | imp 444 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉))) |
9 | | simpll 786 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑉) |
10 | | simprl 790 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐵 ∈ 𝑉) |
11 | | simprr 792 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐶 ∈ 𝑉) |
12 | | constr3cycl.f |
. . . . . . . 8
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉} |
13 | | constr3cycl.p |
. . . . . . . 8
⊢ 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) |
14 | 12, 13 | constr3lem4 26175 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴))) |
15 | 9, 10, 11, 14 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴))) |
16 | | usgraf 25875 |
. . . . . . . . . . . . 13
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2}) |
17 | | f1f1orn 6061 |
. . . . . . . . . . . . 13
⊢ (𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2} → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
18 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵}) |
19 | 18 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ({𝐴, 𝐵} ∈ ran 𝐸 → (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵})) |
20 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶}) |
21 | 20 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ({𝐵, 𝐶} ∈ ran 𝐸 → (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) |
22 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{𝐶, 𝐴})) = {𝐶, 𝐴}) |
23 | 22 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → ({𝐶, 𝐴} ∈ ran 𝐸 → (𝐸‘(◡𝐸‘{𝐶, 𝐴})) = {𝐶, 𝐴})) |
24 | 19, 21, 23 | 3anim123d 1398 |
. . . . . . . . . . . . 13
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶} ∧ (𝐸‘(◡𝐸‘{𝐶, 𝐴})) = {𝐶, 𝐴}))) |
25 | 16, 17, 24 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶} ∧ (𝐸‘(◡𝐸‘{𝐶, 𝐴})) = {𝐶, 𝐴}))) |
26 | 25 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶} ∧ (𝐸‘(◡𝐸‘{𝐶, 𝐴})) = {𝐶, 𝐴})) |
27 | 26 | adantl 481 |
. . . . . . . . . 10
⊢
((((((𝑃‘0) =
𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶} ∧ (𝐸‘(◡𝐸‘{𝐶, 𝐴})) = {𝐶, 𝐴})) |
28 | 12, 13 | constr3lem5 26176 |
. . . . . . . . . . 11
⊢ ((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) |
29 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) → (𝐸‘(𝐹‘0)) = (𝐸‘(◡𝐸‘{𝐴, 𝐵}))) |
30 | 29 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (𝐸‘(𝐹‘0)) = (𝐸‘(◡𝐸‘{𝐴, 𝐵}))) |
31 | 30 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ↔ (𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵})) |
32 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) → (𝐸‘(𝐹‘1)) = (𝐸‘(◡𝐸‘{𝐵, 𝐶}))) |
33 | 32 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (𝐸‘(𝐹‘1)) = (𝐸‘(◡𝐸‘{𝐵, 𝐶}))) |
34 | 33 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐸‘(𝐹‘1)) = {𝐵, 𝐶} ↔ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶})) |
35 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘2) = (◡𝐸‘{𝐶, 𝐴}) → (𝐸‘(𝐹‘2)) = (𝐸‘(◡𝐸‘{𝐶, 𝐴}))) |
36 | 35 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (𝐸‘(𝐹‘2)) = (𝐸‘(◡𝐸‘{𝐶, 𝐴}))) |
37 | 36 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → ((𝐸‘(𝐹‘2)) = {𝐶, 𝐴} ↔ (𝐸‘(◡𝐸‘{𝐶, 𝐴})) = {𝐶, 𝐴})) |
38 | 31, 34, 37 | 3anbi123d 1391 |
. . . . . . . . . . 11
⊢ (((𝐹‘0) = (◡𝐸‘{𝐴, 𝐵}) ∧ (𝐹‘1) = (◡𝐸‘{𝐵, 𝐶}) ∧ (𝐹‘2) = (◡𝐸‘{𝐶, 𝐴})) → (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶} ∧ (𝐸‘(𝐹‘2)) = {𝐶, 𝐴}) ↔ ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶} ∧ (𝐸‘(◡𝐸‘{𝐶, 𝐴})) = {𝐶, 𝐴}))) |
39 | 28, 38 | ax-mp 5 |
. . . . . . . . . 10
⊢ (((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶} ∧ (𝐸‘(𝐹‘2)) = {𝐶, 𝐴}) ↔ ((𝐸‘(◡𝐸‘{𝐴, 𝐵})) = {𝐴, 𝐵} ∧ (𝐸‘(◡𝐸‘{𝐵, 𝐶})) = {𝐵, 𝐶} ∧ (𝐸‘(◡𝐸‘{𝐶, 𝐴})) = {𝐶, 𝐴})) |
40 | 27, 39 | sylibr 223 |
. . . . . . . . 9
⊢
((((((𝑃‘0) =
𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶} ∧ (𝐸‘(𝐹‘2)) = {𝐶, 𝐴})) |
41 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (𝑃‘0) = 𝐴) |
42 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (𝑃‘1) = 𝐵) |
43 | 41, 42 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → {(𝑃‘0), (𝑃‘1)} = {𝐴, 𝐵}) |
44 | 43 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ↔ (𝐸‘(𝐹‘0)) = {𝐴, 𝐵})) |
45 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (𝑃‘2) = 𝐶) |
46 | 42, 45 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → {(𝑃‘1), (𝑃‘2)} = {𝐵, 𝐶}) |
47 | 46 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → ((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶})) |
48 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (𝑃‘3) = 𝐴) |
49 | 45, 48 | preq12d 4220 |
. . . . . . . . . . . 12
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → {(𝑃‘2), (𝑃‘3)} = {𝐶, 𝐴}) |
50 | 49 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → ((𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)} ↔ (𝐸‘(𝐹‘2)) = {𝐶, 𝐴})) |
51 | 44, 47, 50 | 3anbi123d 1391 |
. . . . . . . . . 10
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}) ↔ ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶} ∧ (𝐸‘(𝐹‘2)) = {𝐶, 𝐴}))) |
52 | 51 | ad2antrr 758 |
. . . . . . . . 9
⊢
((((((𝑃‘0) =
𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}) ↔ ((𝐸‘(𝐹‘0)) = {𝐴, 𝐵} ∧ (𝐸‘(𝐹‘1)) = {𝐵, 𝐶} ∧ (𝐸‘(𝐹‘2)) = {𝐶, 𝐴}))) |
53 | 40, 52 | mpbird 246 |
. . . . . . . 8
⊢
((((((𝑃‘0) =
𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ (𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸))) → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)})) |
54 | 53 | ex 449 |
. . . . . . 7
⊢
(((((𝑃‘0) =
𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}))) |
55 | 54 | ex 449 |
. . . . . 6
⊢ ((((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) → (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)})))) |
56 | 15, 55 | mpcom 37 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}))) |
57 | 56 | 3adant3 1074 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}))) |
58 | 8, 57 | mpcom 37 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)})) |
59 | | 0z 11265 |
. . . 4
⊢ 0 ∈
ℤ |
60 | | 1z 11284 |
. . . 4
⊢ 1 ∈
ℤ |
61 | | 2z 11286 |
. . . 4
⊢ 2 ∈
ℤ |
62 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝐹‘𝑘) = (𝐹‘0)) |
63 | 62 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 0 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘0))) |
64 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
65 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
66 | | 0p1e1 11009 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
67 | 65, 66 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
68 | 67 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1)) |
69 | 64, 68 | preq12d 4220 |
. . . . . 6
⊢ (𝑘 = 0 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)}) |
70 | 63, 69 | eqeq12d 2625 |
. . . . 5
⊢ (𝑘 = 0 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)})) |
71 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
72 | 71 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 1 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘1))) |
73 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝑃‘𝑘) = (𝑃‘1)) |
74 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
75 | | 1p1e2 11011 |
. . . . . . . . 9
⊢ (1 + 1) =
2 |
76 | 74, 75 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑘 = 1 → (𝑘 + 1) = 2) |
77 | 76 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2)) |
78 | 73, 77 | preq12d 4220 |
. . . . . 6
⊢ (𝑘 = 1 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)}) |
79 | 72, 78 | eqeq12d 2625 |
. . . . 5
⊢ (𝑘 = 1 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) |
80 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 2 → (𝐹‘𝑘) = (𝐹‘2)) |
81 | 80 | fveq2d 6107 |
. . . . . 6
⊢ (𝑘 = 2 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘2))) |
82 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 2 → (𝑃‘𝑘) = (𝑃‘2)) |
83 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = 2 → (𝑘 + 1) = (2 + 1)) |
84 | | 2p1e3 11028 |
. . . . . . . . 9
⊢ (2 + 1) =
3 |
85 | 83, 84 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑘 = 2 → (𝑘 + 1) = 3) |
86 | 85 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3)) |
87 | 82, 86 | preq12d 4220 |
. . . . . 6
⊢ (𝑘 = 2 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)}) |
88 | 81, 87 | eqeq12d 2625 |
. . . . 5
⊢ (𝑘 = 2 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)})) |
89 | 70, 79, 88 | raltpg 4183 |
. . . 4
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ) →
(∀𝑘 ∈ {0, 1, 2}
(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)}))) |
90 | 59, 60, 61, 89 | mp3an 1416 |
. . 3
⊢
(∀𝑘 ∈
{0, 1, 2} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ∧ (𝐸‘(𝐹‘2)) = {(𝑃‘2), (𝑃‘3)})) |
91 | 58, 90 | sylibr 223 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∀𝑘 ∈ {0, 1, 2} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
92 | 12, 13 | constr3lem2 26174 |
. . . . . 6
⊢
(#‘𝐹) =
3 |
93 | 92 | oveq2i 6560 |
. . . . 5
⊢
(0..^(#‘𝐹)) =
(0..^3) |
94 | | fzo0to3tp 12421 |
. . . . 5
⊢ (0..^3) =
{0, 1, 2} |
95 | 93, 94 | eqtri 2632 |
. . . 4
⊢
(0..^(#‘𝐹)) =
{0, 1, 2} |
96 | 95 | a1i 11 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (0..^(#‘𝐹)) = {0, 1, 2}) |
97 | 96 | raleqdv 3121 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1, 2} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) |
98 | 91, 97 | mpbird 246 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |