xpcbas

Description: Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017)

	Ref	Expression
Hypotheses	xpcbas.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
	xpcbas.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
	xpcbas.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
Assertion	xpcbas	⊢ ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		xpcbas.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
2		xpcbas.x	⊢ 𝑋 = ( Base ‘ 𝐶 )
3		xpcbas.y	⊢ 𝑌 = ( Base ‘ 𝐷 )
4		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
5		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
6		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
7		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
8		simpl	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝐶 ∈ V )
9		simpr	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝐷 ∈ V )
10		eqidd	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑋 × 𝑌 ) = ( 𝑋 × 𝑌 ) )
11		eqidd	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) = ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) )
12		eqidd	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑥 ∈ ( ( 𝑋 × 𝑌 ) × ( 𝑋 × 𝑌 ) ) , 𝑦 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) 𝑦 ) , 𝑓 ∈ ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( ( 𝑋 × 𝑌 ) × ( 𝑋 × 𝑌 ) ) , 𝑦 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) 𝑦 ) , 𝑓 ∈ ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) )
13	1 2 3 4 5 6 7 8 9 10 11 12	xpcval	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝑇 = { ⟨ ( Base ‘ ndx ) , ( 𝑋 × 𝑌 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( 𝑋 × 𝑌 ) × ( 𝑋 × 𝑌 ) ) , 𝑦 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) 𝑦 ) , 𝑓 ∈ ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } )
14	2	fvexi	⊢ 𝑋 ∈ V
15	3	fvexi	⊢ 𝑌 ∈ V
16	14 15	xpex	⊢ ( 𝑋 × 𝑌 ) ∈ V
17	16	a1i	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑋 × 𝑌 ) ∈ V )
18	13 17	estrreslem1	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 ) )
19		base0	⊢ ∅ = ( Base ‘ ∅ )
20		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( Base ‘ 𝐶 ) = ∅ )
21	2 20	syl5eq	⊢ ( ¬ 𝐶 ∈ V → 𝑋 = ∅ )
22		fvprc	⊢ ( ¬ 𝐷 ∈ V → ( Base ‘ 𝐷 ) = ∅ )
23	3 22	syl5eq	⊢ ( ¬ 𝐷 ∈ V → 𝑌 = ∅ )
24	21 23	orim12i	⊢ ( ( ¬ 𝐶 ∈ V ∨ ¬ 𝐷 ∈ V ) → ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) )
25		ianor	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ↔ ( ¬ 𝐶 ∈ V ∨ ¬ 𝐷 ∈ V ) )
26		xpeq0	⊢ ( ( 𝑋 × 𝑌 ) = ∅ ↔ ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) )
27	24 25 26	3imtr4i	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑋 × 𝑌 ) = ∅ )
28		fnxpc	⊢ ×_c Fn ( V × V )
29		fndm	⊢ ( ×_c Fn ( V × V ) → dom ×_c = ( V × V ) )
30	28 29	ax-mp	⊢ dom ×_c = ( V × V )
31	30	ndmov	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐶 ×_c 𝐷 ) = ∅ )
32	1 31	syl5eq	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝑇 = ∅ )
33	32	fveq2d	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( Base ‘ 𝑇 ) = ( Base ‘ ∅ ) )
34	19 27 33	3eqtr4a	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 ) )
35	18 34	pm2.61i	⊢ ( 𝑋 × 𝑌 ) = ( Base ‘ 𝑇 )

Metamath Proof Explorer

Theorem xpcbas

Proof