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

Proof

Step	Hyp	Ref	Expression
1		ovexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∈ V )
2		ovexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐶 ↑_m 𝐴 ) ∈ V )
3		ovexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐶 ↑_m 𝐵 ) ∈ V )
4	2 3	xpexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ∈ V )
5		elmapi	⊢ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) → 𝑥 : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )
6		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
7		fssres	⊢ ( ( 𝑥 : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ∧ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ) → ( 𝑥 ↾ 𝐴 ) : 𝐴 ⟶ 𝐶 )
8	5 6 7	sylancl	⊢ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) → ( 𝑥 ↾ 𝐴 ) : 𝐴 ⟶ 𝐶 )
9		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
10		fssres	⊢ ( ( 𝑥 : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ∧ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ) → ( 𝑥 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 )
11	5 9 10	sylancl	⊢ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) → ( 𝑥 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 )
12	8 11	jca	⊢ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) → ( ( 𝑥 ↾ 𝐴 ) : 𝐴 ⟶ 𝐶 ∧ ( 𝑥 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ) )
13		opelxp	⊢ ( ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ↔ ( ( 𝑥 ↾ 𝐴 ) ∈ ( 𝐶 ↑_m 𝐴 ) ∧ ( 𝑥 ↾ 𝐵 ) ∈ ( 𝐶 ↑_m 𝐵 ) ) )
14		simpl3	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐶 ∈ 𝑋 )
15		simpl1	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ∈ 𝑉 )
16	14 15	elmapd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝑥 ↾ 𝐴 ) ∈ ( 𝐶 ↑_m 𝐴 ) ↔ ( 𝑥 ↾ 𝐴 ) : 𝐴 ⟶ 𝐶 ) )
17		simpl2	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ∈ 𝑊 )
18	14 17	elmapd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝑥 ↾ 𝐵 ) ∈ ( 𝐶 ↑_m 𝐵 ) ↔ ( 𝑥 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ) )
19	16 18	anbi12d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( ( 𝑥 ↾ 𝐴 ) ∈ ( 𝐶 ↑_m 𝐴 ) ∧ ( 𝑥 ↾ 𝐵 ) ∈ ( 𝐶 ↑_m 𝐵 ) ) ↔ ( ( 𝑥 ↾ 𝐴 ) : 𝐴 ⟶ 𝐶 ∧ ( 𝑥 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ) ) )
20	13 19	bitrid	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ↔ ( ( 𝑥 ↾ 𝐴 ) : 𝐴 ⟶ 𝐶 ∧ ( 𝑥 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ) ) )
21	12 20	syl5ibr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) → ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) )
22		xp1st	⊢ ( 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) → ( 1^st ‘ 𝑦 ) ∈ ( 𝐶 ↑_m 𝐴 ) )
23	22	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) → ( 1^st ‘ 𝑦 ) ∈ ( 𝐶 ↑_m 𝐴 ) )
24		elmapi	⊢ ( ( 1^st ‘ 𝑦 ) ∈ ( 𝐶 ↑_m 𝐴 ) → ( 1^st ‘ 𝑦 ) : 𝐴 ⟶ 𝐶 )
25	23 24	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) → ( 1^st ‘ 𝑦 ) : 𝐴 ⟶ 𝐶 )
26		xp2nd	⊢ ( 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) → ( 2^nd ‘ 𝑦 ) ∈ ( 𝐶 ↑_m 𝐵 ) )
27	26	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ ( 𝐶 ↑_m 𝐵 ) )
28		elmapi	⊢ ( ( 2^nd ‘ 𝑦 ) ∈ ( 𝐶 ↑_m 𝐵 ) → ( 2^nd ‘ 𝑦 ) : 𝐵 ⟶ 𝐶 )
29	27 28	syl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) → ( 2^nd ‘ 𝑦 ) : 𝐵 ⟶ 𝐶 )
30		simplr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
31	25 29 30	fun2d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) → ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 )
32	31	ex	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) → ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ) )
33		unexg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
34	15 17 33	syl2anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
35	14 34	elmapd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ↔ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ) )
36	32 35	sylibrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) → ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ) )
37		1st2nd2	⊢ ( 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
38	37	ad2antll	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
39	25	adantrl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 1^st ‘ 𝑦 ) : 𝐴 ⟶ 𝐶 )
40	29	adantrl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 2^nd ‘ 𝑦 ) : 𝐵 ⟶ 𝐶 )
41		res0	⊢ ( ( 1^st ‘ 𝑦 ) ↾ ∅ ) = ∅
42		res0	⊢ ( ( 2^nd ‘ 𝑦 ) ↾ ∅ ) = ∅
43	41 42	eqtr4i	⊢ ( ( 1^st ‘ 𝑦 ) ↾ ∅ ) = ( ( 2^nd ‘ 𝑦 ) ↾ ∅ )
44		simplr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
45	44	reseq2d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( 1^st ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 1^st ‘ 𝑦 ) ↾ ∅ ) )
46	44	reseq2d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( 2^nd ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑦 ) ↾ ∅ ) )
47	43 45 46	3eqtr4a	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( 1^st ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) )
48		fresaunres1	⊢ ( ( ( 1^st ‘ 𝑦 ) : 𝐴 ⟶ 𝐶 ∧ ( 2^nd ‘ 𝑦 ) : 𝐵 ⟶ 𝐶 ∧ ( ( 1^st ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) = ( 1^st ‘ 𝑦 ) )
49	39 40 47 48	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) = ( 1^st ‘ 𝑦 ) )
50		fresaunres2	⊢ ( ( ( 1^st ‘ 𝑦 ) : 𝐴 ⟶ 𝐶 ∧ ( 2^nd ‘ 𝑦 ) : 𝐵 ⟶ 𝐶 ∧ ( ( 1^st ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) = ( 2^nd ‘ 𝑦 ) )
51	39 40 47 50	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) = ( 2^nd ‘ 𝑦 ) )
52	49 51	opeq12d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ⟨ ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) , ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) ⟩ = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
53	38 52	eqtr4d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → 𝑦 = ⟨ ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) , ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) ⟩ )
54		reseq1	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → ( 𝑥 ↾ 𝐴 ) = ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) )
55		reseq1	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → ( 𝑥 ↾ 𝐵 ) = ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) )
56	54 55	opeq12d	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ = ⟨ ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) , ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) ⟩ )
57	56	eqeq2d	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ↔ 𝑦 = ⟨ ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) , ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) ⟩ ) )
58	53 57	syl5ibrcom	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ) )
59		ffn	⊢ ( 𝑥 : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 → 𝑥 Fn ( 𝐴 ∪ 𝐵 ) )
60		fnresdm	⊢ ( 𝑥 Fn ( 𝐴 ∪ 𝐵 ) → ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) = 𝑥 )
61	5 59 60	3syl	⊢ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) → ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) = 𝑥 )
62	61	ad2antrl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) = 𝑥 )
63	62	eqcomd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → 𝑥 = ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) )
64		vex	⊢ 𝑥 ∈ V
65	64	resex	⊢ ( 𝑥 ↾ 𝐴 ) ∈ V
66	64	resex	⊢ ( 𝑥 ↾ 𝐵 ) ∈ V
67	65 66	op1std	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( 1^st ‘ 𝑦 ) = ( 𝑥 ↾ 𝐴 ) )
68	65 66	op2ndd	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( 2^nd ‘ 𝑦 ) = ( 𝑥 ↾ 𝐵 ) )
69	67 68	uneq12d	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) = ( ( 𝑥 ↾ 𝐴 ) ∪ ( 𝑥 ↾ 𝐵 ) ) )
70		resundi	⊢ ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑥 ↾ 𝐴 ) ∪ ( 𝑥 ↾ 𝐵 ) )
71	69 70	eqtr4di	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) = ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) )
72	71	eqeq2d	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↔ 𝑥 = ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) ) )
73	63 72	syl5ibrcom	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ) )
74	58 73	impbid	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↔ 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ) )
75	74	ex	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↔ 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ) ) )
76	1 4 21 36 75	en3d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ≈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) )

Metamath Proof Explorer

Theorem mapunen

Proof