Step | Hyp | Ref
| Expression |
1 | | c0ex 9913 |
. . . . 5
⊢ 0 ∈
V |
2 | | 1ex 9914 |
. . . . 5
⊢ 1 ∈
V |
3 | | 2ex 10969 |
. . . . 5
⊢ 2 ∈
V |
4 | | fvex 6113 |
. . . . 5
⊢ (◡𝐸‘{𝐴, 𝐵}) ∈ V |
5 | | fvex 6113 |
. . . . 5
⊢ (◡𝐸‘{𝐵, 𝐶}) ∈ V |
6 | | fvex 6113 |
. . . . 5
⊢ (◡𝐸‘{𝐶, 𝐴}) ∈ V |
7 | | 0ne1 10965 |
. . . . 5
⊢ 0 ≠
1 |
8 | | 0ne2 11116 |
. . . . 5
⊢ 0 ≠
2 |
9 | | 1ne2 11117 |
. . . . 5
⊢ 1 ≠
2 |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | ftp 6329 |
. . . 4
⊢ {〈0,
(◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉}:{0, 1, 2}⟶{(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})} |
11 | | constr3cycl.f |
. . . . . 6
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉} |
12 | 11 | a1i 11 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉}) |
13 | | fzo0to3tp 12421 |
. . . . . 6
⊢ (0..^3) =
{0, 1, 2} |
14 | 13 | a1i 11 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (0..^3) = {0, 1,
2}) |
15 | 12, 14 | feq12d 5946 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐹:(0..^3)⟶{(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})} ↔ {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉}:{0, 1, 2}⟶{(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})})) |
16 | 10, 15 | mpbiri 247 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹:(0..^3)⟶{(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})}) |
17 | | usgraf 25875 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2}) |
18 | | f1f1orn 6061 |
. . . . . 6
⊢ (𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2} → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
19 | | f1ocnvdm 6440 |
. . . . . . . . 9
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝐴, 𝐵} ∈ ran 𝐸) → (◡𝐸‘{𝐴, 𝐵}) ∈ dom 𝐸) |
20 | 19 | 3ad2antr1 1219 |
. . . . . . . 8
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (◡𝐸‘{𝐴, 𝐵}) ∈ dom 𝐸) |
21 | | f1ocnvdm 6440 |
. . . . . . . . 9
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) → (◡𝐸‘{𝐵, 𝐶}) ∈ dom 𝐸) |
22 | 21 | 3ad2antr2 1220 |
. . . . . . . 8
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (◡𝐸‘{𝐵, 𝐶}) ∈ dom 𝐸) |
23 | | f1ocnvdm 6440 |
. . . . . . . . 9
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → (◡𝐸‘{𝐶, 𝐴}) ∈ dom 𝐸) |
24 | 23 | 3ad2antr3 1221 |
. . . . . . . 8
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (◡𝐸‘{𝐶, 𝐴}) ∈ dom 𝐸) |
25 | 20, 22, 24 | 3jca 1235 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((◡𝐸‘{𝐴, 𝐵}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐵, 𝐶}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐶, 𝐴}) ∈ dom 𝐸)) |
26 | 25 | ex 449 |
. . . . . 6
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ((◡𝐸‘{𝐴, 𝐵}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐵, 𝐶}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐶, 𝐴}) ∈ dom 𝐸))) |
27 | 17, 18, 26 | 3syl 18 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) → ((◡𝐸‘{𝐴, 𝐵}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐵, 𝐶}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐶, 𝐴}) ∈ dom 𝐸))) |
28 | 27 | imp 444 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → ((◡𝐸‘{𝐴, 𝐵}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐵, 𝐶}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐶, 𝐴}) ∈ dom 𝐸)) |
29 | 4, 5, 6 | tpss 4308 |
. . . 4
⊢ (((◡𝐸‘{𝐴, 𝐵}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐵, 𝐶}) ∈ dom 𝐸 ∧ (◡𝐸‘{𝐶, 𝐴}) ∈ dom 𝐸) ↔ {(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})} ⊆ dom 𝐸) |
30 | 28, 29 | sylib 207 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → {(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})} ⊆ dom 𝐸) |
31 | 16, 30 | jca 553 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → (𝐹:(0..^3)⟶{(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})} ∧ {(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})} ⊆ dom 𝐸)) |
32 | | fss 5969 |
. 2
⊢ ((𝐹:(0..^3)⟶{(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})} ∧ {(◡𝐸‘{𝐴, 𝐵}), (◡𝐸‘{𝐵, 𝐶}), (◡𝐸‘{𝐶, 𝐴})} ⊆ dom 𝐸) → 𝐹:(0..^3)⟶dom 𝐸) |
33 | | iswrdi 13164 |
. 2
⊢ (𝐹:(0..^3)⟶dom 𝐸 → 𝐹 ∈ Word dom 𝐸) |
34 | 31, 32, 33 | 3syl 18 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) → 𝐹 ∈ Word dom 𝐸) |