P. 71 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7001-7100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	suplubti 7001*	A supremum is the least upper bound. See also supclti 6999 and supubti 7000. (Contributed by Jim Kingdon, 24-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   =>    |- ( ph -> ( ( C e. A /\ C R sup ( B , A , R ) ) -> E. z e. B C R z ) )
Theorem	suplub2ti 7002*	Bidirectional form of suplubti 7001. (Contributed by Jim Kingdon, 17-Jan-2022.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   &    |- ( ph -> R Or A )   &    |- ( ph -> B C_ A )   =>    |- ( ( ph /\ C e. A ) -> ( C R sup ( B , A , R ) <-> E. z e. B C R z ) )
Theorem	supelti 7003*	Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. C ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )   &    |- ( ph -> C C_ A )   =>    |- ( ph -> sup ( B , A , R ) e. C )
Theorem	sup00 7004	The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.)
|- sup ( B , (/) , R ) = (/)
Theorem	supmaxti 7005*	The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jim Kingdon, 24-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> C e. A )   &    |- ( ph -> C e. B )   &    |- ( ( ph /\ y e. B ) -> -. C R y )   =>    |- ( ph -> sup ( B , A , R ) = C )
Theorem	supsnti 7006*	The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> B e. A )   =>    |- ( ph -> sup ( { B } , A , R ) = B )
Theorem	isotilem 7007*	Lemma for isoti 7008. (Contributed by Jim Kingdon, 26-Nov-2021.)
|- ( F Isom R , S ( A , B ) -> ( A. x e. B A. y e. B ( x = y <-> ( -. x S y /\ -. y S x ) ) -> A. u e. A A. v e. A ( u = v <-> ( -. u R v /\ -. v R u ) ) ) )
Theorem	isoti 7008*	An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.)
|- ( F Isom R , S ( A , B ) -> ( A. u e. A A. v e. A ( u = v <-> ( -. u R v /\ -. v R u ) ) <-> A. u e. B A. v e. B ( u = v <-> ( -. u S v /\ -. v S u ) ) ) )
Theorem	supisolem 7009*	Lemma for supisoti 7011. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> F Isom R , S ( A , B ) )   &    |- ( ph -> C C_ A )   =>    |- ( ( ph /\ D e. A ) -> ( ( A. y e. C -. D R y /\ A. y e. A ( y R D -> E. z e. C y R z ) ) <-> ( A. w e. ( F " C ) -. ( F ` D ) S w /\ A. w e. B ( w S ( F ` D ) -> E. v e. ( F " C ) w S v ) ) ) )
Theorem	supisoex 7010*	Lemma for supisoti 7011. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> F Isom R , S ( A , B ) )   &    |- ( ph -> C C_ A )   &    |- ( ph -> E. x e. A ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) )   =>    |- ( ph -> E. u e. B ( A. w e. ( F " C ) -. u S w /\ A. w e. B ( w S u -> E. v e. ( F " C ) w S v ) ) )
Theorem	supisoti 7011*	Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.)
|- ( ph -> F Isom R , S ( A , B ) )   &    |- ( ph -> C C_ A )   &    |- ( ph -> E. x e. A ( A. y e. C -. x R y /\ A. y e. A ( y R x -> E. z e. C y R z ) ) )   &    |- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   =>    |- ( ph -> sup ( ( F " C ) , B , S ) = ( F ` sup ( C , A , R ) ) )
Theorem	infeq1 7012	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( B = C -> inf ( B , A , R ) = inf ( C , A , R ) )
Theorem	infeq1d 7013	Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( ph -> B = C )   =>    |- ( ph -> inf ( B , A , R ) = inf ( C , A , R ) )
Theorem	infeq1i 7014	Equality inference for infimum. (Contributed by AV, 2-Sep-2020.)
|- B = C   =>    |- inf ( B , A , R ) = inf ( C , A , R )
Theorem	infeq2 7015	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( B = C -> inf ( A , B , R ) = inf ( A , C , R ) )
Theorem	infeq3 7016	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( R = S -> inf ( A , B , R ) = inf ( A , B , S ) )
Theorem	infeq123d 7017	Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( ph -> A = D )   &    |- ( ph -> B = E )   &    |- ( ph -> C = F )   =>    |- ( ph -> inf ( A , B , C ) = inf ( D , E , F ) )
Theorem	nfinf 7018	Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x R   =>    |- F/_ xinf ( A , B , R )
Theorem	cnvinfex 7019*	Two ways of expressing existence of an infimum (one in terms of converse). (Contributed by Jim Kingdon, 17-Dec-2021.)
|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )
Theorem	cnvti 7020*	If a relation satisfies a condition corresponding to tightness of an apartness generated by an order, so does its converse. (Contributed by Jim Kingdon, 17-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   =>    |- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u `' R v /\ -. v `' R u ) ) )
Theorem	eqinfti 7021*	Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   =>    |- ( ph -> ( ( C e. A /\ A. y e. B -. y R C /\ A. y e. A ( C R y -> E. z e. B z R y ) ) -> inf ( B , A , R ) = C ) )
Theorem	eqinftid 7022*	Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> C e. A )   &    |- ( ( ph /\ y e. B ) -> -. y R C )   &    |- ( ( ph /\ ( y e. A /\ C R y ) ) -> E. z e. B z R y )   =>    |- ( ph -> inf ( B , A , R ) = C )
Theorem	infvalti 7023*	Alternate expression for the infimum. (Contributed by Jim Kingdon, 17-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> inf ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )
Theorem	infclti 7024*	An infimum belongs to its base class (closure law). See also inflbti 7025 and infglbti 7026. (Contributed by Jim Kingdon, 17-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> inf ( B , A , R ) e. A )
Theorem	inflbti 7025*	An infimum is a lower bound. See also infclti 7024 and infglbti 7026. (Contributed by Jim Kingdon, 18-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> ( C e. B -> -. C Rinf ( B , A , R ) ) )
Theorem	infglbti 7026*	An infimum is the greatest lower bound. See also infclti 7024 and inflbti 7025. (Contributed by Jim Kingdon, 18-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> ( ( C e. A /\ inf ( B , A , R ) R C ) -> E. z e. B z R C ) )
Theorem	infnlbti 7027*	A lower bound is not greater than the infimum. (Contributed by Jim Kingdon, 18-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> ( ( C e. A /\ A. z e. B -. z R C ) -> -. inf ( B , A , R ) R C ) )
Theorem	infminti 7028*	The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by Jim Kingdon, 18-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> C e. A )   &    |- ( ph -> C e. B )   &    |- ( ( ph /\ y e. B ) -> -. y R C )   =>    |- ( ph -> inf ( B , A , R ) = C )
Theorem	infmoti 7029*	Any class B has at most one infimum in A (where R is interpreted as 'less than'). (Contributed by Jim Kingdon, 18-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   =>    |- ( ph -> E* x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
Theorem	infeuti 7030*	An infimum is unique. (Contributed by Jim Kingdon, 19-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )   =>    |- ( ph -> E! x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
Theorem	infsnti 7031*	The infimum of a singleton. (Contributed by Jim Kingdon, 19-Dec-2021.)
|- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   &    |- ( ph -> B e. A )   =>    |- ( ph -> inf ( { B } , A , R ) = B )
Theorem	inf00 7032	The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.)
|- inf ( B , (/) , R ) = (/)
Theorem	infisoti 7033*	Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.)
|- ( ph -> F Isom R , S ( A , B ) )   &    |- ( ph -> C C_ A )   &    |- ( ph -> E. x e. A ( A. y e. C -. y R x /\ A. y e. A ( x R y -> E. z e. C z R y ) ) )   &    |- ( ( ph /\ ( u e. A /\ v e. A ) ) -> ( u = v <-> ( -. u R v /\ -. v R u ) ) )   =>    |- ( ph -> inf ( ( F " C ) , B , S ) = ( F ` inf ( C , A , R ) ) )
Theorem	supex2g 7034	Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. C -> sup ( B , A , R ) e. _V )
Theorem	infex2g 7035	Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.)
|- ( A e. C -> inf ( B , A , R ) e. _V )
2.6.35  Ordinal isomorphism
Theorem	ordiso2 7036	Generalize ordiso 7037 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A = B )
Theorem	ordiso 7037*	Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009.) (Proof shortened by Mario Carneiro, 24-Jun-2015.)
|- ( ( A e. On /\ B e. On ) -> ( A = B <-> E. f f Isom _E , _E ( A , B ) ) )
2.6.36  Disjoint union
2.6.36.1  Disjoint union
Syntax	cdju 7038	Extend class notation to include disjoint union of two classes.
class ( A ⊔ B )
Definition	df-dju 7039	Disjoint union of two classes. This is a way of creating a class which contains elements corresponding to each element of A or B, tagging each one with whether it came from A or B. (Contributed by Jim Kingdon, 20-Jun-2022.)
|- ( A ⊔ B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
Theorem	djueq12 7040	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- ( ( A = B /\ C = D ) -> ( A ⊔ C ) = ( B ⊔ D ) )
Theorem	djueq1 7041	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- ( A = B -> ( A ⊔ C ) = ( B ⊔ C ) )
Theorem	djueq2 7042	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- ( A = B -> ( C ⊔ A ) = ( C ⊔ B ) )
Theorem	nfdju 7043	Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A ⊔ B )
Theorem	djuex 7044	The disjoint union of sets is a set. See also the more precise djuss 7071. (Contributed by AV, 28-Jun-2022.)
|- ( ( A e. V /\ B e. W ) -> ( A ⊔ B ) e. _V )
Theorem	djuexb 7045	The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023.)
|- ( ( A e. _V /\ B e. _V ) <-> ( A ⊔ B ) e. _V )
2.6.36.2  Left and right injections of a disjoint union In this section, we define the left and right injections of a disjoint union and prove their main properties. These injections are restrictions of the "template" functions inl and inr, which appear in most applications in the form (inl |` A ) and (inr |` B ).
Syntax	cinl 7046	Extend class notation to include left injection of a disjoint union.
class inl
Syntax	cinr 7047	Extend class notation to include right injection of a disjoint union.
class inr
Definition	df-inl 7048	Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.)
|- inl = ( x e. _V |-> <. (/) , x >. )
Definition	df-inr 7049	Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.)
|- inr = ( x e. _V |-> <. 1o , x >. )
Theorem	djulclr 7050	Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.)
|- ( C e. A -> ( (inl |` A ) ` C ) e. ( A ⊔ B ) )
Theorem	djurclr 7051	Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.)
|- ( C e. B -> ( (inr |` B ) ` C ) e. ( A ⊔ B ) )
Theorem	djulcl 7052	Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
|- ( C e. A -> (inl ` C ) e. ( A ⊔ B ) )
Theorem	djurcl 7053	Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
|- ( C e. B -> (inr ` C ) e. ( A ⊔ B ) )
Theorem	djuf1olem 7054*	Lemma for djulf1o 7059 and djurf1o 7060. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.)
|- X e. _V   &    |- F = ( x e. A |-> <. X , x >. )   =>    |- F : A -1-1-onto-> ( { X } X. A )
Theorem	djuf1olemr 7055*	Lemma for djulf1or 7057 and djurf1or 7058. For a version of this lemma with F defined on A and no restriction in the conclusion, see djuf1olem 7054. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.)
|- X e. _V   &    |- F = ( x e. _V |-> <. X , x >. )   =>    |- ( F |` A ) : A -1-1-onto-> ( { X } X. A )
Theorem	djulclb 7056	Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.)
|- ( C e. V -> ( C e. A <-> (inl ` C ) e. ( A ⊔ B ) ) )
Theorem	djulf1or 7057	The left injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.)
|- (inl |` A ) : A -1-1-onto-> ( { (/) } X. A )
Theorem	djurf1or 7058	The right injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.)
|- (inr |` A ) : A -1-1-onto-> ( { 1o } X. A )
Theorem	djulf1o 7059	The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.)
|- inl : _V -1-1-onto-> ( { (/) } X. _V )
Theorem	djurf1o 7060	The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.)
|- inr : _V -1-1-onto-> ( { 1o } X. _V )
Theorem	inresflem 7061*	Lemma for inlresf1 7062 and inrresf1 7063. (Contributed by BJ, 4-Jul-2022.)
|- F : A -1-1-onto-> ( { X } X. A )   &    |- ( x e. A -> ( F ` x ) e. B )   =>    |- F : A -1-1-> B
Theorem	inlresf1 7062	The left injection restricted to the left class of a disjoint union is an injective function from the left class into the disjoint union. (Contributed by AV, 28-Jun-2022.)
|- (inl |` A ) : A -1-1-> ( A ⊔ B )
Theorem	inrresf1 7063	The right injection restricted to the right class of a disjoint union is an injective function from the right class into the disjoint union. (Contributed by AV, 28-Jun-2022.)
|- (inr |` B ) : B -1-1-> ( A ⊔ B )
Theorem	djuinr 7064	The ranges of any left and right injections are disjoint. Remark: the extra generality offered by the two restrictions makes the theorem more readily usable (e.g., by djudom 7094 and djufun 7105) while the simpler statement |- ( ran inl i^i ran inr ) = (/) is easily recovered from it by substituting _V for both A and B as done in casefun 7086). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.)
|- ( ran (inl |` A ) i^i ran (inr |` B ) ) = (/)
Theorem	djuin 7065	The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.)
|- ( (inl " A ) i^i (inr " B ) ) = (/)
Theorem	inl11 7066	Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> ( (inl ` A ) = (inl ` B ) <-> A = B ) )
Theorem	djuunr 7067	The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 6-Jul-2022.)
|- ( ran (inl |` A ) u. ran (inr |` B ) ) = ( A ⊔ B )
Theorem	djuun 7068	The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.)
|- ( (inl " A ) u. (inr " B ) ) = ( A ⊔ B )
Theorem	eldju 7069*	Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.)
|- ( C e. ( A ⊔ B ) <-> ( E. x e. A C = ( (inl |` A ) ` x ) \/ E. x e. B C = ( (inr |` B ) ` x ) ) )
Theorem	djur 7070*	A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) Upgrade implication to biconditional and shorten proof. (Revised by BJ, 14-Jul-2023.)
|- ( C e. ( A ⊔ B ) <-> ( E. x e. A C = (inl ` x ) \/ E. x e. B C = (inr ` x ) ) )
2.6.36.3  Universal property of the disjoint union
Theorem	djuss 7071	A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.)
|- ( A ⊔ B ) C_ ( { (/) , 1o } X. ( A u. B ) )
Theorem	eldju1st 7072	The first component of an element of a disjoint union is either (/) or 1o. (Contributed by AV, 26-Jun-2022.)
|- ( X e. ( A ⊔ B ) -> ( ( 1st ` X ) = (/) \/ ( 1st ` X ) = 1o ) )
Theorem	eldju2ndl 7073	The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.)
|- ( ( X e. ( A ⊔ B ) /\ ( 1st ` X ) = (/) ) -> ( 2nd ` X ) e. A )
Theorem	eldju2ndr 7074	The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022.)
|- ( ( X e. ( A ⊔ B ) /\ ( 1st ` X ) =/= (/) ) -> ( 2nd ` X ) e. B )
Theorem	1stinl 7075	The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.)
|- ( X e. V -> ( 1st ` (inl ` X ) ) = (/) )
Theorem	2ndinl 7076	The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.)
|- ( X e. V -> ( 2nd ` (inl ` X ) ) = X )
Theorem	1stinr 7077	The first component of the value of a right injection is 1o. (Contributed by AV, 27-Jun-2022.)
|- ( X e. V -> ( 1st ` (inr ` X ) ) = 1o )
Theorem	2ndinr 7078	The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.)
|- ( X e. V -> ( 2nd ` (inr ` X ) ) = X )
Theorem	djune 7079	Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.)
|- ( ( A e. V /\ B e. W ) -> (inl ` A ) =/= (inr ` B ) )
Theorem	updjudhf 7080*	The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.)
|- ( ph -> F : A --> C )   &    |- ( ph -> G : B --> C )   &    |- H = ( x e. ( A ⊔ B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) )   =>    |- ( ph -> H : ( A ⊔ B ) --> C )
Theorem	updjudhcoinlf 7081*	The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.)
|- ( ph -> F : A --> C )   &    |- ( ph -> G : B --> C )   &    |- H = ( x e. ( A ⊔ B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) )   =>    |- ( ph -> ( H o. (inl |` A ) ) = F )
Theorem	updjudhcoinrg 7082*	The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.)
|- ( ph -> F : A --> C )   &    |- ( ph -> G : B --> C )   &    |- H = ( x e. ( A ⊔ B ) |-> if ( ( 1st ` x ) = (/) , ( F ` ( 2nd ` x ) ) , ( G ` ( 2nd ` x ) ) ) )   =>    |- ( ph -> ( H o. (inr |` B ) ) = G )
Theorem	updjud 7083*	Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.)
|- ( ph -> F : A --> C )   &    |- ( ph -> G : B --> C )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> E! h ( h : ( A ⊔ B ) --> C /\ ( h o. (inl |` A ) ) = F /\ ( h o. (inr |` B ) ) = G ) )
Syntax	cdjucase 7084	Syntax for the "case" construction.
class case ( R , S )
Definition	df-case 7085	The "case" construction: if F : A --> X and G : B --> X are functions, then case ( F , G ) : ( A ⊔ B ) --> X is the natural function obtained by a definition by cases, hence the name. It is the unique function whose existence is asserted by the universal property of disjoint unions updjud 7083. The definition is adapted to make sense also for binary relations (where the universal property also holds). (Contributed by MC and BJ, 10-Jul-2022.)
|- case ( R , S ) = ( ( R o. `'inl ) u. ( S o. `'inr ) )
Theorem	casefun 7086	The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> Fun F )   &    |- ( ph -> Fun G )   =>    |- ( ph -> Fun case ( F , G ) )
Theorem	casedm 7087	The domain of the "case" construction is the disjoint union of the domains. TODO (although less important): |- ran case ( F , G ) = ( ran F u. ran G ). (Contributed by BJ, 10-Jul-2022.)
|- dom case ( F , G ) = ( dom F ⊔ dom G )
Theorem	caserel 7088	The "case" construction of two relations is a relation, with bounds on its domain and codomain. Typically, the "case" construction is used when both relations have a common codomain. (Contributed by BJ, 10-Jul-2022.)
|- case ( R , S ) C_ ( ( dom R ⊔ dom S ) X. ( ran R u. ran S ) )
Theorem	casef 7089	The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> F : A --> X )   &    |- ( ph -> G : B --> X )   =>    |- ( ph -> case ( F , G ) : ( A ⊔ B ) --> X )
Theorem	caseinj 7090	The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> Fun `' R )   &    |- ( ph -> Fun `' S )   &    |- ( ph -> ( ran R i^i ran S ) = (/) )   =>    |- ( ph -> Fun `'case ( R , S ) )
Theorem	casef1 7091	The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> F : A -1-1-> X )   &    |- ( ph -> G : B -1-1-> X )   &    |- ( ph -> ( ran F i^i ran G ) = (/) )   =>    |- ( ph -> case ( F , G ) : ( A ⊔ B ) -1-1-> X )
Theorem	caseinl 7092	Applying the "case" construction to a left injection. (Contributed by Jim Kingdon, 15-Mar-2023.)
|- ( ph -> F Fn B )   &    |- ( ph -> Fun G )   &    |- ( ph -> A e. B )   =>    |- ( ph -> (case ( F , G ) ` (inl ` A ) ) = ( F ` A ) )
Theorem	caseinr 7093	Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.)
|- ( ph -> Fun F )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. B )   =>    |- ( ph -> (case ( F , G ) ` (inr ` A ) ) = ( G ` A ) )
2.6.36.4  Dominance and equinumerosity properties of disjoint union
Theorem	djudom 7094	Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.)
|- ( ( A ~<_ B /\ C ~<_ D ) -> ( A ⊔ C ) ~<_ ( B ⊔ D ) )
Theorem	omp1eomlem 7095*	Lemma for omp1eom 7096. (Contributed by Jim Kingdon, 11-Jul-2023.)
|- F = ( x e. om |-> if ( x = (/) , (inr ` x ) , (inl ` U. x ) ) )   &    |- S = ( x e. om |-> suc x )   &    |- G = case ( S , ( _I |` 1o ) )   =>    |- F : om -1-1-onto-> ( om ⊔ 1o )
Theorem	omp1eom 7096	Adding one to om. (Contributed by Jim Kingdon, 10-Jul-2023.)
|- ( om ⊔ 1o ) ~~ om
Theorem	endjusym 7097	Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> ( A ⊔ B ) ~~ ( B ⊔ A ) )
Theorem	eninl 7098	Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( A e. V -> (inl " A ) ~~ A )
Theorem	eninr 7099	Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( A e. V -> (inr " A ) ~~ A )
Theorem	difinfsnlem 7100*	Lemma for difinfsn 7101. The case where we need to swap B and (inr ` (/) ) in building the mapping G. (Contributed by Jim Kingdon, 9-Aug-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> B e. A )   &    |- ( ph -> F : ( om ⊔ 1o ) -1-1-> A )   &    |- ( ph -> ( F ` (inr ` (/) ) ) =/= B )   &    |- G = ( n e. om |-> if ( ( F ` (inl ` n ) ) = B , ( F ` (inr ` (/) ) ) , ( F ` (inl ` n ) ) ) )   =>    |- ( ph -> G : om -1-1-> ( A \ { B } ) )