Step | Hyp | Ref
| Expression |
1 | | wrdexg 13315 |
. . . 4
⊢ (𝑉 ∈ 𝑌 → Word 𝑉 ∈ V) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉) → Word 𝑉 ∈ V) |
3 | | rabexg 4812 |
. . 3
⊢ (Word
𝑉 ∈ V → {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ∈ V) |
4 | | mptexg 6484 |
. . 3
⊢ ({𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ∈ V → (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)) ∈ V) |
5 | 2, 3, 4 | 3syl 18 |
. 2
⊢ ((𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉) → (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)) ∈ V) |
6 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑤 = 𝑢 → (#‘𝑤) = (#‘𝑢)) |
7 | 6 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = 𝑢 → ((#‘𝑤) = 2 ↔ (#‘𝑢) = 2)) |
8 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0)) |
9 | 8 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑃 ↔ (𝑢‘0) = 𝑃)) |
10 | | fveq1 6190 |
. . . . . . . 8
⊢ (𝑤 = 𝑢 → (𝑤‘1) = (𝑢‘1)) |
11 | 8, 10 | preq12d 4276 |
. . . . . . 7
⊢ (𝑤 = 𝑢 → {(𝑤‘0), (𝑤‘1)} = {(𝑢‘0), (𝑢‘1)}) |
12 | 11 | eleq1d 2686 |
. . . . . 6
⊢ (𝑤 = 𝑢 → ({(𝑤‘0), (𝑤‘1)} ∈ 𝑋 ↔ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) |
13 | 7, 9, 12 | 3anbi123d 1399 |
. . . . 5
⊢ (𝑤 = 𝑢 → (((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋) ↔ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))) |
14 | 13 | cbvrabv 3199 |
. . . 4
⊢ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} = {𝑢 ∈ Word 𝑉 ∣ ((#‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)} |
15 | | preq2 4269 |
. . . . . 6
⊢ (𝑛 = 𝑝 → {𝑃, 𝑛} = {𝑃, 𝑝}) |
16 | 15 | eleq1d 2686 |
. . . . 5
⊢ (𝑛 = 𝑝 → ({𝑃, 𝑛} ∈ 𝑋 ↔ {𝑃, 𝑝} ∈ 𝑋)) |
17 | 16 | cbvrabv 3199 |
. . . 4
⊢ {𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} = {𝑝 ∈ 𝑉 ∣ {𝑃, 𝑝} ∈ 𝑋} |
18 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (#‘𝑡) = (#‘𝑤)) |
19 | 18 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((#‘𝑡) = 2 ↔ (#‘𝑤) = 2)) |
20 | | fveq1 6190 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → (𝑡‘0) = (𝑤‘0)) |
21 | 20 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ((𝑡‘0) = 𝑃 ↔ (𝑤‘0) = 𝑃)) |
22 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑡 = 𝑤 → (𝑡‘1) = (𝑤‘1)) |
23 | 20, 22 | preq12d 4276 |
. . . . . . . 8
⊢ (𝑡 = 𝑤 → {(𝑡‘0), (𝑡‘1)} = {(𝑤‘0), (𝑤‘1)}) |
24 | 23 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → ({(𝑡‘0), (𝑡‘1)} ∈ 𝑋 ↔ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)) |
25 | 19, 21, 24 | 3anbi123d 1399 |
. . . . . 6
⊢ (𝑡 = 𝑤 → (((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋) ↔ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋))) |
26 | 25 | cbvrabv 3199 |
. . . . 5
⊢ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} |
27 | | mpteq1 4737 |
. . . . 5
⊢ ({𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} → (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)) = (𝑥 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ↦ (𝑥‘1))) |
28 | 26, 27 | ax-mp 5 |
. . . 4
⊢ (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)) = (𝑥 ∈ {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ↦ (𝑥‘1)) |
29 | 14, 17, 28 | wwlktovf1o 13702 |
. . 3
⊢ (𝑃 ∈ 𝑉 → (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)):{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}) |
30 | 29 | adantl 482 |
. 2
⊢ ((𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉) → (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)):{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}) |
31 | | f1oeq1 6127 |
. . 3
⊢ (𝑓 = (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)) → (𝑓:{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} ↔ (𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)):{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋})) |
32 | 31 | spcegv 3294 |
. 2
⊢ ((𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)) ∈ V → ((𝑥 ∈ {𝑡 ∈ Word 𝑉 ∣ ((#‘𝑡) = 2 ∧ (𝑡‘0) = 𝑃 ∧ {(𝑡‘0), (𝑡‘1)} ∈ 𝑋)} ↦ (𝑥‘1)):{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋} → ∃𝑓 𝑓:{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋})) |
33 | 5, 30, 32 | sylc 65 |
1
⊢ ((𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉) → ∃𝑓 𝑓:{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}) |