Proof of Theorem constr2spthlem1
Step | Hyp | Ref
| Expression |
1 | | 0z 11265 |
. . . 4
⊢ 0 ∈
ℤ |
2 | | 1z 11284 |
. . . 4
⊢ 1 ∈
ℤ |
3 | | 2z 11286 |
. . . 4
⊢ 2 ∈
ℤ |
4 | 1, 2, 3 | 3pm3.2i 1232 |
. . 3
⊢ (0 ∈
ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ) |
5 | | funtpg 5856 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (0 ∈ ℤ ∧ 1 ∈
ℤ ∧ 2 ∈ ℤ) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun {〈𝐴, 0〉, 〈𝐵, 1〉, 〈𝐶, 2〉}) |
6 | 4, 5 | mp3an2 1404 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun {〈𝐴, 0〉, 〈𝐵, 1〉, 〈𝐶, 2〉}) |
7 | | cnvun 5457 |
. . . . . . . 8
⊢ ◡({〈0, 𝐴〉} ∪ {〈1, 𝐵〉}) = (◡{〈0, 𝐴〉} ∪ ◡{〈1, 𝐵〉}) |
8 | 1 | jctl 562 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → (0 ∈ ℤ ∧ 𝐴 ∈ 𝑉)) |
9 | 8 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (0 ∈ ℤ ∧ 𝐴 ∈ 𝑉)) |
10 | | cnvsng 5539 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ 𝐴
∈ 𝑉) → ◡{〈0, 𝐴〉} = {〈𝐴, 0〉}) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ◡{〈0, 𝐴〉} = {〈𝐴, 0〉}) |
12 | 2 | jctl 562 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑉 → (1 ∈ ℤ ∧ 𝐵 ∈ 𝑉)) |
13 | 12 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (1 ∈ ℤ ∧ 𝐵 ∈ 𝑉)) |
14 | | cnvsng 5539 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ 𝐵
∈ 𝑉) → ◡{〈1, 𝐵〉} = {〈𝐵, 1〉}) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ◡{〈1, 𝐵〉} = {〈𝐵, 1〉}) |
16 | 11, 15 | uneq12d 3730 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (◡{〈0, 𝐴〉} ∪ ◡{〈1, 𝐵〉}) = ({〈𝐴, 0〉} ∪ {〈𝐵, 1〉})) |
17 | 7, 16 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ◡({〈0, 𝐴〉} ∪ {〈1, 𝐵〉}) = ({〈𝐴, 0〉} ∪ {〈𝐵, 1〉})) |
18 | | df-pr 4128 |
. . . . . . . . 9
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉} = ({〈0, 𝐴〉} ∪ {〈1, 𝐵〉}) |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {〈0, 𝐴〉, 〈1, 𝐵〉} = ({〈0, 𝐴〉} ∪ {〈1, 𝐵〉})) |
20 | 19 | cnveqd 5220 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ◡{〈0, 𝐴〉, 〈1, 𝐵〉} = ◡({〈0, 𝐴〉} ∪ {〈1, 𝐵〉})) |
21 | | df-pr 4128 |
. . . . . . . 8
⊢
{〈𝐴, 0〉,
〈𝐵, 1〉} =
({〈𝐴, 0〉} ∪
{〈𝐵,
1〉}) |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {〈𝐴, 0〉, 〈𝐵, 1〉} = ({〈𝐴, 0〉} ∪ {〈𝐵, 1〉})) |
23 | 17, 20, 22 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ◡{〈0, 𝐴〉, 〈1, 𝐵〉} = {〈𝐴, 0〉, 〈𝐵, 1〉}) |
24 | 3 | jctl 562 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑉 → (2 ∈ ℤ ∧ 𝐶 ∈ 𝑉)) |
25 | 24 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (2 ∈ ℤ ∧ 𝐶 ∈ 𝑉)) |
26 | | cnvsng 5539 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝐶
∈ 𝑉) → ◡{〈2, 𝐶〉} = {〈𝐶, 2〉}) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ◡{〈2, 𝐶〉} = {〈𝐶, 2〉}) |
28 | 23, 27 | uneq12d 3730 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (◡{〈0, 𝐴〉, 〈1, 𝐵〉} ∪ ◡{〈2, 𝐶〉}) = ({〈𝐴, 0〉, 〈𝐵, 1〉} ∪ {〈𝐶, 2〉})) |
29 | | 2pth.p |
. . . . . . 7
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
30 | 29 | cnveqi 5219 |
. . . . . 6
⊢ ◡𝑃 = ◡{〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
31 | | df-tp 4130 |
. . . . . . 7
⊢ {〈0,
𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉}) |
32 | 31 | cnveqi 5219 |
. . . . . 6
⊢ ◡{〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} = ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉}) |
33 | | cnvun 5457 |
. . . . . 6
⊢ ◡({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉}) = (◡{〈0, 𝐴〉, 〈1, 𝐵〉} ∪ ◡{〈2, 𝐶〉}) |
34 | 30, 32, 33 | 3eqtri 2636 |
. . . . 5
⊢ ◡𝑃 = (◡{〈0, 𝐴〉, 〈1, 𝐵〉} ∪ ◡{〈2, 𝐶〉}) |
35 | | df-tp 4130 |
. . . . 5
⊢
{〈𝐴, 0〉,
〈𝐵, 1〉,
〈𝐶, 2〉} =
({〈𝐴, 0〉,
〈𝐵, 1〉} ∪
{〈𝐶,
2〉}) |
36 | 28, 34, 35 | 3eqtr4g 2669 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ◡𝑃 = {〈𝐴, 0〉, 〈𝐵, 1〉, 〈𝐶, 2〉}) |
37 | 36 | funeqd 5825 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (Fun ◡𝑃 ↔ Fun {〈𝐴, 0〉, 〈𝐵, 1〉, 〈𝐶, 2〉})) |
38 | 37 | adantr 480 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (Fun ◡𝑃 ↔ Fun {〈𝐴, 0〉, 〈𝐵, 1〉, 〈𝐶, 2〉})) |
39 | 6, 38 | mpbird 246 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun ◡𝑃) |