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⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}$
		wemapso2.u	$⊢ U = \{x \in (B^{A}) \| {finSupp}_{Z} (x)\}$
	Assertion	wemapso2	$⊢ (A \in V \land R Or A \land S Or B) \to T Or U$

Proof

Step	Hyp	Ref	Expression
1		wemapso.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}$
2		wemapso2.u	$⊢ U = \{x \in (B^{A}) \| {finSupp}_{Z} (x)\}$
3	1 2	wemapso2lem	$⊢ ((A \in V \land R Or A \land S Or B) \land Z \in V) \to T Or U$
4	3	expcom	$⊢ Z \in V \to ((A \in V \land R Or A \land S Or B) \to T Or U)$
5		so0	$⊢ T Or \emptyset$
6		relfsupp	$⊢ Rel finSupp$
7	6	brrelex2i	$⊢ {finSupp}_{Z} (x) \to Z \in V$
8	7	con3i	$⊢ \neg Z \in V \to \neg {finSupp}_{Z} (x)$
9	8	ralrimivw	$⊢ \neg Z \in V \to \forall x \in (B^{A}) \neg {finSupp}_{Z} (x)$
10		rabeq0	$⊢ \{x \in (B^{A}) \| {finSupp}_{Z} (x)\} = \emptyset \leftrightarrow \forall x \in (B^{A}) \neg {finSupp}_{Z} (x)$
11	9 10	sylibr	$⊢ \neg Z \in V \to \{x \in (B^{A}) \| {finSupp}_{Z} (x)\} = \emptyset$
12	2 11	eqtrid	$⊢ \neg Z \in V \to U = \emptyset$
13		soeq2	$⊢ U = \emptyset \to (T Or U \leftrightarrow T Or \emptyset)$
14	12 13	syl	$⊢ \neg Z \in V \to (T Or U \leftrightarrow T Or \emptyset)$
15	5 14	mpbiri	$⊢ \neg Z \in V \to T Or U$
16	15	a1d	$⊢ \neg Z \in V \to ((A \in V \land R Or A \land S Or B) \to T Or U)$
17	4 16	pm2.61i	$⊢ (A \in V \land R Or A \land S Or B) \to T Or U$