Step | Hyp | Ref
| Expression |
1 | | wrd2f1tovbij.d |
. . 3
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} |
2 | | wrd2f1tovbij.r |
. . 3
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} |
3 | | wrd2f1tovbij.f |
. . 3
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1)) |
4 | 1, 2, 3 | wwlktovf 13547 |
. 2
⊢ 𝐹:𝐷⟶𝑅 |
5 | | fveq1 6102 |
. . . . . 6
⊢ (𝑡 = 𝑥 → (𝑡‘1) = (𝑥‘1)) |
6 | | fvex 6113 |
. . . . . 6
⊢ (𝑥‘1) ∈
V |
7 | 5, 3, 6 | fvmpt 6191 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → (𝐹‘𝑥) = (𝑥‘1)) |
8 | | fveq1 6102 |
. . . . . 6
⊢ (𝑡 = 𝑦 → (𝑡‘1) = (𝑦‘1)) |
9 | | fvex 6113 |
. . . . . 6
⊢ (𝑦‘1) ∈
V |
10 | 8, 3, 9 | fvmpt 6191 |
. . . . 5
⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) = (𝑦‘1)) |
11 | 7, 10 | eqeqan12d 2626 |
. . . 4
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝑥‘1) = (𝑦‘1))) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (#‘𝑤) = (#‘𝑥)) |
13 | 12 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ((#‘𝑤) = 2 ↔ (#‘𝑥) = 2)) |
14 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0)) |
15 | 14 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ((𝑤‘0) = 𝑃 ↔ (𝑥‘0) = 𝑃)) |
16 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑤‘1) = (𝑥‘1)) |
17 | 14, 16 | preq12d 4220 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → {(𝑤‘0), (𝑤‘1)} = {(𝑥‘0), (𝑥‘1)}) |
18 | 17 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑤 = 𝑥 → ({(𝑤‘0), (𝑤‘1)} ∈ 𝑋 ↔ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) |
19 | 13, 15, 18 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑤 = 𝑥 → (((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋) ↔ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋))) |
20 | 19, 1 | elrab2 3333 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋))) |
21 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (#‘𝑤) = (#‘𝑦)) |
22 | 21 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → ((#‘𝑤) = 2 ↔ (#‘𝑦) = 2)) |
23 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0)) |
24 | 23 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → ((𝑤‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃)) |
25 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤‘1) = (𝑦‘1)) |
26 | 23, 25 | preq12d 4220 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → {(𝑤‘0), (𝑤‘1)} = {(𝑦‘0), (𝑦‘1)}) |
27 | 26 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → ({(𝑤‘0), (𝑤‘1)} ∈ 𝑋 ↔ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋)) |
28 | 22, 24, 27 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋) ↔ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) |
29 | 28, 1 | elrab2 3333 |
. . . . 5
⊢ (𝑦 ∈ 𝐷 ↔ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) |
30 | | simp1 1054 |
. . . . . . . . . 10
⊢
(((#‘𝑥) = 2
∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋) → (#‘𝑥) = 2) |
31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) → (#‘𝑥) = 2) |
32 | | simp1 1054 |
. . . . . . . . . . 11
⊢
(((#‘𝑦) = 2
∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋) → (#‘𝑦) = 2) |
33 | 32 | eqcomd 2616 |
. . . . . . . . . 10
⊢
(((#‘𝑦) = 2
∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋) → 2 = (#‘𝑦)) |
34 | 33 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋)) → 2 = (#‘𝑦)) |
35 | 31, 34 | sylan9eq 2664 |
. . . . . . . 8
⊢ (((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) → (#‘𝑥) = (#‘𝑦)) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) ∧ (𝑥‘1) = (𝑦‘1)) → (#‘𝑥) = (#‘𝑦)) |
37 | | simp2 1055 |
. . . . . . . . . . 11
⊢
(((#‘𝑥) = 2
∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋) → (𝑥‘0) = 𝑃) |
38 | 37 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) → (𝑥‘0) = 𝑃) |
39 | | simp2 1055 |
. . . . . . . . . . . 12
⊢
(((#‘𝑦) = 2
∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋) → (𝑦‘0) = 𝑃) |
40 | 39 | eqcomd 2616 |
. . . . . . . . . . 11
⊢
(((#‘𝑦) = 2
∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋) → 𝑃 = (𝑦‘0)) |
41 | 40 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋)) → 𝑃 = (𝑦‘0)) |
42 | 38, 41 | sylan9eq 2664 |
. . . . . . . . 9
⊢ (((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) → (𝑥‘0) = (𝑦‘0)) |
43 | 42 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) ∧ (𝑥‘1) = (𝑦‘1)) → (𝑥‘0) = (𝑦‘0)) |
44 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) ∧ (𝑥‘1) = (𝑦‘1)) → (𝑥‘1) = (𝑦‘1)) |
45 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢
((#‘𝑥) = 2
→ (0..^(#‘𝑥)) =
(0..^2)) |
46 | | fzo0to2pr 12420 |
. . . . . . . . . . . . 13
⊢ (0..^2) =
{0, 1} |
47 | 45, 46 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢
((#‘𝑥) = 2
→ (0..^(#‘𝑥)) =
{0, 1}) |
48 | 47 | raleqdv 3121 |
. . . . . . . . . . 11
⊢
((#‘𝑥) = 2
→ (∀𝑖 ∈
(0..^(#‘𝑥))(𝑥‘𝑖) = (𝑦‘𝑖) ↔ ∀𝑖 ∈ {0, 1} (𝑥‘𝑖) = (𝑦‘𝑖))) |
49 | | c0ex 9913 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
50 | | 1ex 9914 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
51 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 0 → (𝑥‘𝑖) = (𝑥‘0)) |
52 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 0 → (𝑦‘𝑖) = (𝑦‘0)) |
53 | 51, 52 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑖 = 0 → ((𝑥‘𝑖) = (𝑦‘𝑖) ↔ (𝑥‘0) = (𝑦‘0))) |
54 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (𝑥‘𝑖) = (𝑥‘1)) |
55 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (𝑦‘𝑖) = (𝑦‘1)) |
56 | 54, 55 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑖 = 1 → ((𝑥‘𝑖) = (𝑦‘𝑖) ↔ (𝑥‘1) = (𝑦‘1))) |
57 | 49, 50, 53, 56 | ralpr 4185 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
{0, 1} (𝑥‘𝑖) = (𝑦‘𝑖) ↔ ((𝑥‘0) = (𝑦‘0) ∧ (𝑥‘1) = (𝑦‘1))) |
58 | 48, 57 | syl6bb 275 |
. . . . . . . . . 10
⊢
((#‘𝑥) = 2
→ (∀𝑖 ∈
(0..^(#‘𝑥))(𝑥‘𝑖) = (𝑦‘𝑖) ↔ ((𝑥‘0) = (𝑦‘0) ∧ (𝑥‘1) = (𝑦‘1)))) |
59 | 58 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢
(((#‘𝑥) = 2
∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋) → (∀𝑖 ∈ (0..^(#‘𝑥))(𝑥‘𝑖) = (𝑦‘𝑖) ↔ ((𝑥‘0) = (𝑦‘0) ∧ (𝑥‘1) = (𝑦‘1)))) |
60 | 59 | ad3antlr 763 |
. . . . . . . 8
⊢ ((((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) ∧ (𝑥‘1) = (𝑦‘1)) → (∀𝑖 ∈ (0..^(#‘𝑥))(𝑥‘𝑖) = (𝑦‘𝑖) ↔ ((𝑥‘0) = (𝑦‘0) ∧ (𝑥‘1) = (𝑦‘1)))) |
61 | 43, 44, 60 | mpbir2and 959 |
. . . . . . 7
⊢ ((((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) ∧ (𝑥‘1) = (𝑦‘1)) → ∀𝑖 ∈ (0..^(#‘𝑥))(𝑥‘𝑖) = (𝑦‘𝑖)) |
62 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) → 𝑥 ∈ Word 𝑉) |
63 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋)) → 𝑦 ∈ Word 𝑉) |
64 | 62, 63 | anim12i 588 |
. . . . . . . . 9
⊢ (((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) → (𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉)) |
65 | 64 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) ∧ (𝑥‘1) = (𝑦‘1)) → (𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉)) |
66 | | eqwrd 13201 |
. . . . . . . 8
⊢ ((𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉) → (𝑥 = 𝑦 ↔ ((#‘𝑥) = (#‘𝑦) ∧ ∀𝑖 ∈ (0..^(#‘𝑥))(𝑥‘𝑖) = (𝑦‘𝑖)))) |
67 | 65, 66 | syl 17 |
. . . . . . 7
⊢ ((((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) ∧ (𝑥‘1) = (𝑦‘1)) → (𝑥 = 𝑦 ↔ ((#‘𝑥) = (#‘𝑦) ∧ ∀𝑖 ∈ (0..^(#‘𝑥))(𝑥‘𝑖) = (𝑦‘𝑖)))) |
68 | 36, 61, 67 | mpbir2and 959 |
. . . . . 6
⊢ ((((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) ∧ (𝑥‘1) = (𝑦‘1)) → 𝑥 = 𝑦) |
69 | 68 | ex 449 |
. . . . 5
⊢ (((𝑥 ∈ Word 𝑉 ∧ ((#‘𝑥) = 2 ∧ (𝑥‘0) = 𝑃 ∧ {(𝑥‘0), (𝑥‘1)} ∈ 𝑋)) ∧ (𝑦 ∈ Word 𝑉 ∧ ((#‘𝑦) = 2 ∧ (𝑦‘0) = 𝑃 ∧ {(𝑦‘0), (𝑦‘1)} ∈ 𝑋))) → ((𝑥‘1) = (𝑦‘1) → 𝑥 = 𝑦)) |
70 | 20, 29, 69 | syl2anb 495 |
. . . 4
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝑥‘1) = (𝑦‘1) → 𝑥 = 𝑦)) |
71 | 11, 70 | sylbid 229 |
. . 3
⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
72 | 71 | rgen2a 2960 |
. 2
⊢
∀𝑥 ∈
𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) |
73 | | dff13 6416 |
. 2
⊢ (𝐹:𝐷–1-1→𝑅 ↔ (𝐹:𝐷⟶𝑅 ∧ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
74 | 4, 72, 73 | mpbir2an 957 |
1
⊢ 𝐹:𝐷–1-1→𝑅 |