xpcbas - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xpcbas		Structured version Visualization version GIF version

Theorem xpcbas 18101

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

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

**Assertion**
Ref	Expression
xpcbas	⊢ (𝑋 × 𝑌) = (Base‘𝑇)

Proof of Theorem xpcbas Dummy variables 𝑓 𝑔 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpcbas.t	. . . 4 ⊢ 𝑇 = (𝐶 ×_c 𝐷)
2		xpcbas.x	. . . 4 ⊢ 𝑋 = (Base‘𝐶)
3		xpcbas.y	. . . 4 ⊢ 𝑌 = (Base‘𝐷)
4		eqid 2736	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
5		eqid 2736	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
6		eqid 2736	. . . 4 ⊢ (comp‘𝐶) = (comp‘𝐶)
7		eqid 2736	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
8		simpl 482	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐶 ∈ V)
9		simpr 484	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐷 ∈ V)
10		eqidd 2737	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = (𝑋 × 𝑌))
11		eqidd 2737	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1^st ‘𝑢)(Hom ‘𝐶)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝐷)(2^nd ‘𝑣)))) = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ (((1^st ‘𝑢)(Hom ‘𝐶)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝐷)(2^nd ‘𝑣)))))
12		eqidd 2737	. . . 4 ⊢ ((𝐶 ∈ 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 18100	. . 3 ⊢ ((𝐶 ∈ 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 6848	. . . . 5 ⊢ 𝑋 ∈ V
15	3	fvexi 6848	. . . . 5 ⊢ 𝑌 ∈ V
16	14, 15	xpex 7698	. . . 4 ⊢ (𝑋 × 𝑌) ∈ V
17	16	a1i 11	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) ∈ V)
18	13, 17	estrreslem1 18060	. 2 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = (Base‘𝑇))
19		base0 17141	. . 3 ⊢ ∅ = (Base‘∅)
20		fvprc 6826	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → (Base‘𝐶) = ∅)
21	2, 20	eqtrid 2783	. . . . 5 ⊢ (¬ 𝐶 ∈ V → 𝑋 = ∅)
22		fvprc 6826	. . . . . 6 ⊢ (¬ 𝐷 ∈ V → (Base‘𝐷) = ∅)
23	3, 22	eqtrid 2783	. . . . 5 ⊢ (¬ 𝐷 ∈ V → 𝑌 = ∅)
24	21, 23	orim12i 908	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∨ ¬ 𝐷 ∈ V) → (𝑋 = ∅ ∨ 𝑌 = ∅))
25		ianor 983	. . . 4 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) ↔ (¬ 𝐶 ∈ V ∨ ¬ 𝐷 ∈ V))
26		xpeq0 6118	. . . 4 ⊢ ((𝑋 × 𝑌) = ∅ ↔ (𝑋 = ∅ ∨ 𝑌 = ∅))
27	24, 25, 26	3imtr4i 292	. . 3 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = ∅)
28		fnxpc 18099	. . . . . . 7 ⊢ ×_c Fn (V × V)
29		fndm 6595	. . . . . . 7 ⊢ ( ×_c Fn (V × V) → dom ×_c = (V × V))
30	28, 29	ax-mp 5	. . . . . 6 ⊢ dom ×_c = (V × V)
31	30	ndmov 7542	. . . . 5 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝐶 ×_c 𝐷) = ∅)
32	1, 31	eqtrid 2783	. . . 4 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = ∅)
33	32	fveq2d 6838	. . 3 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) → (Base‘𝑇) = (Base‘∅))
34	19, 27, 33	3eqtr4a 2797	. 2 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = (Base‘𝑇))
35	18, 34	pm2.61i 182	1 ⊢ (𝑋 × 𝑌) = (Base‘𝑇)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2113 Vcvv 3440 ∅c0 4285 ⟨cop 4586 × cxp 5622 dom cdm 5624 Fn wfn 6487 ‘cfv 6492 (class class class)co 7358 ∈ cmpo 7360 1^st c1st 7931 2^nd c2nd 7932 Basecbs 17136 Hom chom 17188 compcco 17189 ×_c cxpc 18091

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-er 8635 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-slot 17109 df-ndx 17121 df-base 17137 df-hom 17201 df-cco 17202 df-xpc 18095

This theorem is referenced by: xpchomfval 18102 xpccofval 18105 xpchom2 18109 xpcco2 18110 xpccatid 18111 1stfval 18114 2ndfval 18117 1stfcl 18120 2ndfcl 18121 prfcl 18126 prf1st 18127 prf2nd 18128 1st2ndprf 18129 catcxpccl 18130 xpcpropd 18131 evlfcl 18145 curf1cl 18151 curf2cl 18154 curfcl 18155 uncf1 18159 uncf2 18160 uncfcurf 18162 diag11 18166 diag12 18167 diag2 18168 curf2ndf 18170 hofcl 18182 yonedalem21 18196 yonedalem22 18201 yonedalem3b 18202 yonedalem3 18203 yonedainv 18204 yonffthlem 18205 elxpcbasex1ALT 49490 elxpcbasex2ALT 49492 xpcfucbas 49493 dfswapf2 49502 swapf1a 49510 swapf1 49513 swapf2val 49514 swapf1f1o 49516 swapf2f1oa 49518 swapfida 49521 oppc1stf 49529 oppc2ndf 49530 cofuswapf1 49535 cofuswapf2 49536

W3C validator