Metamath Proof Explorer


Theorem wemapso2

Description: An alternative to having a well-order on R in wemapso is to restrict the function set to finitely-supported functions. (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 wemapso2 A V R Or A S Or B 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 1 2 wemapso2lem A V R Or A S Or B Z V T Or U
4 3 expcom Z V A V R Or A S Or B T Or U
5 so0 T Or
6 relfsupp Rel finSupp
7 6 brrelex2i finSupp Z x Z V
8 7 con3i ¬ Z V ¬ finSupp Z x
9 8 ralrimivw ¬ Z V x B A ¬ finSupp Z x
10 rabeq0 x B A | finSupp Z x = x B A ¬ finSupp Z x
11 9 10 sylibr ¬ Z V x B A | finSupp Z x =
12 2 11 eqtrid ¬ Z V U =
13 soeq2 U = T Or U T Or
14 12 13 syl ¬ Z V T Or U T Or
15 5 14 mpbiri ¬ Z V T Or U
16 15 a1d ¬ Z V A V R Or A S Or B T Or U
17 4 16 pm2.61i A V R Or A S Or B T Or U