Theorem mapunen 8533

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	⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ≈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))

Proof of Theorem mapunen

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

Step	Hyp	Ref	Expression
1		ovex 7048	. . 3 ⊢ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∈ V
2	1	a1i 11	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∈ V)
3		ovex 7048	. . . 4 ⊢ (𝐶 ↑𝑚 𝐴) ∈ V
4		ovex 7048	. . . 4 ⊢ (𝐶 ↑𝑚 𝐵) ∈ V
5	3, 4	xpex 7333	. . 3 ⊢ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)) ∈ V
6	5	a1i 11	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)) ∈ V)
7		elmapi 8278	. . . . 5 ⊢ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) → 𝑥:(𝐴 ∪ 𝐵)⟶𝐶)
8		ssun1 4069	. . . . 5 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
9		fssres 6412	. . . . 5 ⊢ ((𝑥:(𝐴 ∪ 𝐵)⟶𝐶 ∧ 𝐴 ⊆ (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐴):𝐴⟶𝐶)
10	7, 8, 9	sylancl 586	. . . 4 ⊢ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐴):𝐴⟶𝐶)
11		ssun2 4070	. . . . 5 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
12		fssres 6412	. . . . 5 ⊢ ((𝑥:(𝐴 ∪ 𝐵)⟶𝐶 ∧ 𝐵 ⊆ (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐵):𝐵⟶𝐶)
13	7, 11, 12	sylancl 586	. . . 4 ⊢ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) → (𝑥 ↾ 𝐵):𝐵⟶𝐶)
14	10, 13	jca 512	. . 3 ⊢ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) → ((𝑥 ↾ 𝐴):𝐴⟶𝐶 ∧ (𝑥 ↾ 𝐵):𝐵⟶𝐶))
15		opelxp 5479	. . . 4 ⊢ (⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)) ↔ ((𝑥 ↾ 𝐴) ∈ (𝐶 ↑𝑚 𝐴) ∧ (𝑥 ↾ 𝐵) ∈ (𝐶 ↑𝑚 𝐵)))
16		simpl3 1186	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐶 ∈ 𝑋)
17		simpl1 1184	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐴 ∈ 𝑉)
18	16, 17	elmapd 8270	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ↾ 𝐴) ∈ (𝐶 ↑𝑚 𝐴) ↔ (𝑥 ↾ 𝐴):𝐴⟶𝐶))
19		simpl2 1185	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → 𝐵 ∈ 𝑊)
20	16, 19	elmapd 8270	. . . . 5 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ↾ 𝐵) ∈ (𝐶 ↑𝑚 𝐵) ↔ (𝑥 ↾ 𝐵):𝐵⟶𝐶))
21	18, 20	anbi12d 630	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (((𝑥 ↾ 𝐴) ∈ (𝐶 ↑𝑚 𝐴) ∧ (𝑥 ↾ 𝐵) ∈ (𝐶 ↑𝑚 𝐵)) ↔ ((𝑥 ↾ 𝐴):𝐴⟶𝐶 ∧ (𝑥 ↾ 𝐵):𝐵⟶𝐶)))
22	15, 21	syl5bb 284	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)) ↔ ((𝑥 ↾ 𝐴):𝐴⟶𝐶 ∧ (𝑥 ↾ 𝐵):𝐵⟶𝐶)))
23	14, 22	syl5ibr 247	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) → ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵))))
24		xp1st 7577	. . . . . . 7 ⊢ (𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)) → (1st ‘𝑦) ∈ (𝐶 ↑𝑚 𝐴))
25	24	adantl 482	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵))) → (1st ‘𝑦) ∈ (𝐶 ↑𝑚 𝐴))
26		elmapi 8278	. . . . . 6 ⊢ ((1st ‘𝑦) ∈ (𝐶 ↑𝑚 𝐴) → (1st ‘𝑦):𝐴⟶𝐶)
27	25, 26	syl 17	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵))) → (1st ‘𝑦):𝐴⟶𝐶)
28		xp2nd 7578	. . . . . . 7 ⊢ (𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)) → (2nd ‘𝑦) ∈ (𝐶 ↑𝑚 𝐵))
29	28	adantl 482	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵))) → (2nd ‘𝑦) ∈ (𝐶 ↑𝑚 𝐵))
30		elmapi 8278	. . . . . 6 ⊢ ((2nd ‘𝑦) ∈ (𝐶 ↑𝑚 𝐵) → (2nd ‘𝑦):𝐵⟶𝐶)
31	29, 30	syl 17	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵))) → (2nd ‘𝑦):𝐵⟶𝐶)
32		simplr 765	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵))) → (𝐴 ∩ 𝐵) = ∅)
33	27, 31, 32	fun2d 6410	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵))) → ((1st ‘𝑦) ∪ (2nd ‘𝑦)):(𝐴 ∪ 𝐵)⟶𝐶)
34	33	ex 413	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)) → ((1st ‘𝑦) ∪ (2nd ‘𝑦)):(𝐴 ∪ 𝐵)⟶𝐶))
35		unexg 7329	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
36	17, 19, 35	syl2anc 584	. . . 4 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ V)
37	16, 36	elmapd 8270	. . 3 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ↔ ((1st ‘𝑦) ∪ (2nd ‘𝑦)):(𝐴 ∪ 𝐵)⟶𝐶))
38	34, 37	sylibrd 260	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)) → ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵))))
39		1st2nd2 7584	. . . . . . 7 ⊢ (𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
40	39	ad2antll 725	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
41	27	adantrl 712	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → (1st ‘𝑦):𝐴⟶𝐶)
42	31	adantrl 712	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → (2nd ‘𝑦):𝐵⟶𝐶)
43		res0 5738	. . . . . . . . . 10 ⊢ ((1st ‘𝑦) ↾ ∅) = ∅
44		res0 5738	. . . . . . . . . 10 ⊢ ((2nd ‘𝑦) ↾ ∅) = ∅
45	43, 44	eqtr4i 2822	. . . . . . . . 9 ⊢ ((1st ‘𝑦) ↾ ∅) = ((2nd ‘𝑦) ↾ ∅)
46		simplr 765	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → (𝐴 ∩ 𝐵) = ∅)
47	46	reseq2d 5734	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((1st ‘𝑦) ↾ ∅))
48	46	reseq2d 5734	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ ∅))
49	45, 47, 48	3eqtr4a 2857	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵)))
50		fresaunres1 6419	. . . . . . . 8 ⊢ (((1st ‘𝑦):𝐴⟶𝐶 ∧ (2nd ‘𝑦):𝐵⟶𝐶 ∧ ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵))) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴) = (1st ‘𝑦))
51	41, 42, 49, 50	syl3anc 1364	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴) = (1st ‘𝑦))
52		fresaunres2 6418	. . . . . . . 8 ⊢ (((1st ‘𝑦):𝐴⟶𝐶 ∧ (2nd ‘𝑦):𝐵⟶𝐶 ∧ ((1st ‘𝑦) ↾ (𝐴 ∩ 𝐵)) = ((2nd ‘𝑦) ↾ (𝐴 ∩ 𝐵))) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵) = (2nd ‘𝑦))
53	41, 42, 49, 52	syl3anc 1364	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵) = (2nd ‘𝑦))
54	51, 53	opeq12d 4718	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → ⟨(((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴), (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵)⟩ = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
55	40, 54	eqtr4d 2834	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → 𝑦 = ⟨(((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴), (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵)⟩)
56		reseq1 5728	. . . . . . 7 ⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → (𝑥 ↾ 𝐴) = (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴))
57		reseq1 5728	. . . . . . 7 ⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → (𝑥 ↾ 𝐵) = (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵))
58	56, 57	opeq12d 4718	. . . . . 6 ⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ = ⟨(((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴), (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵)⟩)
59	58	eqeq2d 2805	. . . . 5 ⊢ (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ ↔ 𝑦 = ⟨(((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐴), (((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↾ 𝐵)⟩))
60	55, 59	syl5ibrcom 248	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) → 𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩))
61		ffn 6382	. . . . . . . 8 ⊢ (𝑥:(𝐴 ∪ 𝐵)⟶𝐶 → 𝑥 Fn (𝐴 ∪ 𝐵))
62		fnresdm 6336	. . . . . . . 8 ⊢ (𝑥 Fn (𝐴 ∪ 𝐵) → (𝑥 ↾ (𝐴 ∪ 𝐵)) = 𝑥)
63	7, 61, 62	3syl 18	. . . . . . 7 ⊢ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) → (𝑥 ↾ (𝐴 ∪ 𝐵)) = 𝑥)
64	63	ad2antrl 724	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → (𝑥 ↾ (𝐴 ∪ 𝐵)) = 𝑥)
65	64	eqcomd 2801	. . . . 5 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → 𝑥 = (𝑥 ↾ (𝐴 ∪ 𝐵)))
66		vex 3440	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
67	66	resex 5780	. . . . . . . . 9 ⊢ (𝑥 ↾ 𝐴) ∈ V
68	66	resex 5780	. . . . . . . . 9 ⊢ (𝑥 ↾ 𝐵) ∈ V
69	67, 68	op1std 7555	. . . . . . . 8 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → (1st ‘𝑦) = (𝑥 ↾ 𝐴))
70	67, 68	op2ndd 7556	. . . . . . . 8 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → (2nd ‘𝑦) = (𝑥 ↾ 𝐵))
71	69, 70	uneq12d 4061	. . . . . . 7 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → ((1st ‘𝑦) ∪ (2nd ‘𝑦)) = ((𝑥 ↾ 𝐴) ∪ (𝑥 ↾ 𝐵)))
72		resundi 5748	. . . . . . 7 ⊢ (𝑥 ↾ (𝐴 ∪ 𝐵)) = ((𝑥 ↾ 𝐴) ∪ (𝑥 ↾ 𝐵))
73	71, 72	syl6eqr 2849	. . . . . 6 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → ((1st ‘𝑦) ∪ (2nd ‘𝑦)) = (𝑥 ↾ (𝐴 ∪ 𝐵)))
74	73	eqeq2d 2805	. . . . 5 ⊢ (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↔ 𝑥 = (𝑥 ↾ (𝐴 ∪ 𝐵))))
75	65, 74	syl5ibrcom 248	. . . 4 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → (𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩ → 𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦))))
76	60, 75	impbid 213	. . 3 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) ∧ (𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))) → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↔ 𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩))
77	76	ex 413	. 2 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝑥 ∈ (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ∧ 𝑦 ∈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵))) → (𝑥 = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ↔ 𝑦 = ⟨(𝑥 ↾ 𝐴), (𝑥 ↾ 𝐵)⟩)))
78	2, 6, 23, 38, 77	en3d 8394	1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑𝑚 (𝐴 ∪ 𝐵)) ≈ ((𝐶 ↑𝑚 𝐴) × (𝐶 ↑𝑚 𝐵)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1522   ∈ wcel 2081  Vcvv 3437   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  ∅c0 4211  ⟨cop 4478   class class class wbr 4962   × cxp 5441   ↾ cres 5445   Fn wfn 6220  ⟶wf 6221  ‘cfv 6225  (class class class)co 7016  1^st c1st 7543  2^nd c2nd 7544   ↑_𝑚 cmap 8256   ≈ cen 8354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-ov 7019  df-oprab 7020  df-mpo 7021  df-1st 7545  df-2nd 7546  df-map 8258  df-en 8358

This theorem is referenced by:  map2xp  8534  mapdom2  8535  mapdjuen  9452  ackbij1lem5  9492  hashmap  13644  mpct  41004