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 = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }
Assertion wemaplem1 
|- ( ( P e. V /\ Q e. W ) -> ( P T Q <-> E. a e. A ( ( P ` a ) S ( Q ` a ) /\ A. b e. A ( b R a -> ( P ` b ) = ( Q ` b ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wemapso.t 
 |-  T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }
2 fveq1 
 |-  ( x = P -> ( x ` z ) = ( P ` z ) )
3 fveq1 
 |-  ( y = Q -> ( y ` z ) = ( Q ` z ) )
4 2 3 breqan12d 
 |-  ( ( x = P /\ y = Q ) -> ( ( x ` z ) S ( y ` z ) <-> ( P ` z ) S ( Q ` z ) ) )
5 fveq1 
 |-  ( x = P -> ( x ` w ) = ( P ` w ) )
6 fveq1 
 |-  ( y = Q -> ( y ` w ) = ( Q ` w ) )
7 5 6 eqeqan12d 
 |-  ( ( x = P /\ y = Q ) -> ( ( x ` w ) = ( y ` w ) <-> ( P ` w ) = ( Q ` w ) ) )
8 7 imbi2d 
 |-  ( ( x = P /\ y = Q ) -> ( ( w R z -> ( x ` w ) = ( y ` w ) ) <-> ( w R z -> ( P ` w ) = ( Q ` w ) ) ) )
9 8 ralbidv 
 |-  ( ( x = P /\ y = Q ) -> ( A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) <-> A. w e. A ( w R z -> ( P ` w ) = ( Q ` w ) ) ) )
10 4 9 anbi12d 
 |-  ( ( x = P /\ y = Q ) -> ( ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( P ` z ) S ( Q ` z ) /\ A. w e. A ( w R z -> ( P ` w ) = ( Q ` w ) ) ) ) )
11 10 rexbidv 
 |-  ( ( x = P /\ y = Q ) -> ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. A ( ( P ` z ) S ( Q ` z ) /\ A. w e. A ( w R z -> ( P ` w ) = ( Q ` w ) ) ) ) )
12 fveq2 
 |-  ( z = a -> ( P ` z ) = ( P ` a ) )
13 fveq2 
 |-  ( z = a -> ( Q ` z ) = ( Q ` a ) )
14 12 13 breq12d 
 |-  ( z = a -> ( ( P ` z ) S ( Q ` z ) <-> ( P ` a ) S ( Q ` a ) ) )
15 breq2 
 |-  ( z = a -> ( w R z <-> w R a ) )
16 15 imbi1d 
 |-  ( z = a -> ( ( w R z -> ( P ` w ) = ( Q ` w ) ) <-> ( w R a -> ( P ` w ) = ( Q ` w ) ) ) )
17 16 ralbidv 
 |-  ( z = a -> ( A. w e. A ( w R z -> ( P ` w ) = ( Q ` w ) ) <-> A. w e. A ( w R a -> ( P ` w ) = ( Q ` w ) ) ) )
18 breq1 
 |-  ( w = b -> ( w R a <-> b R a ) )
19 fveq2 
 |-  ( w = b -> ( P ` w ) = ( P ` b ) )
20 fveq2 
 |-  ( w = b -> ( Q ` w ) = ( Q ` b ) )
21 19 20 eqeq12d 
 |-  ( w = b -> ( ( P ` w ) = ( Q ` w ) <-> ( P ` b ) = ( Q ` b ) ) )
22 18 21 imbi12d 
 |-  ( w = b -> ( ( w R a -> ( P ` w ) = ( Q ` w ) ) <-> ( b R a -> ( P ` b ) = ( Q ` b ) ) ) )
23 22 cbvralvw 
 |-  ( A. w e. A ( w R a -> ( P ` w ) = ( Q ` w ) ) <-> A. b e. A ( b R a -> ( P ` b ) = ( Q ` b ) ) )
24 17 23 bitrdi 
 |-  ( z = a -> ( A. w e. A ( w R z -> ( P ` w ) = ( Q ` w ) ) <-> A. b e. A ( b R a -> ( P ` b ) = ( Q ` b ) ) ) )
25 14 24 anbi12d 
 |-  ( z = a -> ( ( ( P ` z ) S ( Q ` z ) /\ A. w e. A ( w R z -> ( P ` w ) = ( Q ` w ) ) ) <-> ( ( P ` a ) S ( Q ` a ) /\ A. b e. A ( b R a -> ( P ` b ) = ( Q ` b ) ) ) ) )
26 25 cbvrexvw 
 |-  ( E. z e. A ( ( P ` z ) S ( Q ` z ) /\ A. w e. A ( w R z -> ( P ` w ) = ( Q ` w ) ) ) <-> E. a e. A ( ( P ` a ) S ( Q ` a ) /\ A. b e. A ( b R a -> ( P ` b ) = ( Q ` b ) ) ) )
27 11 26 bitrdi 
 |-  ( ( x = P /\ y = Q ) -> ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) <-> E. a e. A ( ( P ` a ) S ( Q ` a ) /\ A. b e. A ( b R a -> ( P ` b ) = ( Q ` b ) ) ) ) )
28 27 1 brabga 
 |-  ( ( P e. V /\ Q e. W ) -> ( P T Q <-> E. a e. A ( ( P ` a ) S ( Q ` a ) /\ A. b e. A ( b R a -> ( P ` b ) = ( Q ` b ) ) ) ) )