Theorem mapunen 3397

Description: Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of [Mendelson] p. 255.

Hypotheses

Ref	Expression
mapunen.1	|- A e. V
mapunen.2	|- B e. V
mapunen.3	|- C e. V

Assertion

Ref	Expression
mapunen	|- ((A i^i B) = (/) -> (C ^m (A u. B)) ~~ ((C ^m A) X. (C ^m B)))

Proof of Theorem mapunen

Step	Hyp	Ref	Expression
1		oprex 3018	. . 3 |- (C ^m (A u. B)) e. V
2	1	a1i 7	. 2 |- ((A i^i B) = (/) -> (C ^m (A u. B)) e. V)
3		ssun1 1621	. . . . . . 7 |- A (_ (A u. B)
4		fssres 2764	. . . . . . 7 |- ((x:(A u. B)-->C /\ A (_ (A u. B)) -> (x |` A):A-->C)
5	3, 4	mpan2 519	. . . . . 6 |- (x:(A u. B)-->C -> (x |` A):A-->C)
6		mapunen.3	. . . . . . 7 |- C e. V
7		mapunen.1	. . . . . . 7 |- A e. V
8	6, 7	elmap 3265	. . . . . 6 |- ((x |` A) e. (C ^m A) <-> (x |` A):A-->C)
9	5, 8	sylibr 175	. . . . 5 |- (x:(A u. B)-->C -> (x |` A) e. (C ^m A))
10		ssun2 1622	. . . . . . 7 |- B (_ (A u. B)
11		fssres 2764	. . . . . . 7 |- ((x:(A u. B)-->C /\ B (_ (A u. B)) -> (x |` B):B-->C)
12	10, 11	mpan2 519	. . . . . 6 |- (x:(A u. B)-->C -> (x |` B):B-->C)
13		mapunen.2	. . . . . . 7 |- B e. V
14	6, 13	elmap 3265	. . . . . 6 |- ((x |` B) e. (C ^m B) <-> (x |` B):B-->C)
15	12, 14	sylibr 175	. . . . 5 |- (x:(A u. B)-->C -> (x |` B) e. (C ^m B))
16	9, 15	jca 236	. . . 4 |- (x:(A u. B)-->C -> ((x |` A) e. (C ^m A) /\ (x |` B) e. (C ^m B)))
17	7, 13	unex 1949	. . . . 5 |- (A u. B) e. V
18	6, 17	elmap 3265	. . . 4 |- (x e. (C ^m (A u. B)) <-> x:(A u. B)-->C)
19		visset 1350	. . . . . 6 |- x e. V
20		resexg 2597	. . . . . 6 |- (x e. V -> (x |` B) e. V)
21	19, 20	ax-mp 6	. . . . 5 |- (x |` B) e. V
22	21	opelxp 2452	. . . 4 |- (<.(x |` A), (x |` B)>. e. ((C ^m A) X. (C ^m B)) <-> ((x |` A) e. (C ^m A) /\ (x |` B) e. (C ^m B)))
23	16, 18, 22	3imtr4 192	. . 3 |- (x e. (C ^m (A u. B)) -> <.(x |` A), (x |` B)>. e. ((C ^m A) X. (C ^m B)))
24	23	a1i 7	. 2 |- ((A i^i B) = (/) -> (x e. (C ^m (A u. B)) -> <.(x |` A), (x |` B)>. e. ((C ^m A) X. (C ^m B))))
25		fun 2763	. . . . . 6 |- (((|^||^|y:A-->C /\ U.ran {y}:B-->C) /\ (A i^i B) = (/)) -> (|^||^|y u. U.ran {y}):(A u. B)-->(C u. C))
26	6, 17	elmap 3265	. . . . . . 7 |- ((|^||^|y u. U.ran {y}) e. (C ^m (A u. B)) <-> (|^||^|y u. U.ran {y}):(A u. B)-->C)
27		unidm 1603	. . . . . . . 8 |- (C u. C) = C
28		feq3 2750	. . . . . . . 8 |- ((C u. C) = C -> ((|^||^|y u. U.ran {y}):(A u. B)-->(C u. C) <-> (|^||^|y u. U.ran {y}):(A u. B)-->C))
29	27, 28	ax-mp 6	. . . . . . 7 |- ((|^||^|y u. U.ran {y}):(A u. B)-->(C u. C) <-> (|^||^|y u. U.ran {y}):(A u. B)-->C)
30	26, 29	bitr4 154	. . . . . 6 |- ((|^||^|y u. U.ran {y}) e. (C ^m (A u. B)) <-> (|^||^|y u. U.ran {y}):(A u. B)-->(C u. C))
31	25, 30	sylibr 175	. . . . 5 |- (((|^||^|y:A-->C /\ U.ran {y}:B-->C) /\ (A i^i B) = (/)) -> (|^||^|y u. U.ran {y}) e. (C ^m (A u. B)))
32		elxp5 2641	. . . . . . 7 |- (y e. ((C ^m A) X. (C ^m B)) <-> (y = <.|^||^|y, U.ran {y}>. /\ (|^||^|y e. (C ^m A) /\ U.ran {y} e. (C ^m B))))
33	32	pm3.27bd 263	. . . . . 6 |- (y e. ((C ^m A) X. (C ^m B)) -> (|^||^|y e. (C ^m A) /\ U.ran {y} e. (C ^m B)))
34	6, 7	elmap 3265	. . . . . . 7 |- (|^||^|y e. (C ^m A) <-> |^||^|y:A-->C)
35	6, 13	elmap 3265	. . . . . . 7 |- (U.ran {y} e. (C ^m B) <-> U.ran {y}:B-->C)
36	34, 35	anbi12i 369	. . . . . 6 |- ((|^||^|y e. (C ^m A) /\ U.ran {y} e. (C ^m B)) <-> (|^||^|y:A-->C /\ U.ran {y}:B-->C))
37	33, 36	sylib 173	. . . . 5 |- (y e. ((C ^m A) X. (C ^m B)) -> (|^||^|y:A-->C /\ U.ran {y}:B-->C))
38	31, 37	sylan 343	. . . 4 |- ((y e. ((C ^m A) X. (C ^m B)) /\ (A i^i B) = (/)) -> (|^||^|y u. U.ran {y}) e. (C ^m (A u. B)))
39	38	exp 291	. . 3 |- (y e. ((C ^m A) X. (C ^m B)) -> ((A i^i B) = (/) -> (|^||^|y u. U.ran {y}) e. (C ^m (A u. B))))
40	39	com12 13	. 2 |- ((A i^i B) = (/) -> (y e. ((C ^m A) X. (C ^m B)) -> (|^||^|y u. U.ran {y}) e. (C ^m (A u. B))))
41		opeq12 1878	. . . . . . . . . . . . . 14 |- (((x |` A) = |^||^|y /\ (x |` B) = U.ran {y}) -> <.(x |` A), (x |` B)>. = <.|^||^|y, U.ran {y}>.)
42		reseq1 2575	. . . . . . . . . . . . . . . 16 |- (x = (|^||^|y u. U.ran {y}) -> (x |` A) = ((|^||^|y u. U.ran {y}) |` A))
43		resundir 2583	. . . . . . . . . . . . . . . 16 |- ((|^||^|y u. U.ran {y}) |` A) = ((|^||^|y |` A) u. (U.ran {y} |` A))
44	42, 43	syl6eq 1140	. . . . . . . . . . . . . . 15 |- (x = (|^||^|y u. U.ran {y}) -> (x |` A) = ((|^||^|y |` A) u. (U.ran {y} |` A)))
45		fnresdm 2731	. . . . . . . . . . . . . . . . . 18 |- (|^||^|y Fn A -> (|^||^|y |` A) = |^||^|y)
46	45	uneq1d 1610	. . . . . . . . . . . . . . . . 17 |- (|^||^|y Fn A -> ((|^||^|y |` A) u. (U.ran {y} |` A)) = (|^||^|y u. (U.ran {y} |` A)))
47		fnresdisj 2732	. . . . . . . . . . . . . . . . . . . . 21 |- (U.ran {y} Fn B -> ((B i^i A) = (/) <-> (U.ran {y} |` A) = (/)))
48	47	biimpa 324	. . . . . . . . . . . . . . . . . . . 20 |- ((U.ran {y} Fn B /\ (B i^i A) = (/)) -> (U.ran {y} |` A) = (/))
49		incom 1636	. . . . . . . . . . . . . . . . . . . . 21 |- (A i^i B) = (B i^i A)
50	49	cleq1i 1108	. . . . . . . . . . . . . . . . . . . 20 |- ((A i^i B) = (/) <-> (B i^i A) = (/))
51	48, 50	sylan2b 347	. . . . . . . . . . . . . . . . . . 19 |- ((U.ran {y} Fn B /\ (A i^i B) = (/)) -> (U.ran {y} |` A) = (/))
52	51	uneq2d 1611	. . . . . . . . . . . . . . . . . 18 |- ((U.ran {y} Fn B /\ (A i^i B) = (/)) -> (|^||^|y u. (U.ran {y} |` A)) = (|^||^|y u. (/)))
53		un0 1721	. . . . . . . . . . . . . . . . . 18 |- (|^||^|y u. (/)) = |^||^|y
54	52, 53	syl6eq 1140	. . . . . . . . . . . . . . . . 17 |- ((U.ran {y} Fn B /\ (A i^i B) = (/)) -> (|^||^|y u. (U.ran {y} |` A)) = |^||^|y)
55	46, 54	sylan9eq 1144	. . . . . . . . . . . . . . . 16 |- ((|^||^|y Fn A /\ (U.ran {y} Fn B /\ (A i^i B) = (/))) -> ((|^||^|y |` A) u. (U.ran {y} |` A)) = |^||^|y)
56	55	anassrs 338	. . . . . . . . . . . . . . 15 |- (((|^||^|y Fn A /\ U.ran {y} Fn B) /\ (A i^i B) = (/)) -> ((|^||^|y |` A) u. (U.ran {y} |` A)) = |^||^|y)
57	44, 56	sylan9eqr 1145	. . . . . . . . . . . . . 14 |- ((((|^||^|y Fn A /\ U.ran {y} Fn B) /\ (A i^i B) = (/)) /\ x = (|^||^|y u. U.ran {y})) -> (x |` A) = |^||^|y)
58		reseq1 2575	. . . . . . . . . . . . . . . 16 |- (x = (|^||^|y u. U.ran {y}) -> (x |` B) = ((|^||^|y u. U.ran {y}) |` B))
59		resundir 2583	. . . . . . . . . . . . . . . 16 |- ((|^||^|y u. U.ran {y}) |` B) = ((|^||^|y |` B) u. (U.ran {y} |` B))
60	58, 59	syl6eq 1140	. . . . . . . . . . . . . . 15 |- (x = (|^||^|y u. U.ran {y}) -> (x |` B) = ((|^||^|y |` B) u. (U.ran {y} |` B)))
61		fnresdm 2731	. . . . . . . . . . . . . . . . . 18 |- (U.ran {y} Fn B -> (U.ran {y} |` B) = U.ran {y})
62	61	uneq2d 1611	. . . . . . . . . . . . . . . . 17 |- (U.ran {y} Fn B -> ((|^||^|y |` B) u. (U.ran {y} |` B)) =