Theorem mapunen 8689

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.)

Assertion

Ref	Expression
mapunen	⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑m (𝐴 ∪ 𝐵)) ≈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))

Proof of Theorem mapunen

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 7192	. . 3 ⊢ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∈ V
2	1	a1i 11	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑m (𝐴 ∪ 𝐵)) ∈ V)
3		ovex 7192	. . . 4 ⊢ (𝐶 ↑m 𝐴) ∈ V
4		ovex 7192	. . . 4 ⊢ (𝐶 ↑m 𝐵) ∈ V
5	3, 4	xpex 7479	. . 3 ⊢ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) ∈ V
6	5	a1i 11	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) ∈ V)
7		elmapi 8431	. . . . 5 ⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → 𝑥:(𝐴 ∪ 𝐵)⟶𝐶)
8		ssun1 4151	. . . . 5 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
9		fssres 6547	. . . . 5 ⊢ ((𝑥:(𝐴 ∪ 𝐵)⟶𝐶 ∧ 𝐴 ⊆ (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐴):𝐴⟶𝐶)
10	7, 8, 9	sylancl 588	. . . 4 ⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐴):𝐴⟶𝐶)
11		ssun2 4152	. . . . 5 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
12		fssres 6547	. . . . 5 ⊢ ((𝑥:(𝐴 ∪ 𝐵)⟶𝐶 ∧ 𝐵 ⊆ (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐵):𝐵⟶𝐶)
13	7, 11, 12	sylancl 588	. . . 4 ⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐵):𝐵⟶𝐶)
14	10, 13	jca 514	. . 3 ⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → ((𝑥 ↾ 𝐴):𝐴⟶𝐶 ∧ (𝑥 ↾ 𝐵):𝐵⟶𝐶))
15		opelxp 5594	. . . 4 ⊢ (⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) ↔ ((𝑥 ↾ 𝐴) ∈ (𝐶 ↑m 𝐴) ∧ (𝑥 ↾ 𝐵) ∈ (𝐶 ↑m 𝐵)))
16		simpl3 1189	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐶 ∈ 𝑋)
17		simpl1 1187	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ∈ 𝑉)
18	16, 17	elmapd 8423	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ↾ 𝐴) ∈ (𝐶 ↑m 𝐴) ↔ (𝑥 ↾ 𝐴):𝐴⟶𝐶))
19		simpl2 1188	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ∈ 𝑊)
20	16, 19	elmapd 8423	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ↾ 𝐵) ∈ (𝐶 ↑m 𝐵) ↔ (𝑥 ↾ 𝐵):𝐵⟶𝐶))
21	18, 20	anbi12d 632	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (((𝑥 ↾ 𝐴) ∈ (𝐶 ↑m 𝐴) ∧ (𝑥 ↾ 𝐵) ∈ (𝐶 ↑m 𝐵)) ↔ ((𝑥 ↾ 𝐴):𝐴⟶𝐶 ∧ (𝑥 ↾ 𝐵):𝐵⟶𝐶)))
22	15, 21	syl5bb 285	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) ↔ ((𝑥 ↾ 𝐴):𝐴⟶𝐶 ∧ (𝑥 ↾ 𝐵):𝐵⟶𝐶)))
23	14, 22	syl5ibr 248	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))))
24		xp1st 7724	. . . . . . 7 ⊢ (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → (1st ‘𝑦) ∈ (𝐶 ↑m 𝐴))
25	24	adantl 484	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (1st ‘𝑦) ∈ (𝐶 ↑m 𝐴))
26		elmapi 8431	. . . . . 6 ⊢ ((1st ‘𝑦) ∈ (𝐶 ↑m 𝐴) → (1st ‘𝑦):𝐴⟶𝐶)
27	25, 26	syl 17	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (1st ‘𝑦):𝐴⟶𝐶)
28		xp2nd 7725	. . . . . . 7 ⊢ (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → (2nd ‘𝑦) ∈ (𝐶 ↑m 𝐵))
29	28	adantl 484	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (2nd ‘𝑦) ∈ (𝐶 ↑m 𝐵))
30		elmapi 8431	. . . . . 6 ⊢ ((2nd ‘𝑦) ∈ (𝐶 ↑m 𝐵) → (2nd ‘𝑦):𝐵⟶𝐶)
31	29, 30	syl 17	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (2nd ‘𝑦):𝐵⟶𝐶)
32		simplr 767	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (𝐴 ∩ 𝐵) = ∅)
33	27, 31, 32	fun2d 6545	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → ((1st ‘𝑦) ∪ (2nd ‘𝑦)):(𝐴 ∪ 𝐵)⟶𝐶)
34	33	ex 415	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → ((1st ‘𝑦) ∪ (2nd ‘𝑦)):(𝐴 ∪ 𝐵)⟶𝐶))
35		unexg 7475	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
36	17, 19, 35	syl2anc 586	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ V)
37	16, 36	elmapd 8423	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ↔ ((1st ‘𝑦) ∪ (2nd ‘𝑦)):(𝐴 ∪ 𝐵)⟶𝐶))
38	34, 37	sylibrd 261	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∈ (𝐶 ↑m (𝐴 ∪ 𝐵))))
39		1st2nd2 7731	. . . . . . 7 ⊢ (𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
40	39	ad2antll 727	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
41	27	adantrl 714	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (1st ‘𝑦):𝐴⟶𝐶)
42	31	adantrl 714	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (2nd ‘𝑦):𝐵⟶𝐶)
43		res0 5860	. . . . . . . . . 10 ⊢ ((1st ‘𝑦) ↾ ∅) = ∅
44		res0 5860	. . . . . . . . . 10 ⊢ ((2nd ‘𝑦) ↾ ∅) = ∅
45	43, 44	eqtr4i 2850	. . . . . . . . 9 ⊢ ((1st ‘𝑦) ↾ ∅) = ((2nd ‘𝑦) ↾ ∅)
46		simplr 767	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝐴 ∩ 𝐵) = ∅)
47	46	reseq2d 5856	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((1st ‘𝑦) ↾ ∅))
48	46	reseq2d 5856	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ ∅))
49	45, 47, 48	3eqtr4a 2885	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵)))
50		fresaunres1 6554	. . . . . . . 8 ⊢ (((1st ‘𝑦):𝐴⟶𝐶 ∧ (2nd ‘𝑦):𝐵⟶𝐶 ∧ ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵))) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴) = (1st ‘𝑦))
51	41, 42, 49, 50	syl3anc 1367	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴) = (1st ‘𝑦))
52		fresaunres2 6553	. . . . . . . 8 ⊢ (((1st ‘𝑦):𝐴⟶𝐶 ∧ (2nd ‘𝑦):𝐵⟶𝐶 ∧ ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵))) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵) = (2nd ‘𝑦))
53	41, 42, 49, 52	syl3anc 1367	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵) = (2nd ‘𝑦))
54	51, 53	opeq12d 4814	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → ⟨(((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴), (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
55	40, 54	eqtr4d 2862	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → 𝑦 = ⟨(((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴), (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵)⟩)
56		reseq1 5850	. . . . . . 7 ⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → (𝑥 ↾ 𝐴) = (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴))
57		reseq1 5850	. . . . . . 7 ⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → (𝑥 ↾ 𝐵) = (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵))
58	56, 57	opeq12d 4814	. . . . . 6 ⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ = ⟨(((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴), (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵)⟩)
59	58	eqeq2d 2835	. . . . 5 ⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ↔ 𝑦 = ⟨(((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴), (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵)⟩))
60	55, 59	syl5ibrcom 249	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → 𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩))
61		ffn 6517	. . . . . . . 8 ⊢ (𝑥:(𝐴 ∪ 𝐵)⟶𝐶 → 𝑥 Fn (𝐴 ∪ 𝐵))
62		fnresdm 6469	. . . . . . . 8 ⊢ (𝑥 Fn (𝐴 ∪ 𝐵) → (𝑥 ↾ (𝐴 ∪ 𝐵)) = 𝑥)
63	7, 61, 62	3syl 18	. . . . . . 7 ⊢ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) → (𝑥 ↾ (𝐴 ∪ 𝐵)) = 𝑥)
64	63	ad2antrl 726	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝑥 ↾ (𝐴 ∪ 𝐵)) = 𝑥)
65	64	eqcomd 2830	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → 𝑥 = (𝑥 ↾ (𝐴 ∪ 𝐵)))
66		vex 3500	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
67	66	resex 5902	. . . . . . . . 9 ⊢ (𝑥 ↾ 𝐴) ∈ V
68	66	resex 5902	. . . . . . . . 9 ⊢ (𝑥 ↾ 𝐵) ∈ V
69	67, 68	op1std 7702	. . . . . . . 8 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → (1st ‘𝑦) = (𝑥 ↾ 𝐴))
70	67, 68	op2ndd 7703	. . . . . . . 8 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → (2nd ‘𝑦) = (𝑥 ↾ 𝐵))
71	69, 70	uneq12d 4143	. . . . . . 7 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → ((1st ‘𝑦) ∪ (2nd ‘𝑦)) = ((𝑥 ↾ 𝐴) ∪ (𝑥 ↾ 𝐵)))
72		resundi 5870	. . . . . . 7 ⊢ (𝑥 ↾ (𝐴 ∪ 𝐵)) = ((𝑥 ↾ 𝐴) ∪ (𝑥 ↾ 𝐵))
73	71, 72	syl6eqr 2877	. . . . . 6 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → ((1st ‘𝑦) ∪ (2nd ‘𝑦)) = (𝑥 ↾ (𝐴 ∪ 𝐵)))
74	73	eqeq2d 2835	. . . . 5 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↔ 𝑥 = (𝑥 ↾ (𝐴 ∪ 𝐵))))
75	65, 74	syl5ibrcom 249	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → 𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦))))
76	60, 75	impbid 214	. . 3 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))) → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↔ 𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩))
77	76	ex 415	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↔ 𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩)))
78	2, 6, 23, 38, 77	en3d 8549	1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑m (𝐴 ∪ 𝐵)) ≈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1536   ∈ wcel 2113  Vcvv 3497   ∪ cun 3937   ∩ cin 3938   ⊆ wss 3939  ∅c0 4294  ⟨cop 4576   class class class wbr 5069   × cxp 5556   ↾ cres 5560   Fn wfn 6353  ⟶wf 6354  ‘cfv 6358  (class class class)co 7159  1^st c1st 7690  2^nd c2nd 7691   ↑_m cmap 8409   ≈ cen 8509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7162  df-oprab 7163  df-mpo 7164  df-1st 7692  df-2nd 7693  df-map 8411  df-en 8513

This theorem is referenced by:  map2xp  8690  mapdom2  8691  mapdjuen  9609  ackbij1lem5  9649  hashmap  13799  mpct  41470