Metamath Proof Explorer


Theorem wemaplem1

Description: Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypothesis wemapso.t T=xy|zAxzSyzwAwRzxw=yw
Assertion wemaplem1 PVQWPTQaAPaSQabAbRaPb=Qb

Proof

Step Hyp Ref Expression
1 wemapso.t T=xy|zAxzSyzwAwRzxw=yw
2 fveq1 x=Pxz=Pz
3 fveq1 y=Qyz=Qz
4 2 3 breqan12d x=Py=QxzSyzPzSQz
5 fveq1 x=Pxw=Pw
6 fveq1 y=Qyw=Qw
7 5 6 eqeqan12d x=Py=Qxw=ywPw=Qw
8 7 imbi2d x=Py=QwRzxw=ywwRzPw=Qw
9 8 ralbidv x=Py=QwAwRzxw=ywwAwRzPw=Qw
10 4 9 anbi12d x=Py=QxzSyzwAwRzxw=ywPzSQzwAwRzPw=Qw
11 10 rexbidv x=Py=QzAxzSyzwAwRzxw=ywzAPzSQzwAwRzPw=Qw
12 fveq2 z=aPz=Pa
13 fveq2 z=aQz=Qa
14 12 13 breq12d z=aPzSQzPaSQa
15 breq2 z=awRzwRa
16 15 imbi1d z=awRzPw=QwwRaPw=Qw
17 16 ralbidv z=awAwRzPw=QwwAwRaPw=Qw
18 breq1 w=bwRabRa
19 fveq2 w=bPw=Pb
20 fveq2 w=bQw=Qb
21 19 20 eqeq12d w=bPw=QwPb=Qb
22 18 21 imbi12d w=bwRaPw=QwbRaPb=Qb
23 22 cbvralvw wAwRaPw=QwbAbRaPb=Qb
24 17 23 bitrdi z=awAwRzPw=QwbAbRaPb=Qb
25 14 24 anbi12d z=aPzSQzwAwRzPw=QwPaSQabAbRaPb=Qb
26 25 cbvrexvw zAPzSQzwAwRzPw=QwaAPaSQabAbRaPb=Qb
27 11 26 bitrdi x=Py=QzAxzSyzwAwRzxw=ywaAPaSQabAbRaPb=Qb
28 27 1 brabga PVQWPTQaAPaSQabAbRaPb=Qb