Metamath Proof Explorer

Theorem wrd2f1tovbij

Description: There is a bijection between words of length two with a fixed first symbol contained in a pair and the symbols contained in a pair together with the fixed symbol. (Contributed by Alexander van der Vekens, 28-Jul-2018)

Ref Expression
Assertion wrd2f1tovbij ⊢V∈Y∧P∈V→∃ff:w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X⟶1-1 onton∈V|Pn∈X

Proof

Step Hyp Ref Expression
1 wrdexg ⊢V∈Y→WordV∈V
2 1 adantr ⊢V∈Y∧P∈V→WordV∈V
3 rabexg ⊢WordV∈V→t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X∈V
4 mptexg ⊢t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X∈V→x∈t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X⟼x⁡1∈V
5 2 3 4 3syl ⊢V∈Y∧P∈V→x∈t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X⟼x⁡1∈V
6 fveqeq2 ⊢w=u→w=2↔u=2
7 fveq1 ⊢w=u→w⁡0=u⁡0
8 7 eqeq1d ⊢w=u→w⁡0=P↔u⁡0=P
9 fveq1 ⊢w=u→w⁡1=u⁡1
10 7 9 preq12d ⊢w=u→w⁡0w⁡1=u⁡0u⁡1
11 10 eleq1d ⊢w=u→w⁡0w⁡1∈X↔u⁡0u⁡1∈X
12 6 8 11 3anbi123d ⊢w=u→w=2∧w⁡0=P∧w⁡0w⁡1∈X↔u=2∧u⁡0=P∧u⁡0u⁡1∈X
13 12 cbvrabv ⊢w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X=u∈WordV|u=2∧u⁡0=P∧u⁡0u⁡1∈X
14 preq2 ⊢n=p→Pn=Pp
15 14 eleq1d ⊢n=p→Pn∈X↔Pp∈X
16 15 cbvrabv ⊢n∈V|Pn∈X=p∈V|Pp∈X
17 fveqeq2 ⊢t=w→t=2↔w=2
18 fveq1 ⊢t=w→t⁡0=w⁡0
19 18 eqeq1d ⊢t=w→t⁡0=P↔w⁡0=P
20 fveq1 ⊢t=w→t⁡1=w⁡1
21 18 20 preq12d ⊢t=w→t⁡0t⁡1=w⁡0w⁡1
22 21 eleq1d ⊢t=w→t⁡0t⁡1∈X↔w⁡0w⁡1∈X
23 17 19 22 3anbi123d ⊢t=w→t=2∧t⁡0=P∧t⁡0t⁡1∈X↔w=2∧w⁡0=P∧w⁡0w⁡1∈X
24 23 cbvrabv ⊢t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X=w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X
25 24 mpteq1i ⊢x∈t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X⟼x⁡1=x∈w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X⟼x⁡1
26 13 16 25 wwlktovf1o ⊢P∈V→x∈t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X⟼x⁡1:w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X⟶1-1 onton∈V|Pn∈X
27 26 adantl ⊢V∈Y∧P∈V→x∈t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X⟼x⁡1:w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X⟶1-1 onton∈V|Pn∈X
28 f1oeq1 ⊢f=x∈t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X⟼x⁡1→f:w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X⟶1-1 onton∈V|Pn∈X↔x∈t∈WordV|t=2∧t⁡0=P∧t⁡0t⁡1∈X⟼x⁡1:w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X⟶1-1 onton∈V|Pn∈X
29 5 27 28 spcedv ⊢V∈Y∧P∈V→∃ff:w∈WordV|w=2∧w⁡0=P∧w⁡0w⁡1∈X⟶1-1 onton∈V|Pn∈X