Theorem wemapso 8456

Description: Construct lexicographic order on a function space based on a well-ordering of the indexes and a total ordering of the values. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.)

Hypothesis

Ref	Expression
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

Ref	Expression
wemapso	|- ( ( A e. V /\ R We A /\ S Or B ) -> T Or ( B ^m A ) )

Distinct variable groups:   x, B   x, w, y, z, A   w, R, x, y, z   w, S, x, y, z

Allowed substitution hints:   B( y, z, w)   T( x, y, z, w)   V( x, y, z, w)

Proof of Theorem wemapso

Dummy variables a b c d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3212	. 2 |- ( A e. V -> A e. _V )
2		wemapso.t	. . 3 |- T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }
3		ssid 3624	. . 3 |- ( B ^m A ) C_ ( B ^m A )
4		simp1 1061	. . 3 |- ( ( A e. _V /\ R We A /\ S Or B ) -> A e. _V )
5		weso 5105	. . . 4 |- ( R We A -> R Or A )
6	5	3ad2ant2 1083	. . 3 |- ( ( A e. _V /\ R We A /\ S Or B ) -> R Or A )
7		simp3 1063	. . 3 |- ( ( A e. _V /\ R We A /\ S Or B ) -> S Or B )
8		simpl1 1064	. . . . 5 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> A e. _V )
9		difss 3737	. . . . . . 7 |- ( a \ b ) C_ a
10		dmss 5323	. . . . . . 7 |- ( ( a \ b ) C_ a -> dom ( a \ b ) C_ dom a )
11	9, 10	ax-mp 5	. . . . . 6 |- dom ( a \ b ) C_ dom a
12		simprll 802	. . . . . . . . 9 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> a e. ( B ^m A ) )
13		elmapi 7879	. . . . . . . . 9 |- ( a e. ( B ^m A ) -> a : A --> B )
14	12, 13	syl 17	. . . . . . . 8 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> a : A --> B )
15		ffn 6045	. . . . . . . 8 |- ( a : A --> B -> a Fn A )
16	14, 15	syl 17	. . . . . . 7 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> a Fn A )
17		fndm 5990	. . . . . . 7 |- ( a Fn A -> dom a = A )
18	16, 17	syl 17	. . . . . 6 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> dom a = A )
19	11, 18	syl5sseq 3653	. . . . 5 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> dom ( a \ b ) C_ A )
20	8, 19	ssexd 4805	. . . 4 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> dom ( a \ b ) e. _V )
21		simpl2 1065	. . . . 5 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> R We A )
22		wefr 5104	. . . . 5 |- ( R We A -> R Fr A )
23	21, 22	syl 17	. . . 4 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> R Fr A )
24		simprr 796	. . . . 5 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> a =/= b )
25		simprlr 803	. . . . . . . . 9 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> b e. ( B ^m A ) )
26		elmapi 7879	. . . . . . . . 9 |- ( b e. ( B ^m A ) -> b : A --> B )
27	25, 26	syl 17	. . . . . . . 8 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> b : A --> B )
28		ffn 6045	. . . . . . . 8 |- ( b : A --> B -> b Fn A )
29	27, 28	syl 17	. . . . . . 7 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> b Fn A )
30		fndmdifeq0 6323	. . . . . . 7 |- ( ( a Fn A /\ b Fn A ) -> ( dom ( a \ b ) = (/) <-> a = b ) )
31	16, 29, 30	syl2anc 693	. . . . . 6 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> ( dom ( a \ b ) = (/) <-> a = b ) )
32	31	necon3bid 2838	. . . . 5 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> ( dom ( a \ b ) =/= (/) <-> a =/= b ) )
33	24, 32	mpbird 247	. . . 4 |- ( ( ( A e. _V /\ R We A /\ S Or B ) /\ ( ( a e. ( B ^m A ) /\ b e. ( B ^m A ) ) /\ a =/= b ) ) -> dom ( a \ b ) =/= (/) )
34		fri 5076	. . . 4 |- ( ( ( 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 )
35	20, 23, 19, 33, 34	syl22anc 1327	. . 3 |- ( ( ( A e. _V /\ 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 )
36	2, 3, 4, 6, 7, 35	wemapsolem 8455	. 2 |- ( ( A e. _V /\ R We A /\ S Or B ) -> T Or ( B ^m A ) )
37	1, 36	syl3an1 1359	1 |- ( ( A e. V /\ R We A /\ S Or B ) -> T Or ( B ^m A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   C_ wss 3574   (/)c0 3915   class class class wbr 4653   {copab 4712   Or wor 5034   Fr wfr 5070   We wwe 5072   dom cdm 5114   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-map 7859

This theorem is referenced by:  opsrtoslem2  19485  wepwso  37613