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 | z A x z S y z w A w R z x w = y w
wemapso2.u U = x B A | finSupp Z x
Assertion wemapso2lem A V R Or A S Or B Z W T Or U

Proof

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