# Metamath Proof Explorer

## Theorem 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 ) → ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝐶 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd𝑣 ) ) ) ) = ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝐶 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd𝑣 ) ) ) ) )
12 eqidd ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑥 ∈ ( ( 𝑋 × 𝑌 ) × ( 𝑋 × 𝑌 ) ) , 𝑦 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝐶 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd𝑣 ) ) ) ) 𝑦 ) , 𝑓 ∈ ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝐶 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd𝑣 ) ) ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝐶 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝐷 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( ( 𝑋 × 𝑌 ) × ( 𝑋 × 𝑌 ) ) , 𝑦 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝐶 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd𝑣 ) ) ) ) 𝑦 ) , 𝑓 ∈ ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝐶 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd𝑣 ) ) ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝐶 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝐷 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 xpcval ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝑇 = { ⟨ ( Base ‘ ndx ) , ( 𝑋 × 𝑌 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝐶 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd𝑣 ) ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( 𝑋 × 𝑌 ) × ( 𝑋 × 𝑌 ) ) , 𝑦 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑔 ∈ ( ( 2nd𝑥 ) ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝐶 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd𝑣 ) ) ) ) 𝑦 ) , 𝑓 ∈ ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) , 𝑣 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1st𝑢 ) ( Hom ‘ 𝐶 ) ( 1st𝑣 ) ) × ( ( 2nd𝑢 ) ( Hom ‘ 𝐷 ) ( 2nd𝑣 ) ) ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 1st𝑔 ) ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 1st ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝐶 ) ( 1st𝑦 ) ) ( 1st𝑓 ) ) , ( ( 2nd𝑔 ) ( ⟨ ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 2nd𝑥 ) ) ⟩ ( comp ‘ 𝐷 ) ( 2nd𝑦 ) ) ( 2nd𝑓 ) ) ⟩ ) ) ⟩ } )
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 ‘ 𝑇 )