mapunen

Description: Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of Mendelson p. 255. (Contributed by NM, 23-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	mapunen	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (C^{(A \cup B)}) \approx ((C^{A}) \times (C^{B}))$

Proof

Step	Hyp	Ref	Expression
1		ovexd	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to C^{(A \cup B)} \in V$
2		ovexd	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to C^{A} \in V$
3		ovexd	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to C^{B} \in V$
4	2 3	xpexd	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (C^{A}) \times (C^{B}) \in V$
5		elmapi	$⊢ x \in (C^{(A \cup B)}) \to x : A \cup B ⟶ C$
6		ssun1	$⊢ A \subseteq A \cup B$
7		fssres	$⊢ (x : A \cup B ⟶ C \land A \subseteq A \cup B) \to ({x ↾}_{A}) : A ⟶ C$
8	5 6 7	sylancl	$⊢ x \in (C^{(A \cup B)}) \to ({x ↾}_{A}) : A ⟶ C$
9		ssun2	$⊢ B \subseteq A \cup B$
10		fssres	$⊢ (x : A \cup B ⟶ C \land B \subseteq A \cup B) \to ({x ↾}_{B}) : B ⟶ C$
11	5 9 10	sylancl	$⊢ x \in (C^{(A \cup B)}) \to ({x ↾}_{B}) : B ⟶ C$
12	8 11	jca	$⊢ x \in (C^{(A \cup B)}) \to (({x ↾}_{A}) : A ⟶ C \land ({x ↾}_{B}) : B ⟶ C)$
13		opelxp	$⊢ ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \in ((C^{A}) \times (C^{B})) \leftrightarrow ({x ↾}_{A} \in (C^{A}) \land {x ↾}_{B} \in (C^{B}))$
14		simpl3	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to C \in X$
15		simpl1	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to A \in V$
16	14 15	elmapd	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to ({x ↾}_{A} \in (C^{A}) \leftrightarrow ({x ↾}_{A}) : A ⟶ C)$
17		simpl2	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to B \in W$
18	14 17	elmapd	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to ({x ↾}_{B} \in (C^{B}) \leftrightarrow ({x ↾}_{B}) : B ⟶ C)$
19	16 18	anbi12d	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (({x ↾}_{A} \in (C^{A}) \land {x ↾}_{B} \in (C^{B})) \leftrightarrow (({x ↾}_{A}) : A ⟶ C \land ({x ↾}_{B}) : B ⟶ C))$
20	13 19	bitrid	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (⟨{x ↾}_{A}, {x ↾}_{B}⟩ \in ((C^{A}) \times (C^{B})) \leftrightarrow (({x ↾}_{A}) : A ⟶ C \land ({x ↾}_{B}) : B ⟶ C))$
21	12 20	imbitrrid	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (x \in (C^{(A \cup B)}) \to ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \in ((C^{A}) \times (C^{B})))$
22		xp1st	$⊢ y \in ((C^{A}) \times (C^{B})) \to 1^{st} (y) \in (C^{A})$
23	22	adantl	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land y \in ((C^{A}) \times (C^{B}))) \to 1^{st} (y) \in (C^{A})$
24		elmapi	$⊢ 1^{st} (y) \in (C^{A}) \to 1^{st} (y) : A ⟶ C$
25	23 24	syl	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land y \in ((C^{A}) \times (C^{B}))) \to 1^{st} (y) : A ⟶ C$
26		xp2nd	$⊢ y \in ((C^{A}) \times (C^{B})) \to 2^{nd} (y) \in (C^{B})$
27	26	adantl	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land y \in ((C^{A}) \times (C^{B}))) \to 2^{nd} (y) \in (C^{B})$
28		elmapi	$⊢ 2^{nd} (y) \in (C^{B}) \to 2^{nd} (y) : B ⟶ C$
29	27 28	syl	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land y \in ((C^{A}) \times (C^{B}))) \to 2^{nd} (y) : B ⟶ C$
30		simplr	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land y \in ((C^{A}) \times (C^{B}))) \to A \cap B = \emptyset$
31	25 29 30	fun2d	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land y \in ((C^{A}) \times (C^{B}))) \to (1^{st} (y) \cup 2^{nd} (y)) : A \cup B ⟶ C$
32	31	ex	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (y \in ((C^{A}) \times (C^{B})) \to (1^{st} (y) \cup 2^{nd} (y)) : A \cup B ⟶ C)$
33	15 17	unexd	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to A \cup B \in V$
34	14 33	elmapd	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (1^{st} (y) \cup 2^{nd} (y) \in (C^{(A \cup B)}) \leftrightarrow (1^{st} (y) \cup 2^{nd} (y)) : A \cup B ⟶ C)$
35	32 34	sylibrd	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (y \in ((C^{A}) \times (C^{B})) \to 1^{st} (y) \cup 2^{nd} (y) \in (C^{(A \cup B)}))$
36		1st2nd2	$⊢ y \in ((C^{A}) \times (C^{B})) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
37	36	ad2antll	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
38	25	adantrl	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to 1^{st} (y) : A ⟶ C$
39	29	adantrl	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to 2^{nd} (y) : B ⟶ C$
40		res0	$⊢ {1^{st} (y) ↾}_{\emptyset} = \emptyset$
41		res0	$⊢ {2^{nd} (y) ↾}_{\emptyset} = \emptyset$
42	40 41	eqtr4i	$⊢ {1^{st} (y) ↾}_{\emptyset} = {2^{nd} (y) ↾}_{\emptyset}$
43		simplr	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to A \cap B = \emptyset$
44	43	reseq2d	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to {1^{st} (y) ↾}_{(A \cap B)} = {1^{st} (y) ↾}_{\emptyset}$
45	43	reseq2d	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to {2^{nd} (y) ↾}_{(A \cap B)} = {2^{nd} (y) ↾}_{\emptyset}$
46	42 44 45	3eqtr4a	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to {1^{st} (y) ↾}_{(A \cap B)} = {2^{nd} (y) ↾}_{(A \cap B)}$
47		fresaunres1	$⊢ (1^{st} (y) : A ⟶ C \land 2^{nd} (y) : B ⟶ C \land {1^{st} (y) ↾}_{(A \cap B)} = {2^{nd} (y) ↾}_{(A \cap B)}) \to {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{A} = 1^{st} (y)$
48	38 39 46 47	syl3anc	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{A} = 1^{st} (y)$
49		fresaunres2	$⊢ (1^{st} (y) : A ⟶ C \land 2^{nd} (y) : B ⟶ C \land {1^{st} (y) ↾}_{(A \cap B)} = {2^{nd} (y) ↾}_{(A \cap B)}) \to {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{B} = 2^{nd} (y)$
50	38 39 46 49	syl3anc	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{B} = 2^{nd} (y)$
51	48 50	opeq12d	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to ⟨{(1^{st} (y) \cup 2^{nd} (y)) ↾}_{A}, {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{B}⟩ = ⟨1^{st} (y), 2^{nd} (y)⟩$
52	37 51	eqtr4d	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to y = ⟨{(1^{st} (y) \cup 2^{nd} (y)) ↾}_{A}, {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{B}⟩$
53		reseq1	$⊢ x = 1^{st} (y) \cup 2^{nd} (y) \to {x ↾}_{A} = {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{A}$
54		reseq1	$⊢ x = 1^{st} (y) \cup 2^{nd} (y) \to {x ↾}_{B} = {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{B}$
55	53 54	opeq12d	$⊢ x = 1^{st} (y) \cup 2^{nd} (y) \to ⟨{x ↾}_{A}, {x ↾}_{B}⟩ = ⟨{(1^{st} (y) \cup 2^{nd} (y)) ↾}_{A}, {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{B}⟩$
56	55	eqeq2d	$⊢ x = 1^{st} (y) \cup 2^{nd} (y) \to (y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \leftrightarrow y = ⟨{(1^{st} (y) \cup 2^{nd} (y)) ↾}_{A}, {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{B}⟩)$
57	52 56	syl5ibrcom	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to (x = 1^{st} (y) \cup 2^{nd} (y) \to y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩)$
58		ffn	$⊢ x : A \cup B ⟶ C \to x Fn (A \cup B)$
59		fnresdm	$⊢ x Fn (A \cup B) \to {x ↾}_{(A \cup B)} = x$
60	5 58 59	3syl	$⊢ x \in (C^{(A \cup B)}) \to {x ↾}_{(A \cup B)} = x$
61	60	ad2antrl	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to {x ↾}_{(A \cup B)} = x$
62	61	eqcomd	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to x = {x ↾}_{(A \cup B)}$
63		vex	$⊢ x \in V$
64	63	resex	$⊢ {x ↾}_{A} \in V$
65	63	resex	$⊢ {x ↾}_{B} \in V$
66	64 65	op1std	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 1^{st} (y) = {x ↾}_{A}$
67	64 65	op2ndd	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 2^{nd} (y) = {x ↾}_{B}$
68	66 67	uneq12d	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 1^{st} (y) \cup 2^{nd} (y) = ({x ↾}_{A}) \cup ({x ↾}_{B})$
69		resundi	$⊢ {x ↾}_{(A \cup B)} = ({x ↾}_{A}) \cup ({x ↾}_{B})$
70	68 69	eqtr4di	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 1^{st} (y) \cup 2^{nd} (y) = {x ↾}_{(A \cup B)}$
71	70	eqeq2d	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to (x = 1^{st} (y) \cup 2^{nd} (y) \leftrightarrow x = {x ↾}_{(A \cup B)})$
72	62 71	syl5ibrcom	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to (y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to x = 1^{st} (y) \cup 2^{nd} (y))$
73	57 72	impbid	$⊢ (((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \land (x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B})))) \to (x = 1^{st} (y) \cup 2^{nd} (y) \leftrightarrow y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩)$
74	73	ex	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to ((x \in (C^{(A \cup B)}) \land y \in ((C^{A}) \times (C^{B}))) \to (x = 1^{st} (y) \cup 2^{nd} (y) \leftrightarrow y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩))$
75	1 4 21 35 74	en3d	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (C^{(A \cup B)}) \approx ((C^{A}) \times (C^{B}))$

Metamath Proof Explorer

Theorem mapunen

Proof