This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 >. | 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 )