Metamath Proof Explorer

Theorem wemappo

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 ) )

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 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 ffvelcdmda 
 |-  ( ( ( ( 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 ) )