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⟩ \| \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	wemapso2lem	$⊢ ((A \in V \land R Or A \land S Or B) \land Z \in W) \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	2	ssrab3	$⊢ U \subseteq B^{A}$
4		simpl2	$⊢ ((A \in V \land R Or A \land S Or B) \land Z \in W) \to R Or A$
5		simpl3	$⊢ ((A \in V \land R Or A \land S Or B) \land Z \in W) \to S Or B$
6		simprll	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to a \in U$
7		breq1	$⊢ x = a \to ({finSupp}_{Z} (x) \leftrightarrow {finSupp}_{Z} (a))$
8	7 2	elrab2	$⊢ a \in U \leftrightarrow (a \in (B^{A}) \land {finSupp}_{Z} (a))$
9	8	simprbi	$⊢ a \in U \to {finSupp}_{Z} (a)$
10	6 9	syl	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to {finSupp}_{Z} (a)$
11		simprlr	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to b \in U$
12		breq1	$⊢ x = b \to ({finSupp}_{Z} (x) \leftrightarrow {finSupp}_{Z} (b))$
13	12 2	elrab2	$⊢ b \in U \leftrightarrow (b \in (B^{A}) \land {finSupp}_{Z} (b))$
14	13	simprbi	$⊢ b \in U \to {finSupp}_{Z} (b)$
15	11 14	syl	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to {finSupp}_{Z} (b)$
16	10 15	fsuppunfi	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to {supp}_{Z} (a) \cup {supp}_{Z} (b) \in Fin$
17	3 6	sseldi	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to a \in (B^{A})$
18		elmapi	$⊢ a \in (B^{A}) \to a : A ⟶ B$
19	17 18	syl	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to a : A ⟶ B$
20	19	ffnd	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to a Fn A$
21	3 11	sseldi	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to b \in (B^{A})$
22		elmapi	$⊢ b \in (B^{A}) \to b : A ⟶ B$
23	21 22	syl	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to b : A ⟶ B$
24	23	ffnd	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to b Fn A$
25		fndmdif	$⊢ (a Fn A \land b Fn A) \to dom (a ∖ b) = \{c \in A \| a (c) \neq b (c)\}$
26	20 24 25	syl2anc	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to dom (a ∖ b) = \{c \in A \| a (c) \neq b (c)\}$
27		neneor	$⊢ a (c) \neq b (c) \to (a (c) \neq Z \lor b (c) \neq Z)$
28		elun	$⊢ c \in ({supp}_{Z} (a) \cup {supp}_{Z} (b)) \leftrightarrow (c \in {supp}_{Z} (a) \lor c \in {supp}_{Z} (b))$
29		simpr	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to c \in A$
30	20	adantr	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to a Fn A$
31		elex	$⊢ A \in V \to A \in V$
32	31	3ad2ant1	$⊢ (A \in V \land R Or A \land S Or B) \to A \in V$
33	32	adantr	$⊢ ((A \in V \land R Or A \land S Or B) \land Z \in W) \to A \in V$
34	33	ad2antrr	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to A \in V$
35		simpr	$⊢ ((A \in V \land R Or A \land S Or B) \land Z \in W) \to Z \in W$
36	35	ad2antrr	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to Z \in W$
37		elsuppfn	$⊢ (a Fn A \land A \in V \land Z \in W) \to (c \in {supp}_{Z} (a) \leftrightarrow (c \in A \land a (c) \neq Z))$
38	30 34 36 37	syl3anc	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to (c \in {supp}_{Z} (a) \leftrightarrow (c \in A \land a (c) \neq Z))$
39	29 38	mpbirand	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to (c \in {supp}_{Z} (a) \leftrightarrow a (c) \neq Z)$
40	24	adantr	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to b Fn A$
41		simpll1	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to A \in V$
42	41	adantr	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to A \in V$
43		elsuppfn	$⊢ (b Fn A \land A \in V \land Z \in W) \to (c \in {supp}_{Z} (b) \leftrightarrow (c \in A \land b (c) \neq Z))$
44	40 42 36 43	syl3anc	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to (c \in {supp}_{Z} (b) \leftrightarrow (c \in A \land b (c) \neq Z))$
45	29 44	mpbirand	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to (c \in {supp}_{Z} (b) \leftrightarrow b (c) \neq Z)$
46	39 45	orbi12d	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to ((c \in {supp}_{Z} (a) \lor c \in {supp}_{Z} (b)) \leftrightarrow (a (c) \neq Z \lor b (c) \neq Z))$
47	28 46	syl5bb	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to (c \in ({supp}_{Z} (a) \cup {supp}_{Z} (b)) \leftrightarrow (a (c) \neq Z \lor b (c) \neq Z))$
48	27 47	syl5ibr	$⊢ ((((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \land c \in A) \to (a (c) \neq b (c) \to c \in ({supp}_{Z} (a) \cup {supp}_{Z} (b)))$
49	48	ralrimiva	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to \forall c \in A (a (c) \neq b (c) \to c \in ({supp}_{Z} (a) \cup {supp}_{Z} (b)))$
50		rabss	$⊢ \{c \in A \| a (c) \neq b (c)\} \subseteq {supp}_{Z} (a) \cup {supp}_{Z} (b) \leftrightarrow \forall c \in A (a (c) \neq b (c) \to c \in ({supp}_{Z} (a) \cup {supp}_{Z} (b)))$
51	49 50	sylibr	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to \{c \in A \| a (c) \neq b (c)\} \subseteq {supp}_{Z} (a) \cup {supp}_{Z} (b)$
52	26 51	eqsstrd	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to dom (a ∖ b) \subseteq {supp}_{Z} (a) \cup {supp}_{Z} (b)$
53	16 52	ssfid	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to dom (a ∖ b) \in Fin$
54		suppssdm	$⊢ a supp Z \subseteq dom a$
55	54 19	fssdm	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to a supp Z \subseteq A$
56		suppssdm	$⊢ b supp Z \subseteq dom b$
57	56 23	fssdm	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to b supp Z \subseteq A$
58	55 57	unssd	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to {supp}_{Z} (a) \cup {supp}_{Z} (b) \subseteq A$
59	4	adantr	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to R Or A$
60		soss	$⊢ {supp}_{Z} (a) \cup {supp}_{Z} (b) \subseteq A \to (R Or A \to R Or ({supp}_{Z} (a) \cup {supp}_{Z} (b)))$
61	58 59 60	sylc	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to R Or ({supp}_{Z} (a) \cup {supp}_{Z} (b))$
62		wofi	$⊢ (R Or ({supp}_{Z} (a) \cup {supp}_{Z} (b)) \land {supp}_{Z} (a) \cup {supp}_{Z} (b) \in Fin) \to R We ({supp}_{Z} (a) \cup {supp}_{Z} (b))$
63	61 16 62	syl2anc	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to R We ({supp}_{Z} (a) \cup {supp}_{Z} (b))$
64		wefr	$⊢ R We ({supp}_{Z} (a) \cup {supp}_{Z} (b)) \to R Fr ({supp}_{Z} (a) \cup {supp}_{Z} (b))$
65	63 64	syl	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to R Fr ({supp}_{Z} (a) \cup {supp}_{Z} (b))$
66		simprr	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to a \neq b$
67		fndmdifeq0	$⊢ (a Fn A \land b Fn A) \to (dom (a ∖ b) = \emptyset \leftrightarrow a = b)$
68	20 24 67	syl2anc	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to (dom (a ∖ b) = \emptyset \leftrightarrow a = b)$
69	68	necon3bid	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to (dom (a ∖ b) \neq \emptyset \leftrightarrow a \neq b)$
70	66 69	mpbird	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to dom (a ∖ b) \neq \emptyset$
71		fri	$⊢ ((dom (a ∖ b) \in Fin \land R Fr ({supp}_{Z} (a) \cup {supp}_{Z} (b))) \land (dom (a ∖ b) \subseteq {supp}_{Z} (a) \cup {supp}_{Z} (b) \land dom (a ∖ b) \neq \emptyset)) \to \exists c \in dom (a ∖ b) \forall d \in dom (a ∖ b) \neg d R c$
72	53 65 52 70 71	syl22anc	$⊢ (((A \in V \land R Or A \land S Or B) \land Z \in W) \land ((a \in U \land b \in U) \land a \neq b)) \to \exists c \in dom (a ∖ b) \forall d \in dom (a ∖ b) \neg d R c$
73	1 3 4 5 72	wemapsolem	$⊢ ((A \in V \land R Or A \land S Or B) \land Z \in W) \to T Or U$

Metamath Proof Explorer

Theorem wemapso2lem

Proof