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	syl5ibr	$⊢ ((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		unexg	$⊢ (A \in V \land B \in W) \to A \cup B \in V$
34	15 17 33	syl2anc	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to A \cup B \in V$
35	14 34	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)$
36	32 35	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)}))$
37		1st2nd2	$⊢ y \in ((C^{A}) \times (C^{B})) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
38	37	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)⟩$
39	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$
40	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$
41		res0	$⊢ {1^{st} (y) ↾}_{\emptyset} = \emptyset$
42		res0	$⊢ {2^{nd} (y) ↾}_{\emptyset} = \emptyset$
43	41 42	eqtr4i	$⊢ {1^{st} (y) ↾}_{\emptyset} = {2^{nd} (y) ↾}_{\emptyset}$
44		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$
45	44	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}$
46	44	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}$
47	43 45 46	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)}$
48		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)$
49	39 40 47 48	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)$
50		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)$
51	39 40 47 50	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)$
52	49 51	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)⟩$
53	38 52	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}⟩$
54		reseq1	$⊢ x = 1^{st} (y) \cup 2^{nd} (y) \to {x ↾}_{A} = {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{A}$
55		reseq1	$⊢ x = 1^{st} (y) \cup 2^{nd} (y) \to {x ↾}_{B} = {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{B}$
56	54 55	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}⟩$
57	56	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}⟩)$
58	53 57	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}⟩)$
59		ffn	$⊢ x : A \cup B ⟶ C \to x Fn (A \cup B)$
60		fnresdm	$⊢ x Fn (A \cup B) \to {x ↾}_{(A \cup B)} = x$
61	5 59 60	3syl	$⊢ x \in (C^{(A \cup B)}) \to {x ↾}_{(A \cup B)} = x$
62	61	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$
63	62	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)}$
64		vex	$⊢ x \in V$
65	64	resex	$⊢ {x ↾}_{A} \in V$
66	64	resex	$⊢ {x ↾}_{B} \in V$
67	65 66	op1std	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 1^{st} (y) = {x ↾}_{A}$
68	65 66	op2ndd	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 2^{nd} (y) = {x ↾}_{B}$
69	67 68	uneq12d	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 1^{st} (y) \cup 2^{nd} (y) = ({x ↾}_{A}) \cup ({x ↾}_{B})$
70		resundi	$⊢ {x ↾}_{(A \cup B)} = ({x ↾}_{A}) \cup ({x ↾}_{B})$
71	69 70	eqtr4di	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 1^{st} (y) \cup 2^{nd} (y) = {x ↾}_{(A \cup B)}$
72	71	eqeq2d	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to (x = 1^{st} (y) \cup 2^{nd} (y) \leftrightarrow x = {x ↾}_{(A \cup B)})$
73	63 72	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))$
74	58 73	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}⟩)$
75	74	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}⟩))$
76	1 4 21 36 75	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