Description: Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values.
Without totality on the values or least differing indices, the best we can prove here is a partial order. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by AV, 21-Jul-2024)
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 | wemappo | |- ( ( R Or A /\ S Po B ) -> T Po ( B ^m A ) ) |
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 | simpllr | |- ( ( ( ( R Or A /\ S Po B ) /\ a e. ( B ^m A ) ) /\ b e. A ) -> S Po B ) |
|
3 | elmapi | |- ( a e. ( B ^m A ) -> a : A --> B ) |
|
4 | 3 | adantl | |- ( ( ( R Or A /\ S Po B ) /\ a e. ( B ^m A ) ) -> a : A --> B ) |
5 | 4 | ffvelrnda | |- ( ( ( ( R Or A /\ S Po B ) /\ a e. ( B ^m A ) ) /\ b e. A ) -> ( a ` b ) e. B ) |
6 | poirr | |- ( ( S Po B /\ ( a ` b ) e. B ) -> -. ( a ` b ) S ( a ` b ) ) |
|
7 | 2 5 6 | syl2anc | |- ( ( ( ( R Or A /\ S Po B ) /\ a e. ( B ^m A ) ) /\ b e. A ) -> -. ( a ` b ) S ( a ` b ) ) |
8 | 7 | intnanrd | |- ( ( ( ( R Or A /\ S Po B ) /\ a e. ( B ^m A ) ) /\ b e. A ) -> -. ( ( a ` b ) S ( a ` b ) /\ A. c e. A ( c R b -> ( a ` c ) = ( a ` c ) ) ) ) |
9 | 8 | nrexdv | |- ( ( ( R Or A /\ S Po B ) /\ a e. ( B ^m A ) ) -> -. E. b e. A ( ( a ` b ) S ( a ` b ) /\ A. c e. A ( c R b -> ( a ` c ) = ( a ` c ) ) ) ) |
10 | 1 | wemaplem1 | |- ( ( a e. _V /\ a e. _V ) -> ( a T a <-> E. b e. A ( ( a ` b ) S ( a ` b ) /\ A. c e. A ( c R b -> ( a ` c ) = ( a ` c ) ) ) ) ) |
11 | 10 | el2v | |- ( a T a <-> E. b e. A ( ( a ` b ) S ( a ` b ) /\ A. c e. A ( c R b -> ( a ` c ) = ( a ` c ) ) ) ) |
12 | 9 11 | sylnibr | |- ( ( ( R Or A /\ S Po B ) /\ a e. ( B ^m A ) ) -> -. a T a ) |
13 | simplr1 | |- ( ( ( ( R Or A /\ S Po B ) /\ ( a e. ( B ^m A ) /\ b e. ( B ^m A ) /\ c e. ( B ^m A ) ) ) /\ ( a T b /\ b T c ) ) -> a e. ( B ^m A ) ) |
|
14 | simplr2 | |- ( ( ( ( R Or A /\ S Po B ) /\ ( a e. ( B ^m A ) /\ b e. ( B ^m A ) /\ c e. ( B ^m A ) ) ) /\ ( a T b /\ b T c ) ) -> b e. ( B ^m A ) ) |
|
15 | simplr3 | |- ( ( ( ( R Or A /\ S Po B ) /\ ( a e. ( B ^m A ) /\ b e. ( B ^m A ) /\ c e. ( B ^m A ) ) ) /\ ( a T b /\ b T c ) ) -> c e. ( B ^m A ) ) |
|
16 | simplll | |- ( ( ( ( R Or A /\ S Po B ) /\ ( a e. ( B ^m A ) /\ b e. ( B ^m A ) /\ c e. ( B ^m A ) ) ) /\ ( a T b /\ b T c ) ) -> R Or A ) |
|
17 | simpllr | |- ( ( ( ( R Or A /\ S Po B ) /\ ( a e. ( B ^m A ) /\ b e. ( B ^m A ) /\ c e. ( B ^m A ) ) ) /\ ( a T b /\ b T c ) ) -> S Po B ) |
|
18 | simprl | |- ( ( ( ( R Or A /\ S Po B ) /\ ( a e. ( B ^m A ) /\ b e. ( B ^m A ) /\ c e. ( B ^m A ) ) ) /\ ( a T b /\ b T c ) ) -> a T b ) |
|
19 | simprr | |- ( ( ( ( R Or A /\ S Po B ) /\ ( a e. ( B ^m A ) /\ b e. ( B ^m A ) /\ c e. ( B ^m A ) ) ) /\ ( a T b /\ b T c ) ) -> b T c ) |
|
20 | 1 13 14 15 16 17 18 19 | wemaplem3 | |- ( ( ( ( R Or A /\ S Po B ) /\ ( a e. ( B ^m A ) /\ b e. ( B ^m A ) /\ c e. ( B ^m A ) ) ) /\ ( a T b /\ b T c ) ) -> a T c ) |
21 | 20 | ex | |- ( ( ( R Or A /\ S Po B ) /\ ( a e. ( B ^m A ) /\ b e. ( B ^m A ) /\ c e. ( B ^m A ) ) ) -> ( ( a T b /\ b T c ) -> a T c ) ) |
22 | 12 21 | ispod | |- ( ( R Or A /\ S Po B ) -> T Po ( B ^m A ) ) |