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		ovex	$⊢ C^{(A \cup B)} \in V$
2	1	a1i	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to C^{(A \cup B)} \in V$
3		ovex	$⊢ C^{A} \in V$
4		ovex	$⊢ C^{B} \in V$
5	3 4	xpex	$⊢ (C^{A}) \times (C^{B}) \in V$
6	5	a1i	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to (C^{A}) \times (C^{B}) \in V$
7		elmapi	$⊢ x \in (C^{(A \cup B)}) \to x : A \cup B ⟶ C$
8		ssun1	$⊢ A \subseteq A \cup B$
9		fssres	$⊢ (x : A \cup B ⟶ C \land A \subseteq A \cup B) \to ({x ↾}_{A}) : A ⟶ C$
10	7 8 9	sylancl	$⊢ x \in (C^{(A \cup B)}) \to ({x ↾}_{A}) : A ⟶ C$
11		ssun2	$⊢ B \subseteq A \cup B$
12		fssres	$⊢ (x : A \cup B ⟶ C \land B \subseteq A \cup B) \to ({x ↾}_{B}) : B ⟶ C$
13	7 11 12	sylancl	$⊢ x \in (C^{(A \cup B)}) \to ({x ↾}_{B}) : B ⟶ C$
14	10 13	jca	$⊢ x \in (C^{(A \cup B)}) \to (({x ↾}_{A}) : A ⟶ C \land ({x ↾}_{B}) : B ⟶ C)$
15		opelxp	$⊢ ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \in ((C^{A}) \times (C^{B})) \leftrightarrow ({x ↾}_{A} \in (C^{A}) \land {x ↾}_{B} \in (C^{B}))$
16		simpl3	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to C \in X$
17		simpl1	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to A \in V$
18	16 17	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)$
19		simpl2	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to B \in W$
20	16 19	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)$
21	18 20	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))$
22	15 21	syl5bb	$⊢ ((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))$
23	14 22	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})))$
24		xp1st	$⊢ y \in ((C^{A}) \times (C^{B})) \to 1^{st} (y) \in (C^{A})$
25	24	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})$
26		elmapi	$⊢ 1^{st} (y) \in (C^{A}) \to 1^{st} (y) : A ⟶ C$
27	25 26	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$
28		xp2nd	$⊢ y \in ((C^{A}) \times (C^{B})) \to 2^{nd} (y) \in (C^{B})$
29	28	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})$
30		elmapi	$⊢ 2^{nd} (y) \in (C^{B}) \to 2^{nd} (y) : B ⟶ C$
31	29 30	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$
32		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$
33	27 31 32	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$
34	33	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)$
35		unexg	$⊢ (A \in V \land B \in W) \to A \cup B \in V$
36	17 19 35	syl2anc	$⊢ ((A \in V \land B \in W \land C \in X) \land A \cap B = \emptyset) \to A \cup B \in V$
37	16 36	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)$
38	34 37	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)}))$
39		1st2nd2	$⊢ y \in ((C^{A}) \times (C^{B})) \to y = ⟨1^{st} (y), 2^{nd} (y)⟩$
40	39	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)⟩$
41	27	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$
42	31	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$
43		res0	$⊢ {1^{st} (y) ↾}_{\emptyset} = \emptyset$
44		res0	$⊢ {2^{nd} (y) ↾}_{\emptyset} = \emptyset$
45	43 44	eqtr4i	$⊢ {1^{st} (y) ↾}_{\emptyset} = {2^{nd} (y) ↾}_{\emptyset}$
46		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$
47	46	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}$
48	46	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}$
49	45 47 48	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)}$
50		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)$
51	41 42 49 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)) ↾}_{A} = 1^{st} (y)$
52		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)$
53	41 42 49 52	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)$
54	51 53	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)⟩$
55	40 54	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}⟩$
56		reseq1	$⊢ x = 1^{st} (y) \cup 2^{nd} (y) \to {x ↾}_{A} = {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{A}$
57		reseq1	$⊢ x = 1^{st} (y) \cup 2^{nd} (y) \to {x ↾}_{B} = {(1^{st} (y) \cup 2^{nd} (y)) ↾}_{B}$
58	56 57	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}⟩$
59	58	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}⟩)$
60	55 59	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}⟩)$
61		ffn	$⊢ x : A \cup B ⟶ C \to x Fn (A \cup B)$
62		fnresdm	$⊢ x Fn (A \cup B) \to {x ↾}_{(A \cup B)} = x$
63	7 61 62	3syl	$⊢ x \in (C^{(A \cup B)}) \to {x ↾}_{(A \cup B)} = x$
64	63	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$
65	64	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)}$
66		vex	$⊢ x \in V$
67	66	resex	$⊢ {x ↾}_{A} \in V$
68	66	resex	$⊢ {x ↾}_{B} \in V$
69	67 68	op1std	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 1^{st} (y) = {x ↾}_{A}$
70	67 68	op2ndd	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 2^{nd} (y) = {x ↾}_{B}$
71	69 70	uneq12d	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 1^{st} (y) \cup 2^{nd} (y) = ({x ↾}_{A}) \cup ({x ↾}_{B})$
72		resundi	$⊢ {x ↾}_{(A \cup B)} = ({x ↾}_{A}) \cup ({x ↾}_{B})$
73	71 72	syl6eqr	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to 1^{st} (y) \cup 2^{nd} (y) = {x ↾}_{(A \cup B)}$
74	73	eqeq2d	$⊢ y = ⟨{x ↾}_{A}, {x ↾}_{B}⟩ \to (x = 1^{st} (y) \cup 2^{nd} (y) \leftrightarrow x = {x ↾}_{(A \cup B)})$
75	65 74	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))$
76	60 75	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}⟩)$
77	76	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}⟩))$
78	2 6 23 38 77	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