Proof of Theorem constr3pthlem2
Step | Hyp | Ref
| Expression |
1 | | 3simpc 1053 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
2 | 1 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) |
3 | | 1z 11284 |
. . . . . 6
⊢ 1 ∈
ℤ |
4 | | 2z 11286 |
. . . . . 6
⊢ 2 ∈
ℤ |
5 | 3, 4 | pm3.2i 470 |
. . . . 5
⊢ (1 ∈
ℤ ∧ 2 ∈ ℤ) |
6 | 5 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → (1 ∈ ℤ ∧ 2 ∈
ℤ)) |
7 | | simpr 476 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → 𝐵 ≠ 𝐶) |
8 | | funprg 5854 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (1 ∈ ℤ ∧ 2 ∈
ℤ) ∧ 𝐵 ≠ 𝐶) → Fun {〈𝐵, 1〉, 〈𝐶, 2〉}) |
9 | 2, 6, 7, 8 | syl3anc 1318 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → Fun {〈𝐵, 1〉, 〈𝐶, 2〉}) |
10 | | cnvun 5457 |
. . . . . 6
⊢ ◡({〈1, 𝐵〉} ∪ {〈2, 𝐶〉}) = (◡{〈1, 𝐵〉} ∪ ◡{〈2, 𝐶〉}) |
11 | 3 | jctl 562 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → (1 ∈ ℤ ∧ 𝐵 ∈ 𝑉)) |
12 | 11 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (1 ∈ ℤ ∧ 𝐵 ∈ 𝑉)) |
13 | 12 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → (1 ∈ ℤ ∧ 𝐵 ∈ 𝑉)) |
14 | | cnvsng 5539 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ 𝐵
∈ 𝑉) → ◡{〈1, 𝐵〉} = {〈𝐵, 1〉}) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → ◡{〈1, 𝐵〉} = {〈𝐵, 1〉}) |
16 | 4 | jctl 562 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝑉 → (2 ∈ ℤ ∧ 𝐶 ∈ 𝑉)) |
17 | 16 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (2 ∈ ℤ ∧ 𝐶 ∈ 𝑉)) |
18 | 17 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → (2 ∈ ℤ ∧ 𝐶 ∈ 𝑉)) |
19 | | cnvsng 5539 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 𝐶
∈ 𝑉) → ◡{〈2, 𝐶〉} = {〈𝐶, 2〉}) |
20 | 18, 19 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → ◡{〈2, 𝐶〉} = {〈𝐶, 2〉}) |
21 | 15, 20 | uneq12d 3730 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → (◡{〈1, 𝐵〉} ∪ ◡{〈2, 𝐶〉}) = ({〈𝐵, 1〉} ∪ {〈𝐶, 2〉})) |
22 | 10, 21 | syl5eq 2656 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → ◡({〈1, 𝐵〉} ∪ {〈2, 𝐶〉}) = ({〈𝐵, 1〉} ∪ {〈𝐶, 2〉})) |
23 | | df-pr 4128 |
. . . . . 6
⊢ {〈1,
𝐵〉, 〈2, 𝐶〉} = ({〈1, 𝐵〉} ∪ {〈2, 𝐶〉}) |
24 | 23 | cnveqi 5219 |
. . . . 5
⊢ ◡{〈1, 𝐵〉, 〈2, 𝐶〉} = ◡({〈1, 𝐵〉} ∪ {〈2, 𝐶〉}) |
25 | | df-pr 4128 |
. . . . 5
⊢
{〈𝐵, 1〉,
〈𝐶, 2〉} =
({〈𝐵, 1〉} ∪
{〈𝐶,
2〉}) |
26 | 22, 24, 25 | 3eqtr4g 2669 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → ◡{〈1, 𝐵〉, 〈2, 𝐶〉} = {〈𝐵, 1〉, 〈𝐶, 2〉}) |
27 | 26 | funeqd 5825 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → (Fun ◡{〈1, 𝐵〉, 〈2, 𝐶〉} ↔ Fun {〈𝐵, 1〉, 〈𝐶, 2〉})) |
28 | 9, 27 | mpbird 246 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → Fun ◡{〈1, 𝐵〉, 〈2, 𝐶〉}) |
29 | | constr3cycl.f |
. . . . . . 7
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉} |
30 | | constr3cycl.p |
. . . . . . 7
⊢ 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) |
31 | 29, 30 | constr3pthlem1 26183 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃 ↾ (1..^(#‘𝐹))) = {〈1, 𝐵〉, 〈2, 𝐶〉}) |
32 | 31 | 3adant1 1072 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃 ↾ (1..^(#‘𝐹))) = {〈1, 𝐵〉, 〈2, 𝐶〉}) |
33 | 32 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → (𝑃 ↾ (1..^(#‘𝐹))) = {〈1, 𝐵〉, 〈2, 𝐶〉}) |
34 | 33 | cnveqd 5220 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → ◡(𝑃 ↾ (1..^(#‘𝐹))) = ◡{〈1, 𝐵〉, 〈2, 𝐶〉}) |
35 | 34 | funeqd 5825 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → (Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ↔ Fun ◡{〈1, 𝐵〉, 〈2, 𝐶〉})) |
36 | 28, 35 | mpbird 246 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐶) → Fun ◡(𝑃 ↾ (1..^(#‘𝐹)))) |