Proof of Theorem constr3lem4
Step | Hyp | Ref
| Expression |
1 | | 0z 11265 |
. . . . . 6
⊢ 0 ∈
ℤ |
2 | | 1z 11284 |
. . . . . 6
⊢ 1 ∈
ℤ |
3 | 1, 2 | pm3.2i 470 |
. . . . 5
⊢ (0 ∈
ℤ ∧ 1 ∈ ℤ) |
4 | 3 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (0 ∈ ℤ ∧ 1 ∈
ℤ)) |
5 | | 3simpa 1051 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
6 | | 0ne1 10965 |
. . . . 5
⊢ 0 ≠
1 |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 0 ≠ 1) |
8 | | fnprg 5861 |
. . . 4
⊢ (((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 0 ≠ 1) → {〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0,
1}) |
9 | 4, 5, 7, 8 | syl3anc 1318 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1}) |
10 | | 2z 11286 |
. . . . . 6
⊢ 2 ∈
ℤ |
11 | | 3nn0 11187 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
12 | 10, 11 | pm3.2i 470 |
. . . . 5
⊢ (2 ∈
ℤ ∧ 3 ∈ ℕ0) |
13 | 12 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (2 ∈ ℤ ∧ 3 ∈
ℕ0)) |
14 | | pm3.22 464 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
15 | 14 | 3adant2 1073 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
16 | | 2re 10967 |
. . . . . 6
⊢ 2 ∈
ℝ |
17 | | 2lt3 11072 |
. . . . . 6
⊢ 2 <
3 |
18 | 16, 17 | ltneii 10029 |
. . . . 5
⊢ 2 ≠
3 |
19 | 18 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 2 ≠ 3) |
20 | | fnprg 5861 |
. . . 4
⊢ (((2
∈ ℤ ∧ 3 ∈ ℕ0) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ 2 ≠ 3) → {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2,
3}) |
21 | 13, 15, 19, 20 | syl3anc 1318 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3}) |
22 | | 0ne2 11116 |
. . . . 5
⊢ 0 ≠
2 |
23 | | 1ne2 11117 |
. . . . 5
⊢ 1 ≠
2 |
24 | | 3ne0 10992 |
. . . . . 6
⊢ 3 ≠
0 |
25 | 24 | necomi 2836 |
. . . . 5
⊢ 0 ≠
3 |
26 | | 1re 9918 |
. . . . . 6
⊢ 1 ∈
ℝ |
27 | | 1lt3 11073 |
. . . . . 6
⊢ 1 <
3 |
28 | 26, 27 | ltneii 10029 |
. . . . 5
⊢ 1 ≠
3 |
29 | | disjpr2 4194 |
. . . . 5
⊢ (((0 ≠
2 ∧ 1 ≠ 2) ∧ (0 ≠ 3 ∧ 1 ≠ 3)) → ({0, 1} ∩ {2, 3})
= ∅) |
30 | 22, 23, 25, 28, 29 | mp4an 705 |
. . . 4
⊢ ({0, 1}
∩ {2, 3}) = ∅ |
31 | 30 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({0, 1} ∩ {2, 3}) =
∅) |
32 | 9, 21, 31 | 3jca 1235 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅)) |
33 | | constr3cycl.p |
. . . . . 6
⊢ 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) |
34 | 33 | fveq1i 6104 |
. . . . 5
⊢ (𝑃‘0) = (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})‘0) |
35 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
36 | 35 | prid1 4241 |
. . . . . . . . 9
⊢ 0 ∈
{0, 1} |
37 | 36 | jctr 563 |
. . . . . . . 8
⊢ (({0, 1}
∩ {2, 3}) = ∅ → (({0, 1} ∩ {2, 3}) = ∅ ∧ 0 ∈
{0, 1})) |
38 | 37 | 3anim3i 1243 |
. . . . . . 7
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} Fn {0, 1}
∧ {〈2, 𝐶〉,
〈3, 𝐴〉} Fn {2, 3}
∧ ({0, 1} ∩ {2, 3}) = ∅) → ({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ (({0, 1}
∩ {2, 3}) = ∅ ∧ 0 ∈ {0, 1}))) |
39 | 38 | adantr 480 |
. . . . . 6
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ (({0, 1}
∩ {2, 3}) = ∅ ∧ 0 ∈ {0, 1}))) |
40 | | fvun1 6179 |
. . . . . 6
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} Fn {0, 1}
∧ {〈2, 𝐶〉,
〈3, 𝐴〉} Fn {2, 3}
∧ (({0, 1} ∩ {2, 3}) = ∅ ∧ 0 ∈ {0, 1})) →
(({〈0, 𝐴〉,
〈1, 𝐵〉} ∪
{〈2, 𝐶〉, 〈3,
𝐴〉})‘0) =
({〈0, 𝐴〉,
〈1, 𝐵〉}‘0)) |
41 | 39, 40 | syl 17 |
. . . . 5
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})‘0) = ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0)) |
42 | 34, 41 | syl5eq 2656 |
. . . 4
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑃‘0) = ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0)) |
43 | | fvpr1g 6363 |
. . . . . . 7
⊢ ((0
∈ ℤ ∧ 𝐴
∈ 𝑉 ∧ 0 ≠ 1)
→ ({〈0, 𝐴〉,
〈1, 𝐵〉}‘0)
= 𝐴) |
44 | 1, 6, 43 | mp3an13 1407 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴) |
45 | 44 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴) |
46 | 45 | adantl 481 |
. . . 4
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘0) = 𝐴) |
47 | 42, 46 | eqtrd 2644 |
. . 3
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑃‘0) = 𝐴) |
48 | 33 | fveq1i 6104 |
. . . . 5
⊢ (𝑃‘1) = (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})‘1) |
49 | | 1ex 9914 |
. . . . . . . . . 10
⊢ 1 ∈
V |
50 | 49 | prid2 4242 |
. . . . . . . . 9
⊢ 1 ∈
{0, 1} |
51 | 50 | jctr 563 |
. . . . . . . 8
⊢ (({0, 1}
∩ {2, 3}) = ∅ → (({0, 1} ∩ {2, 3}) = ∅ ∧ 1 ∈
{0, 1})) |
52 | 51 | 3anim3i 1243 |
. . . . . . 7
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} Fn {0, 1}
∧ {〈2, 𝐶〉,
〈3, 𝐴〉} Fn {2, 3}
∧ ({0, 1} ∩ {2, 3}) = ∅) → ({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ (({0, 1}
∩ {2, 3}) = ∅ ∧ 1 ∈ {0, 1}))) |
53 | 52 | adantr 480 |
. . . . . 6
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ (({0, 1}
∩ {2, 3}) = ∅ ∧ 1 ∈ {0, 1}))) |
54 | | fvun1 6179 |
. . . . . 6
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} Fn {0, 1}
∧ {〈2, 𝐶〉,
〈3, 𝐴〉} Fn {2, 3}
∧ (({0, 1} ∩ {2, 3}) = ∅ ∧ 1 ∈ {0, 1})) →
(({〈0, 𝐴〉,
〈1, 𝐵〉} ∪
{〈2, 𝐶〉, 〈3,
𝐴〉})‘1) =
({〈0, 𝐴〉,
〈1, 𝐵〉}‘1)) |
55 | 53, 54 | syl 17 |
. . . . 5
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})‘1) = ({〈0, 𝐴〉, 〈1, 𝐵〉}‘1)) |
56 | 48, 55 | syl5eq 2656 |
. . . 4
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑃‘1) = ({〈0, 𝐴〉, 〈1, 𝐵〉}‘1)) |
57 | | fvpr2g 6364 |
. . . . . . 7
⊢ ((1
∈ ℝ ∧ 𝐵
∈ 𝑉 ∧ 0 ≠ 1)
→ ({〈0, 𝐴〉,
〈1, 𝐵〉}‘1)
= 𝐵) |
58 | 26, 6, 57 | mp3an13 1407 |
. . . . . 6
⊢ (𝐵 ∈ 𝑉 → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘1) = 𝐵) |
59 | 58 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘1) = 𝐵) |
60 | 59 | adantl 481 |
. . . 4
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈0, 𝐴〉, 〈1, 𝐵〉}‘1) = 𝐵) |
61 | 56, 60 | eqtrd 2644 |
. . 3
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑃‘1) = 𝐵) |
62 | 33 | fveq1i 6104 |
. . . . . 6
⊢ (𝑃‘2) = (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})‘2) |
63 | | 2ex 10969 |
. . . . . . . . . . 11
⊢ 2 ∈
V |
64 | 63 | prid1 4241 |
. . . . . . . . . 10
⊢ 2 ∈
{2, 3} |
65 | 64 | jctr 563 |
. . . . . . . . 9
⊢ (({0, 1}
∩ {2, 3}) = ∅ → (({0, 1} ∩ {2, 3}) = ∅ ∧ 2 ∈
{2, 3})) |
66 | 65 | 3anim3i 1243 |
. . . . . . . 8
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} Fn {0, 1}
∧ {〈2, 𝐶〉,
〈3, 𝐴〉} Fn {2, 3}
∧ ({0, 1} ∩ {2, 3}) = ∅) → ({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ (({0, 1}
∩ {2, 3}) = ∅ ∧ 2 ∈ {2, 3}))) |
67 | 66 | adantr 480 |
. . . . . . 7
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ (({0, 1}
∩ {2, 3}) = ∅ ∧ 2 ∈ {2, 3}))) |
68 | | fvun2 6180 |
. . . . . . 7
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} Fn {0, 1}
∧ {〈2, 𝐶〉,
〈3, 𝐴〉} Fn {2, 3}
∧ (({0, 1} ∩ {2, 3}) = ∅ ∧ 2 ∈ {2, 3})) →
(({〈0, 𝐴〉,
〈1, 𝐵〉} ∪
{〈2, 𝐶〉, 〈3,
𝐴〉})‘2) =
({〈2, 𝐶〉,
〈3, 𝐴〉}‘2)) |
69 | 67, 68 | syl 17 |
. . . . . 6
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})‘2) = ({〈2, 𝐶〉, 〈3, 𝐴〉}‘2)) |
70 | 62, 69 | syl5eq 2656 |
. . . . 5
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑃‘2) = ({〈2, 𝐶〉, 〈3, 𝐴〉}‘2)) |
71 | | fvpr1g 6363 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 𝐶
∈ 𝑉 ∧ 2 ≠ 3)
→ ({〈2, 𝐶〉,
〈3, 𝐴〉}‘2)
= 𝐶) |
72 | 10, 18, 71 | mp3an13 1407 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑉 → ({〈2, 𝐶〉, 〈3, 𝐴〉}‘2) = 𝐶) |
73 | 72 | 3ad2ant3 1077 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({〈2, 𝐶〉, 〈3, 𝐴〉}‘2) = 𝐶) |
74 | 73 | adantl 481 |
. . . . 5
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈2, 𝐶〉, 〈3, 𝐴〉}‘2) = 𝐶) |
75 | 70, 74 | eqtrd 2644 |
. . . 4
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑃‘2) = 𝐶) |
76 | 33 | fveq1i 6104 |
. . . . . 6
⊢ (𝑃‘3) = (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})‘3) |
77 | | 3ex 10973 |
. . . . . . . . . . 11
⊢ 3 ∈
V |
78 | 77 | prid2 4242 |
. . . . . . . . . 10
⊢ 3 ∈
{2, 3} |
79 | 78 | jctr 563 |
. . . . . . . . 9
⊢ (({0, 1}
∩ {2, 3}) = ∅ → (({0, 1} ∩ {2, 3}) = ∅ ∧ 3 ∈
{2, 3})) |
80 | 79 | 3anim3i 1243 |
. . . . . . . 8
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} Fn {0, 1}
∧ {〈2, 𝐶〉,
〈3, 𝐴〉} Fn {2, 3}
∧ ({0, 1} ∩ {2, 3}) = ∅) → ({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ (({0, 1}
∩ {2, 3}) = ∅ ∧ 3 ∈ {2, 3}))) |
81 | 80 | adantr 480 |
. . . . . . 7
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ (({0, 1}
∩ {2, 3}) = ∅ ∧ 3 ∈ {2, 3}))) |
82 | | fvun2 6180 |
. . . . . . 7
⊢
(({〈0, 𝐴〉,
〈1, 𝐵〉} Fn {0, 1}
∧ {〈2, 𝐶〉,
〈3, 𝐴〉} Fn {2, 3}
∧ (({0, 1} ∩ {2, 3}) = ∅ ∧ 3 ∈ {2, 3})) →
(({〈0, 𝐴〉,
〈1, 𝐵〉} ∪
{〈2, 𝐶〉, 〈3,
𝐴〉})‘3) =
({〈2, 𝐶〉,
〈3, 𝐴〉}‘3)) |
83 | 81, 82 | syl 17 |
. . . . . 6
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})‘3) = ({〈2, 𝐶〉, 〈3, 𝐴〉}‘3)) |
84 | 76, 83 | syl5eq 2656 |
. . . . 5
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑃‘3) = ({〈2, 𝐶〉, 〈3, 𝐴〉}‘3)) |
85 | | fvpr2g 6364 |
. . . . . . . 8
⊢ ((3
∈ ℕ0 ∧ 𝐴 ∈ 𝑉 ∧ 2 ≠ 3) → ({〈2, 𝐶〉, 〈3, 𝐴〉}‘3) = 𝐴) |
86 | 11, 18, 85 | mp3an13 1407 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ({〈2, 𝐶〉, 〈3, 𝐴〉}‘3) = 𝐴) |
87 | 86 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({〈2, 𝐶〉, 〈3, 𝐴〉}‘3) = 𝐴) |
88 | 87 | adantl 481 |
. . . . 5
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ({〈2, 𝐶〉, 〈3, 𝐴〉}‘3) = 𝐴) |
89 | 84, 88 | eqtrd 2644 |
. . . 4
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑃‘3) = 𝐴) |
90 | 75, 89 | jca 553 |
. . 3
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴)) |
91 | 47, 61, 90 | jca31 555 |
. 2
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉} Fn {0, 1} ∧ {〈2, 𝐶〉, 〈3, 𝐴〉} Fn {2, 3} ∧ ({0, 1}
∩ {2, 3}) = ∅) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴))) |
92 | 32, 91 | mpancom 700 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐴))) |