cnmpt2t

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmpt21.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt21.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
	cnmpt21.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) )
	cnmpt2t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝑀 ) )
Assertion	cnmpt2t	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn ( 𝐿 ×_t 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmpt21.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		cnmpt21.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) )
4		cnmpt2t.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝑀 ) )
5		fveq2	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
6		df-ov	⊢ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
7	5 6	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) = ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) )
8		fveq2	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
9		df-ov	⊢ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) = ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
10	8 9	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) = ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) )
11	7 10	opeq12d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ = ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩ )
12	11	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑢 ∈ 𝑋 , 𝑣 ∈ 𝑌 ↦ ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩ )
13		nfcv	⊢ Ⅎ 𝑥 𝑢
14		nfmpo1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
15		nfcv	⊢ Ⅎ 𝑥 𝑣
16	13 14 15	nfov	⊢ Ⅎ 𝑥 ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 )
17		nfmpo1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
18	13 17 15	nfov	⊢ Ⅎ 𝑥 ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 )
19	16 18	nfop	⊢ Ⅎ 𝑥 ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩
20		nfcv	⊢ Ⅎ 𝑦 𝑢
21		nfmpo2	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
22		nfcv	⊢ Ⅎ 𝑦 𝑣
23	20 21 22	nfov	⊢ Ⅎ 𝑦 ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 )
24		nfmpo2	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
25	20 24 22	nfov	⊢ Ⅎ 𝑦 ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 )
26	23 25	nfop	⊢ Ⅎ 𝑦 ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩
27		nfcv	⊢ Ⅎ 𝑢 ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩
28		nfcv	⊢ Ⅎ 𝑣 ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩
29		oveq12	⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) = ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) )
30		oveq12	⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) = ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) )
31	29 30	opeq12d	⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) → ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩ = ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ )
32	19 26 27 28 31	cbvmpo	⊢ ( 𝑢 ∈ 𝑋 , 𝑣 ∈ 𝑌 ↦ ⟨ ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑣 ) , ( 𝑢 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑣 ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ )
33	12 32	eqtri	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ )
34		txtopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
35	1 2 34	syl2anc	⊢ ( 𝜑 → ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
36		toponuni	⊢ ( ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝐽 ×_t 𝐾 ) )
37		mpteq1	⊢ ( ( 𝑋 × 𝑌 ) = ∪ ( 𝐽 ×_t 𝐾 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑧 ∈ ∪ ( 𝐽 ×_t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) )
38	35 36 37	3syl	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑧 ∈ ∪ ( 𝐽 ×_t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) )
39		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
40		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
41		cntop2	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) → 𝐿 ∈ Top )
42	3 41	syl	⊢ ( 𝜑 → 𝐿 ∈ Top )
43		toptopon2	⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
44	42 43	sylib	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
45		cnf2	⊢ ( ( ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
46	35 44 3 45	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
47		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
48	47	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
49	46 48	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 )
50		rsp2	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ∪ 𝐿 ) )
51	49 50	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ∪ 𝐿 ) )
52	51	3impib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ∪ 𝐿 )
53	47	ovmpt4g	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐴 ∈ ∪ 𝐿 ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) = 𝐴 )
54	39 40 52 53	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) = 𝐴 )
55		cntop2	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝑀 ) → 𝑀 ∈ Top )
56	4 55	syl	⊢ ( 𝜑 → 𝑀 ∈ Top )
57		toptopon2	⊢ ( 𝑀 ∈ Top ↔ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
58	56 57	sylib	⊢ ( 𝜑 → 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) )
59		cnf2	⊢ ( ( ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝑀 ∈ ( TopOn ‘ ∪ 𝑀 ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝑀 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑀 )
60	35 58 4 59	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑀 )
61		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
62	61	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝑀 )
63	60 62	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 )
64		rsp2	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ∪ 𝑀 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ∪ 𝑀 ) )
65	63 64	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ∪ 𝑀 ) )
66	65	3impib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ∪ 𝑀 )
67	61	ovmpt4g	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝐵 ∈ ∪ 𝑀 ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) = 𝐵 )
68	39 40 66 67	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) = 𝐵 )
69	54 68	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
70	69	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) 𝑦 ) , ( 𝑥 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) 𝑦 ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
71	33 38 70	3eqtr3a	⊢ ( 𝜑 → ( 𝑧 ∈ ∪ ( 𝐽 ×_t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) )
72		eqid	⊢ ∪ ( 𝐽 ×_t 𝐾 ) = ∪ ( 𝐽 ×_t 𝐾 )
73		eqid	⊢ ( 𝑧 ∈ ∪ ( 𝐽 ×_t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) = ( 𝑧 ∈ ∪ ( 𝐽 ×_t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ )
74	72 73	txcnmpt	⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝑀 ) ) → ( 𝑧 ∈ ∪ ( 𝐽 ×_t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn ( 𝐿 ×_t 𝑀 ) ) )
75	3 4 74	syl2anc	⊢ ( 𝜑 → ( 𝑧 ∈ ∪ ( 𝐽 ×_t 𝐾 ) ↦ ⟨ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ‘ 𝑧 ) , ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ‘ 𝑧 ) ⟩ ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn ( 𝐿 ×_t 𝑀 ) ) )
76	71 75	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn ( 𝐿 ×_t 𝑀 ) ) )

Metamath Proof Explorer

Theorem cnmpt2t

Proof