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

Metamath Proof Explorer

Theorem mapunen

Proof