Step |
Hyp |
Ref |
Expression |
1 |
|
wrdexg |
⊢ ( 𝑉 ∈ 𝑌 → Word 𝑉 ∈ V ) |
2 |
1
|
adantr |
⊢ ( ( 𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉 ) → Word 𝑉 ∈ V ) |
3 |
|
rabexg |
⊢ ( Word 𝑉 ∈ V → { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ∈ V ) |
4 |
|
mptexg |
⊢ ( { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ∈ V → ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) ∈ V ) |
5 |
2 3 4
|
3syl |
⊢ ( ( 𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) ∈ V ) |
6 |
|
fveqeq2 |
⊢ ( 𝑤 = 𝑢 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ 𝑢 ) = 2 ) ) |
7 |
|
fveq1 |
⊢ ( 𝑤 = 𝑢 → ( 𝑤 ‘ 0 ) = ( 𝑢 ‘ 0 ) ) |
8 |
7
|
eqeq1d |
⊢ ( 𝑤 = 𝑢 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑢 ‘ 0 ) = 𝑃 ) ) |
9 |
|
fveq1 |
⊢ ( 𝑤 = 𝑢 → ( 𝑤 ‘ 1 ) = ( 𝑢 ‘ 1 ) ) |
10 |
7 9
|
preq12d |
⊢ ( 𝑤 = 𝑢 → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ) |
11 |
10
|
eleq1d |
⊢ ( 𝑤 = 𝑢 → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) |
12 |
6 8 11
|
3anbi123d |
⊢ ( 𝑤 = 𝑢 → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) ) |
13 |
12
|
cbvrabv |
⊢ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } = { 𝑢 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) } |
14 |
|
preq2 |
⊢ ( 𝑛 = 𝑝 → { 𝑃 , 𝑛 } = { 𝑃 , 𝑝 } ) |
15 |
14
|
eleq1d |
⊢ ( 𝑛 = 𝑝 → ( { 𝑃 , 𝑛 } ∈ 𝑋 ↔ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) |
16 |
15
|
cbvrabv |
⊢ { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } = { 𝑝 ∈ 𝑉 ∣ { 𝑃 , 𝑝 } ∈ 𝑋 } |
17 |
|
fveqeq2 |
⊢ ( 𝑡 = 𝑤 → ( ( ♯ ‘ 𝑡 ) = 2 ↔ ( ♯ ‘ 𝑤 ) = 2 ) ) |
18 |
|
fveq1 |
⊢ ( 𝑡 = 𝑤 → ( 𝑡 ‘ 0 ) = ( 𝑤 ‘ 0 ) ) |
19 |
18
|
eqeq1d |
⊢ ( 𝑡 = 𝑤 → ( ( 𝑡 ‘ 0 ) = 𝑃 ↔ ( 𝑤 ‘ 0 ) = 𝑃 ) ) |
20 |
|
fveq1 |
⊢ ( 𝑡 = 𝑤 → ( 𝑡 ‘ 1 ) = ( 𝑤 ‘ 1 ) ) |
21 |
18 20
|
preq12d |
⊢ ( 𝑡 = 𝑤 → { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } = { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ) |
22 |
21
|
eleq1d |
⊢ ( 𝑡 = 𝑤 → ( { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ) |
23 |
17 19 22
|
3anbi123d |
⊢ ( 𝑡 = 𝑤 → ( ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ) ) |
24 |
23
|
cbvrabv |
⊢ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } |
25 |
24
|
mpteq1i |
⊢ ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) = ( 𝑥 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) |
26 |
13 16 25
|
wwlktovf1o |
⊢ ( 𝑃 ∈ 𝑉 → ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } ) |
27 |
26
|
adantl |
⊢ ( ( 𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝑡 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) } ↦ ( 𝑥 ‘ 1 ) ) : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } ) |
28 |
|
f1oeq1 |
⊢ ( 𝑓 = ( 𝑥 ∈ { 𝑡 ∈ 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→ { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } ) ) |
29 |
5 27 28
|
spcedv |
⊢ ( ( 𝑉 ∈ 𝑌 ∧ 𝑃 ∈ 𝑉 ) → ∃ 𝑓 𝑓 : { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } –1-1-onto→ { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 } ) |