Theorem wemapso2lem 8457

Description: Lemma for wemapso2 8458. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.)

Hypotheses

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 ) ) ) }
wemapso2.u	|- U = { x e. ( B ^m A ) | x finSupp Z }

Assertion

Ref	Expression
wemapso2lem	|- ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> T Or U )

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

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

Proof of Theorem wemapso2lem

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

Step	Hyp	Ref	Expression
1		wemapso.t	. 2 |- T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }
2		wemapso2.u	. . 3 |- U = { x e. ( B ^m A ) | x finSupp Z }
3		ssrab2 3687	. . 3 |- { x e. ( B ^m A ) | x finSupp Z } C_ ( B ^m A )
4	2, 3	eqsstri 3635	. 2 |- U C_ ( B ^m A )
5		elex 3212	. . . 4 |- ( A e. V -> A e. _V )
6	5	3ad2ant1 1082	. . 3 |- ( ( A e. V /\ R Or A /\ S Or B ) -> A e. _V )
7	6	adantr 481	. 2 |- ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> A e. _V )
8		simpl2 1065	. 2 |- ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> R Or A )
9		simpl3 1066	. 2 |- ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> S Or B )
10		simprll 802	. . . . . 6 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a e. U )
11		breq1 4656	. . . . . . . 8 |- ( x = a -> ( x finSupp Z <-> a finSupp Z ) )
12	11, 2	elrab2 3366	. . . . . . 7 |- ( a e. U <-> ( a e. ( B ^m A ) /\ a finSupp Z ) )
13	12	simprbi 480	. . . . . 6 |- ( a e. U -> a finSupp Z )
14	10, 13	syl 17	. . . . 5 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a finSupp Z )
15		simprlr 803	. . . . . 6 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b e. U )
16		breq1 4656	. . . . . . . 8 |- ( x = b -> ( x finSupp Z <-> b finSupp Z ) )
17	16, 2	elrab2 3366	. . . . . . 7 |- ( b e. U <-> ( b e. ( B ^m A ) /\ b finSupp Z ) )
18	17	simprbi 480	. . . . . 6 |- ( b e. U -> b finSupp Z )
19	15, 18	syl 17	. . . . 5 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b finSupp Z )
20	14, 19	fsuppunfi 8295	. . . 4 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( ( a supp Z ) u. ( b supp Z ) ) e. Fin )
21	4, 10	sseldi 3601	. . . . . . . 8 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a e. ( B ^m A ) )
22		elmapi 7879	. . . . . . . 8 |- ( a e. ( B ^m A ) -> a : A --> B )
23	21, 22	syl 17	. . . . . . 7 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a : A --> B )
24		ffn 6045	. . . . . . 7 |- ( a : A --> B -> a Fn A )
25	23, 24	syl 17	. . . . . 6 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a Fn A )
26	4, 15	sseldi 3601	. . . . . . . 8 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b e. ( B ^m A ) )
27		elmapi 7879	. . . . . . . 8 |- ( b e. ( B ^m A ) -> b : A --> B )
28	26, 27	syl 17	. . . . . . 7 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b : A --> B )
29		ffn 6045	. . . . . . 7 |- ( b : A --> B -> b Fn A )
30	28, 29	syl 17	. . . . . 6 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b Fn A )
31		fndmdif 6321	. . . . . 6 |- ( ( a Fn A /\ b Fn A ) -> dom ( a \ b ) = { c e. A | ( a ` c ) =/= ( b ` c ) } )
32	25, 30, 31	syl2anc 693	. . . . 5 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> dom ( a \ b ) = { c e. A | ( a ` c ) =/= ( b ` c ) } )
33		eqtr3 2643	. . . . . . . . . 10 |- ( ( ( a ` c ) = Z /\ ( b ` c ) = Z ) -> ( a ` c ) = ( b ` c ) )
34	33	necon3ai 2819	. . . . . . . . 9 |- ( ( a ` c ) =/= ( b ` c ) -> -. ( ( a ` c ) = Z /\ ( b ` c ) = Z ) )
35		neorian 2888	. . . . . . . . 9 |- ( ( ( a ` c ) =/= Z \/ ( b ` c ) =/= Z ) <-> -. ( ( a ` c ) = Z /\ ( b ` c ) = Z ) )
36	34, 35	sylibr 224	. . . . . . . 8 |- ( ( a ` c ) =/= ( b ` c ) -> ( ( a ` c ) =/= Z \/ ( b ` c ) =/= Z ) )
37		elun 3753	. . . . . . . . 9 |- ( c e. ( ( a supp Z ) u. ( b supp Z ) ) <-> ( c e. ( a supp Z ) \/ c e. ( b supp Z ) ) )
38		fvex 6201	. . . . . . . . . . . . . . . 16 |- ( a ` c ) e. _V
39		eldifsn 4317	. . . . . . . . . . . . . . . 16 |- ( ( a ` c ) e. ( _V \ { Z } ) <-> ( ( a ` c ) e. _V /\ ( a ` c ) =/= Z ) )
40	38, 39	mpbiran 953	. . . . . . . . . . . . . . 15 |- ( ( a ` c ) e. ( _V \ { Z } ) <-> ( a ` c ) =/= Z )
41	40	bicomi 214	. . . . . . . . . . . . . 14 |- ( ( a ` c ) =/= Z <-> ( a ` c ) e. ( _V \ { Z } ) )
42	41	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( ( a ` c ) =/= Z <-> ( a ` c ) e. ( _V \ { Z } ) ) )
43	42	anbi2d 740	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( ( c e. A /\ ( a ` c ) =/= Z ) <-> ( c e. A /\ ( a ` c ) e. ( _V \ { Z } ) ) ) )
44	25	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> a Fn A )
45	7	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> A e. _V )
46		simpr 477	. . . . . . . . . . . . . 14 |- ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> Z e. W )
47	46	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> Z e. W )
48		elsuppfn 7303	. . . . . . . . . . . . 13 |- ( ( a Fn A /\ A e. _V /\ Z e. W ) -> ( c e. ( a supp Z ) <-> ( c e. A /\ ( a ` c ) =/= Z ) ) )
49	44, 45, 47, 48	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( c e. ( a supp Z ) <-> ( c e. A /\ ( a ` c ) =/= Z ) ) )
50		simpr 477	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> c e. A )
51	50	biantrurd 529	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( ( a ` c ) e. ( _V \ { Z } ) <-> ( c e. A /\ ( a ` c ) e. ( _V \ { Z } ) ) ) )
52	43, 49, 51	3bitr4d 300	. . . . . . . . . . 11 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( c e. ( a supp Z ) <-> ( a ` c ) e. ( _V \ { Z } ) ) )
53	52, 40	syl6bb 276	. . . . . . . . . 10 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( c e. ( a supp Z ) <-> ( a ` c ) =/= Z ) )
54		fvex 6201	. . . . . . . . . . . . . . . 16 |- ( b ` c ) e. _V
55		eldifsn 4317	. . . . . . . . . . . . . . . 16 |- ( ( b ` c ) e. ( _V \ { Z } ) <-> ( ( b ` c ) e. _V /\ ( b ` c ) =/= Z ) )
56	54, 55	mpbiran 953	. . . . . . . . . . . . . . 15 |- ( ( b ` c ) e. ( _V \ { Z } ) <-> ( b ` c ) =/= Z )
57	56	bicomi 214	. . . . . . . . . . . . . 14 |- ( ( b ` c ) =/= Z <-> ( b ` c ) e. ( _V \ { Z } ) )
58	57	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( ( b ` c ) =/= Z <-> ( b ` c ) e. ( _V \ { Z } ) ) )
59	58	anbi2d 740	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( ( c e. A /\ ( b ` c ) =/= Z ) <-> ( c e. A /\ ( b ` c ) e. ( _V \ { Z } ) ) ) )
60	30	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> b Fn A )
61		simpll1 1100	. . . . . . . . . . . . . 14 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> A e. V )
62	61	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> A e. V )
63		elsuppfn 7303	. . . . . . . . . . . . 13 |- ( ( b Fn A /\ A e. V /\ Z e. W ) -> ( c e. ( b supp Z ) <-> ( c e. A /\ ( b ` c ) =/= Z ) ) )
64	60, 62, 47, 63	syl3anc 1326	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( c e. ( b supp Z ) <-> ( c e. A /\ ( b ` c ) =/= Z ) ) )
65	50	biantrurd 529	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( ( b ` c ) e. ( _V \ { Z } ) <-> ( c e. A /\ ( b ` c ) e. ( _V \ { Z } ) ) ) )
66	59, 64, 65	3bitr4d 300	. . . . . . . . . . 11 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( c e. ( b supp Z ) <-> ( b ` c ) e. ( _V \ { Z } ) ) )
67	66, 56	syl6bb 276	. . . . . . . . . 10 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( c e. ( b supp Z ) <-> ( b ` c ) =/= Z ) )
68	53, 67	orbi12d 746	. . . . . . . . 9 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( ( c e. ( a supp Z ) \/ c e. ( b supp Z ) ) <-> ( ( a ` c ) =/= Z \/ ( b ` c ) =/= Z ) ) )
69	37, 68	syl5bb 272	. . . . . . . 8 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( c e. ( ( a supp Z ) u. ( b supp Z ) ) <-> ( ( a ` c ) =/= Z \/ ( b ` c ) =/= Z ) ) )
70	36, 69	syl5ibr 236	. . . . . . 7 |- ( ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( ( a ` c ) =/= ( b ` c ) -> c e. ( ( a supp Z ) u. ( b supp Z ) ) ) )
71	70	ralrimiva 2966	. . . . . 6 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> A. c e. A ( ( a ` c ) =/= ( b ` c ) -> c e. ( ( a supp Z ) u. ( b supp Z ) ) ) )
72		rabss 3679	. . . . . 6 |- ( { c e. A | ( a ` c ) =/= ( b ` c ) } C_ ( ( a supp Z ) u. ( b supp Z ) ) <-> A. c e. A ( ( a ` c ) =/= ( b ` c ) -> c e. ( ( a supp Z ) u. ( b supp Z ) ) ) )
73	71, 72	sylibr 224	. . . . 5 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> { c e. A | ( a ` c ) =/= ( b ` c ) } C_ ( ( a supp Z ) u. ( b supp Z ) ) )
74	32, 73	eqsstrd 3639	. . . 4 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> dom ( a \ b ) C_ ( ( a supp Z ) u. ( b supp Z ) ) )
75		ssfi 8180	. . . 4 |- ( ( ( ( a supp Z ) u. ( b supp Z ) ) e. Fin /\ dom ( a \ b ) C_ ( ( a supp Z ) u. ( b supp Z ) ) ) -> dom ( a \ b ) e. Fin )
76	20, 74, 75	syl2anc 693	. . 3 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> dom ( a \ b ) e. Fin )
77		suppssdm 7308	. . . . . . . 8 |- ( a supp Z ) C_ dom a
78		fdm 6051	. . . . . . . . 9 |- ( a : A --> B -> dom a = A )
79	23, 78	syl 17	. . . . . . . 8 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> dom a = A )
80	77, 79	syl5sseq 3653	. . . . . . 7 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( a supp Z ) C_ A )
81		suppssdm 7308	. . . . . . . 8 |- ( b supp Z ) C_ dom b
82		fdm 6051	. . . . . . . . 9 |- ( b : A --> B -> dom b = A )
83	28, 82	syl 17	. . . . . . . 8 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> dom b = A )
84	81, 83	syl5sseq 3653	. . . . . . 7 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( b supp Z ) C_ A )
85	80, 84	unssd 3789	. . . . . 6 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( ( a supp Z ) u. ( b supp Z ) ) C_ A )
86	8	adantr 481	. . . . . 6 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> R Or A )
87		soss 5053	. . . . . 6 |- ( ( ( a supp Z ) u. ( b supp Z ) ) C_ A -> ( R Or A -> R Or ( ( a supp Z ) u. ( b supp Z ) ) ) )
88	85, 86, 87	sylc 65	. . . . 5 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> R Or ( ( a supp Z ) u. ( b supp Z ) ) )
89		wofi 8209	. . . . 5 |- ( ( R Or ( ( a supp Z ) u. ( b supp Z ) ) /\ ( ( a supp Z ) u. ( b supp Z ) ) e. Fin ) -> R We ( ( a supp Z ) u. ( b supp Z ) ) )
90	88, 20, 89	syl2anc 693	. . . 4 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> R We ( ( a supp Z ) u. ( b supp Z ) ) )
91		wefr 5104	. . . 4 |- ( R We ( ( a supp Z ) u. ( b supp Z ) ) -> R Fr ( ( a supp Z ) u. ( b supp Z ) ) )
92	90, 91	syl 17	. . 3 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> R Fr ( ( a supp Z ) u. ( b supp Z ) ) )
93		simprr 796	. . . 4 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a =/= b )
94		fndmdifeq0 6323	. . . . . 6 |- ( ( a Fn A /\ b Fn A ) -> ( dom ( a \ b ) = (/) <-> a = b ) )
95	25, 30, 94	syl2anc 693	. . . . 5 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( dom ( a \ b ) = (/) <-> a = b ) )
96	95	necon3bid 2838	. . . 4 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( dom ( a \ b ) =/= (/) <-> a =/= b ) )
97	93, 96	mpbird 247	. . 3 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> dom ( a \ b ) =/= (/) )
98		fri 5076	. . 3 |- ( ( ( dom ( a \ b ) e. Fin /\ R Fr ( ( a supp Z ) u. ( b supp Z ) ) ) /\ ( dom ( a \ b ) C_ ( ( a supp Z ) u. ( b supp Z ) ) /\ dom ( a \ b ) =/= (/) ) ) -> E. c e. dom ( a \ b ) A. d e. dom ( a \ b ) -. d R c )
99	76, 92, 74, 97, 98	syl22anc 1327	. 2 |- ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> E. c e. dom ( a \ b ) A. d e. dom ( a \ b ) -. d R c )
100	1, 4, 7, 8, 9, 99	wemapsolem 8455	1 |- ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> T Or U )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   C_ wss 3574   (/)c0 3915   {csn 4177   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   supp csupp 7295   ^m cmap 7857   Fincfn 7955   finSupp cfsupp 8275

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-rep 4771  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-reu 2919  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-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  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-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-fin 7959  df-fsupp 8276

This theorem is referenced by:  wemapso2  8458