brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  ga-pair

---

Theorem ga-pair 179

Description: A universal property of coproducts: given two arrows in Loj, there is an arrow from the coproduct of their sources to the coproduct of their targets. (Contributed by la korvo, 14-Jul-2025.)

Hypotheses

Ref	Expression
ga-pair.0	⊢ ganai broda gi brode
ga-pair.1	⊢ ganai brodi gi brodo

Assertion

Ref	Expression
ga-pair	⊢ ganai ga broda gi brodi gi ga brode gi brodo

---

Proof of Theorem ga-pair

Step	Hyp	Ref	Expression
1		ga-pair.0	. . 3 ⊢ ganai broda gi brode
2	1	ga-lid 177	. 2 ⊢ ganai broda gi ga brode gi brodo
3		ga-pair.1	. . 3 ⊢ ganai brodi gi brodo
4	3	ga-rid 178	. 2 ⊢ ganai brodi gi ga brode gi brodo
5	2, 4	ga-sum 167	1 ⊢ ganai ga broda gi brodi gi ga brode gi brodo

Colors of variables: sumti selbri bridi

Syntax hints:   ga bga 160

This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 48  ax-ge-re 49  ax-ge-in 50

This theorem depends on definitions:  df-go 83  df-ga 161

This theorem is referenced by:  ga-pairl  180  ga-pairr  181

Copyright terms: Public domain

W3C validator