Metamath Proof Explorer

Theorem wemapso

Description: Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Mario Carneiro, 8-Feb-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 wemapso 
|- ( ( R We A /\ S Or B ) -> T Or ( 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 ssid 
 |-  ( B ^m A ) C_ ( B ^m A )
3 weso 
 |-  ( R We A -> R Or A )
4 3 adantr 
 |-  ( ( R We A /\ S Or B ) -> R Or A )
5 simpr 
 |-  ( ( R We A /\ S Or B ) -> S Or B )
6 vex 
 |-  a e. _V
7 6 difexi 
 |-  ( a \ b ) e. _V
8 7 dmex 
 |-  dom ( a \ b ) e. _V
9 8 a1i 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> dom ( a \ b ) e. _V )
10 wefr 
 |-  ( R We A -> R Fr A )
11 10 ad2antrr 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> R Fr A )
12 difss 
 |-  ( a \ b ) C_ a
13 dmss 
 |-  ( ( a \ b ) C_ a -> dom ( a \ b ) C_ dom a )
14 12 13 ax-mp 
 |-  dom ( a \ b ) C_ dom a
15 simprll 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> a e. ( B ^m A ) )
16 elmapi 
 |-  ( a e. ( B ^m A ) -> a : A --> B )
17 15 16 syl 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> a : A --> B )
18 14 17 fssdm 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> dom ( a \ b ) C_ A )
19 simprr 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> a =/= b )
20 17 ffnd 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> a Fn A )
21 simprlr 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> b e. ( B ^m A ) )
22 elmapi 
 |-  ( b e. ( B ^m A ) -> b : A --> B )
23 21 22 syl 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> b : A --> B )
24 23 ffnd 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> b Fn A )
25 fndmdifeq0 
 |-  ( ( a Fn A /\ b Fn A ) -> ( dom ( a \ b ) = (/) <-> a = b ) )
26 20 24 25 syl2anc 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> ( dom ( a \ b ) = (/) <-> a = b ) )
27 26 necon3bid 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> ( dom ( a \ b ) =/= (/) <-> a =/= b ) )
28 19 27 mpbird 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> dom ( a \ b ) =/= (/) )
29 fri 
 |-  ( ( ( dom ( a \ b ) e. _V /\ R Fr A ) /\ ( dom ( a \ b ) C_ A /\ dom ( a \ b ) =/= (/) ) ) -> E. c e. dom ( a \ b ) A. d e. dom ( a \ b ) -. d R c )
30 9 11 18 28 29 syl22anc 
 |-  ( ( ( R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> E. c e. dom ( a \ b ) A. d e. dom ( a \ b ) -. d R c )
31 1 2 4 5 30 wemapsolem 
 |-  ( ( R We A /\ S Or B ) -> T Or ( B ^m A ) )