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 e. Y /\ P e. V ) -> E. f f : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } -1-1-onto-> { n e. V | { P , n } e. X } )

Proof

Step Hyp Ref Expression
1 wrdexg 
 |-  ( V e. Y -> Word V e. _V )
2 1 adantr 
 |-  ( ( V e. Y /\ P e. V ) -> Word V e. _V )
3 rabexg 
 |-  ( Word V e. _V -> { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } e. _V )
4 mptexg 
 |-  ( { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } e. _V -> ( x e. { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } |-> ( x ` 1 ) ) e. _V )
5 2 3 4 3syl 
 |-  ( ( V e. Y /\ P e. V ) -> ( x e. { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } |-> ( x ` 1 ) ) e. _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 ` 0 ) , ( w ` 1 ) } = { ( u ` 0 ) , ( u ` 1 ) } )
11 10 eleq1d 
 |-  ( w = u -> ( { ( w ` 0 ) , ( w ` 1 ) } e. X <-> { ( u ` 0 ) , ( u ` 1 ) } e. X ) )
12 6 8 11 3anbi123d 
 |-  ( w = u -> ( ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) <-> ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) ) )
13 12 cbvrabv 
 |-  { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } = { u e. Word V | ( ( # ` u ) = 2 /\ ( u ` 0 ) = P /\ { ( u ` 0 ) , ( u ` 1 ) } e. X ) }
14 preq2 
 |-  ( n = p -> { P , n } = { P , p } )
15 14 eleq1d 
 |-  ( n = p -> ( { P , n } e. X <-> { P , p } e. X ) )
16 15 cbvrabv 
 |-  { n e. V | { P , n } e. X } = { p e. V | { P , p } e. 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 ` 0 ) , ( t ` 1 ) } = { ( w ` 0 ) , ( w ` 1 ) } )
22 21 eleq1d 
 |-  ( t = w -> ( { ( t ` 0 ) , ( t ` 1 ) } e. X <-> { ( w ` 0 ) , ( w ` 1 ) } e. X ) )
23 17 19 22 3anbi123d 
 |-  ( t = w -> ( ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) <-> ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) ) )
24 23 cbvrabv 
 |-  { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }
25 24 mpteq1i 
 |-  ( x e. { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } |-> ( x ` 1 ) ) = ( x e. { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } |-> ( x ` 1 ) )
26 13 16 25 wwlktovf1o 
 |-  ( P e. V -> ( x e. { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } |-> ( x ` 1 ) ) : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } -1-1-onto-> { n e. V | { P , n } e. X } )
27 26 adantl 
 |-  ( ( V e. Y /\ P e. V ) -> ( x e. { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } |-> ( x ` 1 ) ) : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } -1-1-onto-> { n e. V | { P , n } e. X } )
28 f1oeq1 
 |-  ( f = ( x e. { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } |-> ( x ` 1 ) ) -> ( f : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } -1-1-onto-> { n e. V | { P , n } e. X } <-> ( x e. { t e. Word V | ( ( # ` t ) = 2 /\ ( t ` 0 ) = P /\ { ( t ` 0 ) , ( t ` 1 ) } e. X ) } |-> ( x ` 1 ) ) : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } -1-1-onto-> { n e. V | { P , n } e. X } ) )
29 5 27 28 spcedv 
 |-  ( ( V e. Y /\ P e. V ) -> E. f f : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } -1-1-onto-> { n e. V | { P , n } e. X } )