| Step | Hyp | Ref
| Expression |
| 1 | | wwlktovf1o.d |
. . . 4
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} |
| 2 | | wwlktovf1o.r |
. . . 4
⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} |
| 3 | | wwlktovf1o.f |
. . . 4
⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡‘1)) |
| 4 | 1, 2, 3 | wwlktovf 14995 |
. . 3
⊢ 𝐹:𝐷⟶𝑅 |
| 5 | 4 | a1i 11 |
. 2
⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷⟶𝑅) |
| 6 | | preq2 4734 |
. . . . . 6
⊢ (𝑛 = 𝑝 → {𝑃, 𝑛} = {𝑃, 𝑝}) |
| 7 | 6 | eleq1d 2826 |
. . . . 5
⊢ (𝑛 = 𝑝 → ({𝑃, 𝑛} ∈ 𝑋 ↔ {𝑃, 𝑝} ∈ 𝑋)) |
| 8 | 7, 2 | elrab2 3695 |
. . . 4
⊢ (𝑝 ∈ 𝑅 ↔ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) |
| 9 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋) → 𝑝 ∈ 𝑉) |
| 10 | 9 | anim2i 617 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → (𝑃 ∈ 𝑉 ∧ 𝑝 ∈ 𝑉)) |
| 11 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → {〈0, 𝑃〉, 〈1, 𝑝〉} = {〈0, 𝑃〉, 〈1, 𝑝〉}) |
| 12 | | wrdlen2i 14981 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑝 ∈ 𝑉) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = {〈0, 𝑃〉, 〈1, 𝑝〉} → (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)))) |
| 13 | 10, 11, 12 | sylc 65 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) |
| 14 | | prex 5437 |
. . . . . . . . . . 11
⊢ {〈0,
𝑃〉, 〈1, 𝑝〉} ∈
V |
| 15 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → {〈0, 𝑃〉, 〈1, 𝑝〉} ∈ V) |
| 16 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ↔ 𝑢 ∈ Word 𝑉)) |
| 17 | 16 | biimpd 229 |
. . . . . . . . . . . . . . . . . . 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 407 |
. . . . . . . . . . . . . 14
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → 𝑢 ∈ Word 𝑉) |
| 23 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 →
((♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2 ↔ (♯‘𝑢) = 2)) |
| 24 | 23 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 →
((♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2 → (♯‘𝑢) = 2)) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ((♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2 →
(♯‘𝑢) =
2)) |
| 26 | 25 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2 → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (♯‘𝑢) = 2)) |
| 27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} ∈
Word 𝑉 ∧
(♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (♯‘𝑢) = 2)) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (♯‘𝑢) = 2)) |
| 29 | 28 | impcom 407 |
. . . . . . . . . . . . . . 15
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → (♯‘𝑢) = 2) |
| 30 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = (𝑢‘0)) |
| 31 | 30 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ↔ (𝑢‘0) = 𝑃)) |
| 32 | 31 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 → (𝑢‘0) = 𝑃)) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 → (𝑢‘0) = 𝑃)) |
| 34 | 33 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉}‘0)
= 𝑃 → (({〈0,
𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (𝑢‘0) = 𝑃)) |
| 35 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝) → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (𝑢‘0) = 𝑃)) |
| 36 | 35 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → (({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (𝑢‘0) = 𝑃)) |
| 37 | 36 | impcom 407 |
. . . . . . . . . . . . . . 15
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → (𝑢‘0) = 𝑃) |
| 38 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = (𝑢‘1)) |
| 39 | 38 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝 ↔ (𝑢‘1) = 𝑝)) |
| 40 | 31, 39 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝) ↔ ((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝))) |
| 41 | | preq12 4735 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → {(𝑢‘0), (𝑢‘1)} = {𝑃, 𝑝}) |
| 42 | 41 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → {𝑃, 𝑝} = {(𝑢‘0), (𝑢‘1)}) |
| 43 | 42 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → ({𝑃, 𝑝} ∈ 𝑋 ↔ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
| 44 | 43 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
| 45 | 40, 44 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝) → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
| 46 | 45 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
| 47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
| 48 | 47 | com13 88 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑃, 𝑝} ∈ 𝑋 → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
| 49 | 48 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
| 50 | 49 | impcom 407 |
. . . . . . . . . . . . . . . 16
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
| 51 | 50 | imp 406 |
. . . . . . . . . . . . . . 15
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋) |
| 52 | 29, 37, 51 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
| 53 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉}‘1)
= 𝑝 ↔ 𝑝 = ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1)) |
| 54 | 38 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (𝑝 = ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) ↔ 𝑝 = (𝑢‘1))) |
| 55 | 54 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (𝑝 = ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) → 𝑝 = (𝑢‘1))) |
| 56 | 53, 55 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . 19
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → (({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝 → 𝑝 = (𝑢‘1))) |
| 57 | 56 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉}‘1)
= 𝑝 → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → 𝑝 = (𝑢‘1))) |
| 58 | 57 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 → 𝑝 = (𝑢‘1))) |
| 59 | 58 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0,
𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → 𝑝 = (𝑢‘1))) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → 𝑝 = (𝑢‘1))) |
| 61 | 60 | imp 406 |
. . . . . . . . . . . . . 14
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → 𝑝 = (𝑢‘1)) |
| 62 | 22, 52, 61 | jca31 514 |
. . . . . . . . . . . . 13
⊢
((({〈0, 𝑃〉, 〈1, 𝑝〉} = 𝑢 ∧ (𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝))) → ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))) |
| 63 | 62 | exp31 419 |
. . . . . . . . . . . 12
⊢
({〈0, 𝑃〉,
〈1, 𝑝〉} = 𝑢 → ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))))) |
| 64 | 63 | eqcoms 2745 |
. . . . . . . . . . 11
⊢ (𝑢 = {〈0, 𝑃〉, 〈1, 𝑝〉} → ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))))) |
| 65 | 64 | impcom 407 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) ∧ 𝑢 = {〈0, 𝑃〉, 〈1, 𝑝〉}) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0,
𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))) |
| 66 | 15, 65 | spcimedv 3595 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ((({〈0, 𝑃〉, 〈1, 𝑝〉} ∈ Word 𝑉 ∧ (♯‘{〈0, 𝑃〉, 〈1, 𝑝〉}) = 2) ∧ (({〈0,
𝑃〉, 〈1, 𝑝〉}‘0) = 𝑃 ∧ ({〈0, 𝑃〉, 〈1, 𝑝〉}‘1) = 𝑝)) → ∃𝑢((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))) |
| 67 | 13, 66 | mpd 15 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))) |
| 68 | | fveqeq2 6915 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑢 → ((♯‘𝑤) = 2 ↔ (♯‘𝑢) = 2)) |
| 69 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0)) |
| 70 | 69 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑃 ↔ (𝑢‘0) = 𝑃)) |
| 71 | | fveq1 6905 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑢 → (𝑤‘1) = (𝑢‘1)) |
| 72 | 69, 71 | preq12d 4741 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑢 → {(𝑤‘0), (𝑤‘1)} = {(𝑢‘0), (𝑢‘1)}) |
| 73 | 72 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑢 → ({(𝑤‘0), (𝑤‘1)} ∈ 𝑋 ↔ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
| 74 | 68, 70, 73 | 3anbi123d 1438 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑢 → (((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋) ↔ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
| 75 | 74 | elrab 3692 |
. . . . . . . . . 10
⊢ (𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ↔ (𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
| 76 | 75 | anbi1i 624 |
. . . . . . . . 9
⊢ ((𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1)) ↔ ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))) |
| 77 | 76 | exbii 1848 |
. . . . . . . 8
⊢
(∃𝑢(𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1)) ↔ ∃𝑢((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))) |
| 78 | 67, 77 | sylibr 234 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢(𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1))) |
| 79 | | df-rex 3071 |
. . . . . . 7
⊢
(∃𝑢 ∈
{𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}𝑝 = (𝑢‘1) ↔ ∃𝑢(𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1))) |
| 80 | 78, 79 | sylibr 234 |
. . . . . 6
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}𝑝 = (𝑢‘1)) |
| 81 | 1 | rexeqi 3325 |
. . . . . 6
⊢
(∃𝑢 ∈
𝐷 𝑝 = (𝑢‘1) ↔ ∃𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}𝑝 = (𝑢‘1)) |
| 82 | 80, 81 | sylibr 234 |
. . . . 5
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢 ∈ 𝐷 𝑝 = (𝑢‘1)) |
| 83 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑡 = 𝑢 → (𝑡‘1) = (𝑢‘1)) |
| 84 | | fvex 6919 |
. . . . . . . 8
⊢ (𝑢‘1) ∈
V |
| 85 | 83, 3, 84 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑢 ∈ 𝐷 → (𝐹‘𝑢) = (𝑢‘1)) |
| 86 | 85 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑢 ∈ 𝐷 → (𝑝 = (𝐹‘𝑢) ↔ 𝑝 = (𝑢‘1))) |
| 87 | 86 | rexbiia 3092 |
. . . . 5
⊢
(∃𝑢 ∈
𝐷 𝑝 = (𝐹‘𝑢) ↔ ∃𝑢 ∈ 𝐷 𝑝 = (𝑢‘1)) |
| 88 | 82, 87 | sylibr 234 |
. . . 4
⊢ ((𝑃 ∈ 𝑉 ∧ (𝑝 ∈ 𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢 ∈ 𝐷 𝑝 = (𝐹‘𝑢)) |
| 89 | 8, 88 | sylan2b 594 |
. . 3
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑝 ∈ 𝑅) → ∃𝑢 ∈ 𝐷 𝑝 = (𝐹‘𝑢)) |
| 90 | 89 | ralrimiva 3146 |
. 2
⊢ (𝑃 ∈ 𝑉 → ∀𝑝 ∈ 𝑅 ∃𝑢 ∈ 𝐷 𝑝 = (𝐹‘𝑢)) |
| 91 | | dffo3 7122 |
. 2
⊢ (𝐹:𝐷–onto→𝑅 ↔ (𝐹:𝐷⟶𝑅 ∧ ∀𝑝 ∈ 𝑅 ∃𝑢 ∈ 𝐷 𝑝 = (𝐹‘𝑢))) |
| 92 | 5, 90, 91 | sylanbrc 583 |
1
⊢ (𝑃 ∈ 𝑉 → 𝐹:𝐷–onto→𝑅) |