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

axmp 
⊢ 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 ‘ 𝑇 ) 