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	imbitrrid	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑥 ∈ ( 𝐶 ↑_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	15 17	unexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
34	14 33	elmapd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ↔ ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 ) )
35	32 34	sylibrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) → ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ) )
36		1st2nd2	⊢ ( 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
37	36	ad2antll	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
38	25	adantrl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 1^st ‘ 𝑦 ) : 𝐴 ⟶ 𝐶 )
39	29	adantrl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 2^nd ‘ 𝑦 ) : 𝐵 ⟶ 𝐶 )
40		res0	⊢ ( ( 1^st ‘ 𝑦 ) ↾ ∅ ) = ∅
41		res0	⊢ ( ( 2^nd ‘ 𝑦 ) ↾ ∅ ) = ∅
42	40 41	eqtr4i	⊢ ( ( 1^st ‘ 𝑦 ) ↾ ∅ ) = ( ( 2^nd ‘ 𝑦 ) ↾ ∅ )
43		simplr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
44	43	reseq2d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( 1^st ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 1^st ‘ 𝑦 ) ↾ ∅ ) )
45	43	reseq2d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( 2^nd ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑦 ) ↾ ∅ ) )
46	42 44 45	3eqtr4a	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( 1^st ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) )
47		fresaunres1	⊢ ( ( ( 1^st ‘ 𝑦 ) : 𝐴 ⟶ 𝐶 ∧ ( 2^nd ‘ 𝑦 ) : 𝐵 ⟶ 𝐶 ∧ ( ( 1^st ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) = ( 1^st ‘ 𝑦 ) )
48	38 39 46 47	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) = ( 1^st ‘ 𝑦 ) )
49		fresaunres2	⊢ ( ( ( 1^st ‘ 𝑦 ) : 𝐴 ⟶ 𝐶 ∧ ( 2^nd ‘ 𝑦 ) : 𝐵 ⟶ 𝐶 ∧ ( ( 1^st ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) = ( ( 2^nd ‘ 𝑦 ) ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) = ( 2^nd ‘ 𝑦 ) )
50	38 39 46 49	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) = ( 2^nd ‘ 𝑦 ) )
51	48 50	opeq12d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ⟨ ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) , ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) ⟩ = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
52	37 51	eqtr4d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → 𝑦 = ⟨ ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) , ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) ⟩ )
53		reseq1	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → ( 𝑥 ↾ 𝐴 ) = ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) )
54		reseq1	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → ( 𝑥 ↾ 𝐵 ) = ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) )
55	53 54	opeq12d	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ = ⟨ ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) , ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) ⟩ )
56	55	eqeq2d	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ↔ 𝑦 = ⟨ ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐴 ) , ( ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↾ 𝐵 ) ⟩ ) )
57	52 56	syl5ibrcom	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) → 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ) )
58		ffn	⊢ ( 𝑥 : ( 𝐴 ∪ 𝐵 ) ⟶ 𝐶 → 𝑥 Fn ( 𝐴 ∪ 𝐵 ) )
59		fnresdm	⊢ ( 𝑥 Fn ( 𝐴 ∪ 𝐵 ) → ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) = 𝑥 )
60	5 58 59	3syl	⊢ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) → ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) = 𝑥 )
61	60	ad2antrl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) = 𝑥 )
62	61	eqcomd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → 𝑥 = ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) )
63		vex	⊢ 𝑥 ∈ V
64	63	resex	⊢ ( 𝑥 ↾ 𝐴 ) ∈ V
65	63	resex	⊢ ( 𝑥 ↾ 𝐵 ) ∈ V
66	64 65	op1std	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( 1^st ‘ 𝑦 ) = ( 𝑥 ↾ 𝐴 ) )
67	64 65	op2ndd	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( 2^nd ‘ 𝑦 ) = ( 𝑥 ↾ 𝐵 ) )
68	66 67	uneq12d	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) = ( ( 𝑥 ↾ 𝐴 ) ∪ ( 𝑥 ↾ 𝐵 ) ) )
69		resundi	⊢ ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑥 ↾ 𝐴 ) ∪ ( 𝑥 ↾ 𝐵 ) )
70	68 69	eqtr4di	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) = ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) )
71	70	eqeq2d	⊢ ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↔ 𝑥 = ( 𝑥 ↾ ( 𝐴 ∪ 𝐵 ) ) ) )
72	62 71	syl5ibrcom	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ → 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ) )
73	57 72	impbid	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↔ 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ) )
74	73	ex	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝑥 ∈ ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ∧ 𝑦 ∈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ∪ ( 2^nd ‘ 𝑦 ) ) ↔ 𝑦 = ⟨ ( 𝑥 ↾ 𝐴 ) , ( 𝑥 ↾ 𝐵 ) ⟩ ) ) )
75	1 4 21 35 74	en3d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐶 ↑_m ( 𝐴 ∪ 𝐵 ) ) ≈ ( ( 𝐶 ↑_m 𝐴 ) × ( 𝐶 ↑_m 𝐵 ) ) )

Metamath Proof Explorer

Theorem mapunen

Proof