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 18190

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 2735	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
5		eqid 2735	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
6		eqid 2735	. . . 4 ⊢ (comp‘𝐶) = (comp‘𝐶)
7		eqid 2735	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
8		simpl 482	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐶 ∈ V)
9		simpr 484	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝐷 ∈ V)
10		eqidd 2736	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = (𝑋 × 𝑌))
11		eqidd 2736	. . . 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 2736	. . . 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 18189	. . 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 6890	. . . . 5 ⊢ 𝑋 ∈ V
15	3	fvexi 6890	. . . . 5 ⊢ 𝑌 ∈ V
16	14, 15	xpex 7747	. . . 4 ⊢ (𝑋 × 𝑌) ∈ V
17	16	a1i 11	. . 3 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) ∈ V)
18	13, 17	estrreslem1 18149	. 2 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = (Base‘𝑇))
19		base0 17233	. . 3 ⊢ ∅ = (Base‘∅)
20		fvprc 6868	. . . . . 6 ⊢ (¬ 𝐶 ∈ V → (Base‘𝐶) = ∅)
21	2, 20	eqtrid 2782	. . . . 5 ⊢ (¬ 𝐶 ∈ V → 𝑋 = ∅)
22		fvprc 6868	. . . . . 6 ⊢ (¬ 𝐷 ∈ V → (Base‘𝐷) = ∅)
23	3, 22	eqtrid 2782	. . . . 5 ⊢ (¬ 𝐷 ∈ V → 𝑌 = ∅)
24	21, 23	orim12i 908	. . . 4 ⊢ ((¬ 𝐶 ∈ V ∨ ¬ 𝐷 ∈ V) → (𝑋 = ∅ ∨ 𝑌 = ∅))
25		ianor 983	. . . 4 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) ↔ (¬ 𝐶 ∈ V ∨ ¬ 𝐷 ∈ V))
26		xpeq0 6149	. . . 4 ⊢ ((𝑋 × 𝑌) = ∅ ↔ (𝑋 = ∅ ∨ 𝑌 = ∅))
27	24, 25, 26	3imtr4i 292	. . 3 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝑋 × 𝑌) = ∅)
28		fnxpc 18188	. . . . . . 7 ⊢ ×_c Fn (V × V)
29		fndm 6641	. . . . . . 7 ⊢ ( ×_c Fn (V × V) → dom ×_c = (V × V))
30	28, 29	ax-mp 5	. . . . . 6 ⊢ dom ×_c = (V × V)
31	30	ndmov 7591	. . . . 5 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) → (𝐶 ×_c 𝐷) = ∅)
32	1, 31	eqtrid 2782	. . . 4 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) → 𝑇 = ∅)
33	32	fveq2d 6880	. . 3 ⊢ (¬ (𝐶 ∈ V ∧ 𝐷 ∈ V) → (Base‘𝑇) = (Base‘∅))
34	19, 27, 33	3eqtr4a 2796	. 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 1540 ∈ wcel 2108 Vcvv 3459 ∅c0 4308 ⟨cop 4607 × cxp 5652 dom cdm 5654 Fn wfn 6526 ‘cfv 6531 (class class class)co 7405 ∈ cmpo 7407 1^st c1st 7986 2^nd c2nd 7987 Basecbs 17228 Hom chom 17282 compcco 17283 ×_c cxpc 18180

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-er 8719 df-en 8960 df-dom 8961 df-sdom 8962 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12502 df-z 12589 df-dec 12709 df-slot 17201 df-ndx 17213 df-base 17229 df-hom 17295 df-cco 17296 df-xpc 18184

This theorem is referenced by: xpchomfval 18191 xpccofval 18194 xpchom2 18198 xpcco2 18199 xpccatid 18200 1stfval 18203 2ndfval 18206 1stfcl 18209 2ndfcl 18210 prfcl 18215 prf1st 18216 prf2nd 18217 1st2ndprf 18218 catcxpccl 18219 xpcpropd 18220 evlfcl 18234 curf1cl 18240 curf2cl 18243 curfcl 18244 uncf1 18248 uncf2 18249 uncfcurf 18251 diag11 18255 diag12 18256 diag2 18257 curf2ndf 18259 hofcl 18271 yonedalem21 18285 yonedalem22 18290 yonedalem3b 18291 yonedalem3 18292 yonedainv 18293 yonffthlem 18294 elxpcbasex1ALT 49166 elxpcbasex2ALT 49168 xpcfucbas 49169 dfswapf2 49178 swapf1a 49186 swapf1 49189 swapf2val 49190 swapf1f1o 49192 swapf2f1oa 49194 swapfida 49197 cofuswapf1 49205 cofuswapf2 49206

W3C validator