Metamath Proof Explorer

Theorem wemapso2lem

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

Ref Expression
Hypotheses 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 wemapso2lem 
|- ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> T Or U )

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 wemapso2.u 
 |-  U = { x e. ( B ^m A ) | x finSupp Z }
3 2 ssrab3 
 |-  U C_ ( B ^m A )
4 simpl2 
 |-  ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> R Or A )
5 simpl3 
 |-  ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> S Or B )
6 simprll 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a e. U )
7 breq1 
 |-  ( x = a -> ( x finSupp Z <-> a finSupp Z ) )
8 7 2 elrab2 
 |-  ( a e. U <-> ( a e. ( B ^m A ) /\ a finSupp Z ) )
9 8 simprbi 
 |-  ( a e. U -> a finSupp Z )
10 6 9 syl 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a finSupp Z )
11 simprlr 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b e. U )
12 breq1 
 |-  ( x = b -> ( x finSupp Z <-> b finSupp Z ) )
13 12 2 elrab2 
 |-  ( b e. U <-> ( b e. ( B ^m A ) /\ b finSupp Z ) )
14 13 simprbi 
 |-  ( b e. U -> b finSupp Z )
15 11 14 syl 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b finSupp Z )
16 10 15 fsuppunfi 
 |-  ( ( ( ( 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 )
17 3 6 sselid 
 |-  ( ( ( ( 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 ) )
18 elmapi 
 |-  ( a e. ( B ^m A ) -> a : A --> B )
19 17 18 syl 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a : A --> B )
20 19 ffnd 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a Fn A )
21 3 11 sselid 
 |-  ( ( ( ( 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 ) )
22 elmapi 
 |-  ( b e. ( B ^m A ) -> b : A --> B )
23 21 22 syl 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b : A --> B )
24 23 ffnd 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b Fn A )
25 fndmdif 
 |-  ( ( a Fn A /\ b Fn A ) -> dom ( a \ b ) = { c e. A | ( a ` c ) =/= ( b ` c ) } )
26 20 24 25 syl2anc 
 |-  ( ( ( ( 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 ) } )
27 neneor 
 |-  ( ( a ` c ) =/= ( b ` c ) -> ( ( a ` c ) =/= Z \/ ( b ` c ) =/= Z ) )
28 elun 
 |-  ( c e. ( ( a supp Z ) u. ( b supp Z ) ) <-> ( c e. ( a supp Z ) \/ c e. ( b supp Z ) ) )
29 simpr 
 |-  ( ( ( ( ( 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 )
30 20 adantr 
 |-  ( ( ( ( ( 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 )
31 elex 
 |-  ( A e. V -> A e. _V )
32 31 3ad2ant1 
 |-  ( ( A e. V /\ R Or A /\ S Or B ) -> A e. _V )
33 32 adantr 
 |-  ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> A e. _V )
34 33 ad2antrr 
 |-  ( ( ( ( ( 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 )
35 simpr 
 |-  ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> Z e. W )
36 35 ad2antrr 
 |-  ( ( ( ( ( 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 )
37 elsuppfn 
 |-  ( ( a Fn A /\ A e. _V /\ Z e. W ) -> ( c e. ( a supp Z ) <-> ( c e. A /\ ( a ` c ) =/= Z ) ) )
38 30 34 36 37 syl3anc 
 |-  ( ( ( ( ( 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 ) ) )
39 29 38 mpbirand 
 |-  ( ( ( ( ( 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 ) )
40 24 adantr 
 |-  ( ( ( ( ( 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 )
41 simpll1 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> A e. V )
42 41 adantr 
 |-  ( ( ( ( ( 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 )
43 elsuppfn 
 |-  ( ( b Fn A /\ A e. V /\ Z e. W ) -> ( c e. ( b supp Z ) <-> ( c e. A /\ ( b ` c ) =/= Z ) ) )
44 40 42 36 43 syl3anc 
 |-  ( ( ( ( ( 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 ) ) )
45 29 44 mpbirand 
 |-  ( ( ( ( ( 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 ) )
46 39 45 orbi12d 
 |-  ( ( ( ( ( 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 ) ) )
47 28 46 bitrid 
 |-  ( ( ( ( ( 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 ) ) )
48 27 47 syl5ibr 
 |-  ( ( ( ( ( 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 ) ) ) )
49 48 ralrimiva 
 |-  ( ( ( ( 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 ) ) ) )
50 rabss 
 |-  ( { 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 ) ) ) )
51 49 50 sylibr 
 |-  ( ( ( ( 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 ) ) )
52 26 51 eqsstrd 
 |-  ( ( ( ( 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 ) ) )
53 16 52 ssfid 
 |-  ( ( ( ( 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 )
54 suppssdm 
 |-  ( a supp Z ) C_ dom a
55 54 19 fssdm 
 |-  ( ( ( ( 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 )
56 suppssdm 
 |-  ( b supp Z ) C_ dom b
57 56 23 fssdm 
 |-  ( ( ( ( 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 )
58 55 57 unssd 
 |-  ( ( ( ( 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 )
59 4 adantr 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> R Or A )
60 soss 
 |-  ( ( ( a supp Z ) u. ( b supp Z ) ) C_ A -> ( R Or A -> R Or ( ( a supp Z ) u. ( b supp Z ) ) ) )
61 58 59 60 sylc 
 |-  ( ( ( ( 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 ) ) )
62 wofi 
 |-  ( ( 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 ) ) )
63 61 16 62 syl2anc 
 |-  ( ( ( ( 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 ) ) )
64 wefr 
 |-  ( R We ( ( a supp Z ) u. ( b supp Z ) ) -> R Fr ( ( a supp Z ) u. ( b supp Z ) ) )
65 63 64 syl 
 |-  ( ( ( ( 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 ) ) )
66 simprr 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a =/= b )
67 fndmdifeq0 
 |-  ( ( a Fn A /\ b Fn A ) -> ( dom ( a \ b ) = (/) <-> a = b ) )
68 20 24 67 syl2anc 
 |-  ( ( ( ( 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 ) )
69 68 necon3bid 
 |-  ( ( ( ( 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 ) )
70 66 69 mpbird 
 |-  ( ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> dom ( a \ b ) =/= (/) )
71 fri 
 |-  ( ( ( 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 )
72 53 65 52 70 71 syl22anc 
 |-  ( ( ( ( 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 )
73 1 3 4 5 72 wemapsolem 
 |-  ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. W ) -> T Or U )