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 >. | 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	wemapso2	|- ( ( A e. V /\ R Or A /\ S Or B ) -> 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	1 2	wemapso2lem	|- ( ( ( A e. V /\ R Or A /\ S Or B ) /\ Z e. _V ) -> T Or U )
4	3	expcom	|- ( Z e. _V -> ( ( A e. V /\ R Or A /\ S Or B ) -> T Or U ) )
5		so0	|- T Or (/)
6		relfsupp	|- Rel finSupp
7	6	brrelex2i	|- ( x finSupp Z -> Z e. _V )
8	7	con3i	|- ( -. Z e. _V -> -. x finSupp Z )
9	8	ralrimivw	|- ( -. Z e. _V -> A. x e. ( B ^m A ) -. x finSupp Z )
10		rabeq0	|- ( { x e. ( B ^m A ) | x finSupp Z } = (/) <-> A. x e. ( B ^m A ) -. x finSupp Z )
11	9 10	sylibr	|- ( -. Z e. _V -> { x e. ( B ^m A ) | x finSupp Z } = (/) )
12	2 11	eqtrid	|- ( -. Z e. _V -> U = (/) )
13		soeq2	|- ( U = (/) -> ( T Or U <-> T Or (/) ) )
14	12 13	syl	|- ( -. Z e. _V -> ( T Or U <-> T Or (/) ) )
15	5 14	mpbiri	|- ( -. Z e. _V -> T Or U )
16	15	a1d	|- ( -. Z e. _V -> ( ( A e. V /\ R Or A /\ S Or B ) -> T Or U ) )
17	4 16	pm2.61i	|- ( ( A e. V /\ R Or A /\ S Or B ) -> T Or U )