Step | Hyp | Ref
| Expression |
1 | | wrd2f1tovbij.d |
. . . 4
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} |
2 | | wrd2f1tovbij.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} |
3 | | wrd2f1tovbij.f |
. . . 4
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1)) |
4 | 1, 2, 3 | wwlktovf 13547 |
. . 3
⊢ 𝐹:𝐷⟶𝑅 |
5 | 4 | a1i 11 |
. 2
⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷⟶𝑅) |
6 | | preq2 4213 |
. . . . . 6
⊢ (𝑛 = 𝑝 → {𝑃, 𝑛} = {𝑃, 𝑝}) |
7 | 6 | eleq1d 2672 |
. . . . 5
⊢ (𝑛 = 𝑝 → ({𝑃, 𝑛} ∈ 𝑋 ↔ {𝑃, 𝑝} ∈ 𝑋)) |
8 | 7, 2 | elrab2 3333 |
. . . 4
⊢ (𝑝 ∈ 𝑅 ↔ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) |
9 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋) → 𝑝 ∈ 𝑉) |
10 | 9 | anim2i 591 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → (𝑃 ∈ 𝑉 ∧ 𝑝 ∈ 𝑉)) |
11 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → {〈0, 𝑃〉, 〈1, 𝑝〉} = {〈0, 𝑃〉, 〈1, 𝑝〉}) |
12 | | wrdlen2i 13534 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑝 ∈ 𝑉) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = {〈0, 𝑃〉, 〈1, 𝑝〉} → (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)))) |
13 | 10, 11, 12 | sylc 63 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) |
14 | | prex 4836 |
. . . . . . . . . . 11
⊢ {〈0,
𝑃〉, 〈1, 𝑝〉} ∈
V |
15 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → {〈0, 𝑃〉, 〈1, 𝑝〉} ∈ V) |
16 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ↔ 𝑢 ∈ Word 𝑉)) |
17 | 16 | biimpd 218 |
. . . . . . . . . . . . . . . . . . 19
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 → 𝑢 ∈ Word 𝑉)) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 → 𝑢 ∈ Word 𝑉)) |
19 | 18 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} ∈
Word 𝑉 → (({〈0,
𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → 𝑢 ∈ Word 𝑉)) |
20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} ∈
Word 𝑉 ∧
(#‘{〈0, 𝑃〉,
〈1, 𝑝〉}) = 2)
→ (({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → 𝑢 ∈ Word 𝑉)) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → 𝑢 ∈ Word 𝑉)) |
22 | 21 | impcom 445 |
. . . . . . . . . . . . . 14
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → 𝑢 ∈ Word 𝑉) |
23 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = (#‘𝑢)) |
24 | 23 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((#‘{〈0,
𝑃〉, 〈1, 𝑝〉}) = 2 ↔
(#‘𝑢) =
2)) |
25 | 24 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((#‘{〈0,
𝑃〉, 〈1, 𝑝〉}) = 2 →
(#‘𝑢) =
2)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ((#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2 →
(#‘𝑢) =
2)) |
27 | 26 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2 → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (#‘𝑢) = 2)) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} ∈
Word 𝑉 ∧
(#‘{〈0, 𝑃〉,
〈1, 𝑝〉}) = 2)
→ (({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (#‘𝑢) = 2)) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (#‘𝑢) = 2)) |
30 | 29 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → (#‘𝑢) = 2) |
31 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = (𝑢‘0)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ↔ (𝑢‘0) = 𝑃)) |
33 | 32 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 → (𝑢‘0) = 𝑃)) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 → (𝑢‘0) = 𝑃)) |
35 | 34 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉}‘0)
= 𝑃 → (({〈0,
𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (𝑢‘0) = 𝑃)) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝) → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (𝑢‘0) = 𝑃)) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (𝑢‘0) = 𝑃)) |
38 | 37 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → (𝑢‘0) = 𝑃) |
39 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = (𝑢‘1)) |
40 | 39 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝 ↔ (𝑢‘1) = 𝑝)) |
41 | 32, 40 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝) ↔ ((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝))) |
42 | | preq12 4214 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → {(𝑢‘0), (𝑢‘1)} = {𝑃, 𝑝}) |
43 | 42 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → {𝑃, 𝑝} = {(𝑢‘0), (𝑢‘1)}) |
44 | 43 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → ({𝑃, 𝑝} ∈ 𝑋 ↔ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
45 | 44 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
46 | 41, 45 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝) → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
47 | 46 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
49 | 48 | com13 86 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑃, 𝑝} ∈ 𝑋 → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
50 | 49 | ad2antll 761 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
51 | 50 | impcom 445 |
. . . . . . . . . . . . . . . 16
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
52 | 51 | imp 444 |
. . . . . . . . . . . . . . 15
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋) |
53 | 30, 38, 52 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
54 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉}‘1)
= 𝑝 ↔ 𝑝 = ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1)) |
55 | 39 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (𝑝 = ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) ↔ 𝑝 = (𝑢‘1))) |
56 | 55 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (𝑝 = ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) → 𝑝 = (𝑢‘1))) |
57 | 54, 56 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . 19
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝 → 𝑝 = (𝑢‘1))) |
58 | 57 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉}‘1)
= 𝑝 → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → 𝑝 = (𝑢‘1))) |
59 | 58 | ad2antll 761 |
. . . . . . . . . . . . . . . . 17
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → 𝑝 = (𝑢‘1))) |
60 | 59 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → 𝑝 = (𝑢‘1))) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → 𝑝 = (𝑢‘1))) |
62 | 61 | imp 444 |
. . . . . . . . . . . . . 14
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → 𝑝 = (𝑢‘1)) |
63 | 22, 53, 62 | jca31 555 |
. . . . . . . . . . . . 13
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → ((𝑢 ∈ Word 𝑉 ∧ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))) |
64 | 63 | exp31 628 |
. . . . . . . . . . . 12
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ((𝑢 ∈ Word 𝑉 ∧ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))))) |
65 | 64 | eqcoms 2618 |
. . . . . . . . . . 11
⊢ (𝑢 = {〈0, 𝑃〉, 〈1, 𝑝〉} → ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ((𝑢 ∈ Word 𝑉 ∧ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))))) |
66 | 65 | impcom 445 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) ∧ 𝑢 = {〈0, 𝑃〉, 〈1, 𝑝〉}) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ((𝑢 ∈ Word 𝑉 ∧ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))) |
67 | 15, 66 | spcimedv 3265 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (#‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ∃𝑢((𝑢 ∈ Word 𝑉 ∧ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))) |
68 | 13, 67 | mpd 15 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢((𝑢 ∈ Word 𝑉 ∧ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))) |
69 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑢 → (#‘𝑤) = (#‘𝑢)) |
70 | 69 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑢 → ((#‘𝑤) = 2 ↔ (#‘𝑢) = 2)) |
71 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0)) |
72 | 71 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑃 ↔ (𝑢‘0) = 𝑃)) |
73 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑢 → (𝑤‘1) = (𝑢‘1)) |
74 | 71, 73 | preq12d 4220 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑢 → {(𝑤‘0), (𝑤‘1)} = {(𝑢‘0), (𝑢‘1)}) |
75 | 74 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑢 → ({(𝑤‘0), (𝑤‘1)} ∈ 𝑋 ↔ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
76 | 70, 72, 75 | 3anbi123d 1391 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑢 → (((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋) ↔ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
77 | 76 | elrab 3331 |
. . . . . . . . . 10
⊢ (𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ↔ (𝑢 ∈ Word 𝑉 ∧ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
78 | 77 | anbi1i 727 |
. . . . . . . . 9
⊢ ((𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1)) ↔ ((𝑢 ∈ Word 𝑉 ∧ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))) |
79 | 78 | exbii 1764 |
. . . . . . . 8
⊢
(∃𝑢(𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1)) ↔ ∃𝑢((𝑢 ∈ Word 𝑉 ∧ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))) |
80 | 68, 79 | sylibr 223 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢(𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1))) |
81 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑢 ∈
{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}𝑝 = (𝑢‘1) ↔ ∃𝑢(𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1))) |
82 | 80, 81 | sylibr 223 |
. . . . . 6
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}𝑝 = (𝑢‘1)) |
83 | 1 | rexeqi 3120 |
. . . . . 6
⊢
(∃𝑢 ∈
𝐷 𝑝 = (𝑢‘1) ↔ ∃𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}𝑝 = (𝑢‘1)) |
84 | 82, 83 | sylibr 223 |
. . . . 5
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢 ∈ 𝐷 𝑝 = (𝑢‘1)) |
85 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑡 = 𝑢 → (𝑡‘1) = (𝑢‘1)) |
86 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑢‘1) ∈
V |
87 | 85, 3, 86 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑢 ∈ 𝐷 → (𝐹‘𝑢) = (𝑢‘1)) |
88 | 87 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑢 ∈ 𝐷 → (𝑝 = (𝐹‘𝑢) ↔ 𝑝 = (𝑢‘1))) |
89 | 88 | rexbiia 3022 |
. . . . 5
⊢
(∃𝑢 ∈
𝐷 𝑝 = (𝐹‘𝑢) ↔ ∃𝑢 ∈ 𝐷 𝑝 = (𝑢‘1)) |
90 | 84, 89 | sylibr 223 |
. . . 4
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢 ∈ 𝐷 𝑝 = (𝐹‘𝑢)) |
91 | 8, 90 | sylan2b 491 |
. . 3
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑝 ∈ 𝑅) → ∃𝑢 ∈ 𝐷 𝑝 = (𝐹‘𝑢)) |
92 | 91 | ralrimiva 2949 |
. 2
⊢ (𝑃 ∈ 𝑉 → ∀𝑝 ∈ 𝑅 ∃𝑢 ∈ 𝐷 𝑝 = (𝐹‘𝑢)) |
93 | | dffo3 6282 |
. 2
⊢ (𝐹:𝐷–onto→𝑅 ↔ (𝐹:𝐷⟶𝑅 ∧ ∀𝑝 ∈ 𝑅 ∃𝑢 ∈ 𝐷 𝑝 = (𝐹‘𝑢))) |
94 | 5, 92, 93 | sylanbrc 695 |
1
⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–onto→𝑅) |