Proof of Theorem constr3pthlem1
Step | Hyp | Ref
| Expression |
1 | | df-pr 4128 |
. . . . . . 7
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉} = ({〈0, 𝐴〉} ∪ {〈1, 𝐵〉}) |
2 | 1 | reseq1i 5313 |
. . . . . 6
⊢
({〈0, 𝐴〉,
〈1, 𝐵〉} ↾
{1, 2}) = (({〈0, 𝐴〉} ∪ {〈1, 𝐵〉}) ↾ {1, 2}) |
3 | | resundir 5331 |
. . . . . 6
⊢
(({〈0, 𝐴〉}
∪ {〈1, 𝐵〉})
↾ {1, 2}) = (({〈0, 𝐴〉} ↾ {1, 2}) ∪ ({〈1,
𝐵〉} ↾ {1,
2})) |
4 | 2, 3 | eqtri 2632 |
. . . . 5
⊢
({〈0, 𝐴〉,
〈1, 𝐵〉} ↾
{1, 2}) = (({〈0, 𝐴〉} ↾ {1, 2}) ∪ ({〈1,
𝐵〉} ↾ {1,
2})) |
5 | | 0ne1 10965 |
. . . . . . . . 9
⊢ 0 ≠
1 |
6 | | 0ne2 11116 |
. . . . . . . . 9
⊢ 0 ≠
2 |
7 | 5, 6 | nelpri 4149 |
. . . . . . . 8
⊢ ¬ 0
∈ {1, 2} |
8 | | ressnop0 6325 |
. . . . . . . 8
⊢ (¬ 0
∈ {1, 2} → ({〈0, 𝐴〉} ↾ {1, 2}) =
∅) |
9 | 7, 8 | ax-mp 5 |
. . . . . . 7
⊢
({〈0, 𝐴〉}
↾ {1, 2}) = ∅ |
10 | 9 | uneq1i 3725 |
. . . . . 6
⊢
(({〈0, 𝐴〉}
↾ {1, 2}) ∪ ({〈1, 𝐵〉} ↾ {1, 2})) = (∅ ∪
({〈1, 𝐵〉} ↾
{1, 2})) |
11 | | uncom 3719 |
. . . . . . . 8
⊢ (∅
∪ ({〈1, 𝐵〉}
↾ {1, 2})) = (({〈1, 𝐵〉} ↾ {1, 2}) ∪
∅) |
12 | | un0 3919 |
. . . . . . . 8
⊢
(({〈1, 𝐵〉}
↾ {1, 2}) ∪ ∅) = ({〈1, 𝐵〉} ↾ {1, 2}) |
13 | 11, 12 | eqtri 2632 |
. . . . . . 7
⊢ (∅
∪ ({〈1, 𝐵〉}
↾ {1, 2})) = ({〈1, 𝐵〉} ↾ {1, 2}) |
14 | | 1re 9918 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
15 | 14 | jctl 562 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → (1 ∈ ℝ ∧ 𝐵 ∈ 𝑉)) |
16 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (1 ∈ ℝ ∧ 𝐵 ∈ 𝑉)) |
17 | | funsng 5851 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ 𝐵
∈ 𝑉) → Fun
{〈1, 𝐵〉}) |
18 | | funrel 5821 |
. . . . . . . . 9
⊢ (Fun
{〈1, 𝐵〉} →
Rel {〈1, 𝐵〉}) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → Rel {〈1, 𝐵〉}) |
20 | | dmsnopss 5525 |
. . . . . . . . 9
⊢ dom
{〈1, 𝐵〉} ⊆
{1} |
21 | | snsspr1 4285 |
. . . . . . . . 9
⊢ {1}
⊆ {1, 2} |
22 | 20, 21 | sstri 3577 |
. . . . . . . 8
⊢ dom
{〈1, 𝐵〉} ⊆
{1, 2} |
23 | | relssres 5357 |
. . . . . . . 8
⊢ ((Rel
{〈1, 𝐵〉} ∧
dom {〈1, 𝐵〉}
⊆ {1, 2}) → ({〈1, 𝐵〉} ↾ {1, 2}) = {〈1, 𝐵〉}) |
24 | 19, 22, 23 | sylancl 693 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ({〈1, 𝐵〉} ↾ {1, 2}) = {〈1, 𝐵〉}) |
25 | 13, 24 | syl5eq 2656 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (∅ ∪ ({〈1, 𝐵〉} ↾ {1, 2})) =
{〈1, 𝐵〉}) |
26 | 10, 25 | syl5eq 2656 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (({〈0, 𝐴〉} ↾ {1, 2}) ∪ ({〈1,
𝐵〉} ↾ {1, 2})) =
{〈1, 𝐵〉}) |
27 | 4, 26 | syl5eq 2656 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ {1, 2}) = {〈1, 𝐵〉}) |
28 | | df-pr 4128 |
. . . . . . 7
⊢ {〈2,
𝐶〉, 〈3, 𝐴〉} = ({〈2, 𝐶〉} ∪ {〈3, 𝐴〉}) |
29 | 28 | reseq1i 5313 |
. . . . . 6
⊢
({〈2, 𝐶〉,
〈3, 𝐴〉} ↾
{1, 2}) = (({〈2, 𝐶〉} ∪ {〈3, 𝐴〉}) ↾ {1, 2}) |
30 | | resundir 5331 |
. . . . . 6
⊢
(({〈2, 𝐶〉}
∪ {〈3, 𝐴〉})
↾ {1, 2}) = (({〈2, 𝐶〉} ↾ {1, 2}) ∪ ({〈3,
𝐴〉} ↾ {1,
2})) |
31 | 29, 30 | eqtri 2632 |
. . . . 5
⊢
({〈2, 𝐶〉,
〈3, 𝐴〉} ↾
{1, 2}) = (({〈2, 𝐶〉} ↾ {1, 2}) ∪ ({〈3,
𝐴〉} ↾ {1,
2})) |
32 | | 1lt3 11073 |
. . . . . . . . . 10
⊢ 1 <
3 |
33 | 14, 32 | gtneii 10028 |
. . . . . . . . 9
⊢ 3 ≠
1 |
34 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
35 | | 2lt3 11072 |
. . . . . . . . . 10
⊢ 2 <
3 |
36 | 34, 35 | gtneii 10028 |
. . . . . . . . 9
⊢ 3 ≠
2 |
37 | 33, 36 | nelpri 4149 |
. . . . . . . 8
⊢ ¬ 3
∈ {1, 2} |
38 | | ressnop0 6325 |
. . . . . . . 8
⊢ (¬ 3
∈ {1, 2} → ({〈3, 𝐴〉} ↾ {1, 2}) =
∅) |
39 | 37, 38 | ax-mp 5 |
. . . . . . 7
⊢
({〈3, 𝐴〉}
↾ {1, 2}) = ∅ |
40 | 39 | uneq2i 3726 |
. . . . . 6
⊢
(({〈2, 𝐶〉}
↾ {1, 2}) ∪ ({〈3, 𝐴〉} ↾ {1, 2})) = (({〈2, 𝐶〉} ↾ {1, 2}) ∪
∅) |
41 | | un0 3919 |
. . . . . . 7
⊢
(({〈2, 𝐶〉}
↾ {1, 2}) ∪ ∅) = ({〈2, 𝐶〉} ↾ {1, 2}) |
42 | | 2z 11286 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
43 | | funsng 5851 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 𝐶
∈ 𝑊) → Fun
{〈2, 𝐶〉}) |
44 | 42, 43 | mpan 702 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝑊 → Fun {〈2, 𝐶〉}) |
45 | | funrel 5821 |
. . . . . . . . . 10
⊢ (Fun
{〈2, 𝐶〉} →
Rel {〈2, 𝐶〉}) |
46 | 44, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝐶 ∈ 𝑊 → Rel {〈2, 𝐶〉}) |
47 | 46 | adantl 481 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → Rel {〈2, 𝐶〉}) |
48 | | dmsnopss 5525 |
. . . . . . . . 9
⊢ dom
{〈2, 𝐶〉} ⊆
{2} |
49 | | snsspr2 4286 |
. . . . . . . . 9
⊢ {2}
⊆ {1, 2} |
50 | 48, 49 | sstri 3577 |
. . . . . . . 8
⊢ dom
{〈2, 𝐶〉} ⊆
{1, 2} |
51 | | relssres 5357 |
. . . . . . . 8
⊢ ((Rel
{〈2, 𝐶〉} ∧
dom {〈2, 𝐶〉}
⊆ {1, 2}) → ({〈2, 𝐶〉} ↾ {1, 2}) = {〈2, 𝐶〉}) |
52 | 47, 50, 51 | sylancl 693 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ({〈2, 𝐶〉} ↾ {1, 2}) = {〈2, 𝐶〉}) |
53 | 41, 52 | syl5eq 2656 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (({〈2, 𝐶〉} ↾ {1, 2}) ∪ ∅) =
{〈2, 𝐶〉}) |
54 | 40, 53 | syl5eq 2656 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (({〈2, 𝐶〉} ↾ {1, 2}) ∪ ({〈3,
𝐴〉} ↾ {1, 2})) =
{〈2, 𝐶〉}) |
55 | 31, 54 | syl5eq 2656 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ({〈2, 𝐶〉, 〈3, 𝐴〉} ↾ {1, 2}) = {〈2, 𝐶〉}) |
56 | 27, 55 | uneq12d 3730 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (({〈0, 𝐴〉, 〈1, 𝐵〉} ↾ {1, 2}) ∪ ({〈2,
𝐶〉, 〈3, 𝐴〉} ↾ {1, 2})) =
({〈1, 𝐵〉} ∪
{〈2, 𝐶〉})) |
57 | | resundir 5331 |
. . 3
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} ∪
{〈2, 𝐶〉, 〈3,
𝐴〉}) ↾ {1, 2}) =
(({〈0, 𝐴〉,
〈1, 𝐵〉} ↾
{1, 2}) ∪ ({〈2, 𝐶〉, 〈3, 𝐴〉} ↾ {1, 2})) |
58 | | df-pr 4128 |
. . 3
⊢ {〈1,
𝐵〉, 〈2, 𝐶〉} = ({〈1, 𝐵〉} ∪ {〈2, 𝐶〉}) |
59 | 56, 57, 58 | 3eqtr4g 2669 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) ↾ {1, 2}) = {〈1, 𝐵〉, 〈2, 𝐶〉}) |
60 | | constr3cycl.p |
. . 3
⊢ 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) |
61 | | id 22 |
. . . . 5
⊢ (𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) → 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})) |
62 | | constr3cycl.f |
. . . . . . . . 9
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉} |
63 | 62, 60 | constr3lem2 26174 |
. . . . . . . 8
⊢
(#‘𝐹) =
3 |
64 | 63 | oveq2i 6560 |
. . . . . . 7
⊢
(1..^(#‘𝐹)) =
(1..^3) |
65 | | 3z 11287 |
. . . . . . . 8
⊢ 3 ∈
ℤ |
66 | | fzoval 12340 |
. . . . . . . 8
⊢ (3 ∈
ℤ → (1..^3) = (1...(3 − 1))) |
67 | 65, 66 | ax-mp 5 |
. . . . . . 7
⊢ (1..^3) =
(1...(3 − 1)) |
68 | | 3m1e2 11014 |
. . . . . . . . . 10
⊢ (3
− 1) = 2 |
69 | | df-2 10956 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
70 | 68, 69 | eqtri 2632 |
. . . . . . . . 9
⊢ (3
− 1) = (1 + 1) |
71 | 70 | oveq2i 6560 |
. . . . . . . 8
⊢ (1...(3
− 1)) = (1...(1 + 1)) |
72 | | 1z 11284 |
. . . . . . . . 9
⊢ 1 ∈
ℤ |
73 | | fzpr 12266 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → (1...(1 + 1)) = {1, (1 + 1)}) |
74 | 72, 73 | ax-mp 5 |
. . . . . . . 8
⊢ (1...(1 +
1)) = {1, (1 + 1)} |
75 | | 1p1e2 11011 |
. . . . . . . . 9
⊢ (1 + 1) =
2 |
76 | 75 | preq2i 4216 |
. . . . . . . 8
⊢ {1, (1 +
1)} = {1, 2} |
77 | 71, 74, 76 | 3eqtri 2636 |
. . . . . . 7
⊢ (1...(3
− 1)) = {1, 2} |
78 | 64, 67, 77 | 3eqtri 2636 |
. . . . . 6
⊢
(1..^(#‘𝐹)) =
{1, 2} |
79 | 78 | a1i 11 |
. . . . 5
⊢ (𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) → (1..^(#‘𝐹)) = {1, 2}) |
80 | 61, 79 | reseq12d 5318 |
. . . 4
⊢ (𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) → (𝑃 ↾ (1..^(#‘𝐹))) = (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) ↾ {1, 2})) |
81 | 80 | eqeq1d 2612 |
. . 3
⊢ (𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) → ((𝑃 ↾ (1..^(#‘𝐹))) = {〈1, 𝐵〉, 〈2, 𝐶〉} ↔ (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) ↾ {1, 2}) = {〈1, 𝐵〉, 〈2, 𝐶〉})) |
82 | 60, 81 | ax-mp 5 |
. 2
⊢ ((𝑃 ↾ (1..^(#‘𝐹))) = {〈1, 𝐵〉, 〈2, 𝐶〉} ↔ (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) ↾ {1, 2}) =
{〈1, 𝐵〉, 〈2,
𝐶〉}) |
83 | 59, 82 | sylibr 223 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝑃 ↾ (1..^(#‘𝐹))) = {〈1, 𝐵〉, 〈2, 𝐶〉}) |