P. 73 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7201-7300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	infeq1 7201	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( B = C -> inf ( B , A , R ) = inf ( C , A , R ) )
Theorem	infeq1d 7202	Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( ph -> B = C )   =>    |- ( ph -> inf ( B , A , R ) = inf ( C , A , R ) )
Theorem	infeq1i 7203	Equality inference for infimum. (Contributed by AV, 2-Sep-2020.)
|- B = C   =>    |- inf ( B , A , R ) = inf ( C , A , R )
Theorem	infeq2 7204	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( B = C -> inf ( A , B , R ) = inf ( A , C , R ) )
Theorem	infeq3 7205	Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.)
|- ( R = S -> inf ( A , B , R ) = inf ( A , B , S ) )
Theorem	infeq123d 7206	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 7207	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 7208*	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 7209*	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 7210*	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 7211*	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 7212*	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 7213*	An infimum belongs to its base class (closure law). See also inflbti 7214 and infglbti 7215. (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 7214*	An infimum is a lower bound. See also infclti 7213 and infglbti 7215. (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 7215*	An infimum is the greatest lower bound. See also infclti 7213 and inflbti 7214. (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 7216*	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 7217*	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 7218*	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 7219*	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 7220*	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 7221	The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.)
|- inf ( B , (/) , R ) = (/)
Theorem	infisoti 7222*	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 7223	Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. C -> sup ( B , A , R ) e. _V )
Theorem	infex2g 7224	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 7225	Generalize ordiso 7226 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A = B )
Theorem	ordiso 7226*	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 7227	Extend class notation to include disjoint union of two classes.
class ( A ⊔ B )
Definition	df-dju 7228	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 7229	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- ( ( A = B /\ C = D ) -> ( A ⊔ C ) = ( B ⊔ D ) )
Theorem	djueq1 7230	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- ( A = B -> ( A ⊔ C ) = ( B ⊔ C ) )
Theorem	djueq2 7231	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
|- ( A = B -> ( C ⊔ A ) = ( C ⊔ B ) )
Theorem	nfdju 7232	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 7233	The disjoint union of sets is a set. See also the more precise djuss 7260. (Contributed by AV, 28-Jun-2022.)
|- ( ( A e. V /\ B e. W ) -> ( A ⊔ B ) e. _V )
Theorem	djuexb 7234	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 7235	Extend class notation to include left injection of a disjoint union.
class inl
Syntax	cinr 7236	Extend class notation to include right injection of a disjoint union.
class inr
Definition	df-inl 7237	Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.)
|- inl = ( x e. _V |-> <. (/) , x >. )
Definition	df-inr 7238	Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.)
|- inr = ( x e. _V |-> <. 1o , x >. )
Theorem	djulclr 7239	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 7240	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 7241	Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
|- ( C e. A -> (inl ` C ) e. ( A ⊔ B ) )
Theorem	djurcl 7242	Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
|- ( C e. B -> (inr ` C ) e. ( A ⊔ B ) )
Theorem	djuf1olem 7243*	Lemma for djulf1o 7248 and djurf1o 7249. (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 7244*	Lemma for djulf1or 7246 and djurf1or 7247. For a version of this lemma with F defined on A and no restriction in the conclusion, see djuf1olem 7243. (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 7245	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 7246	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 7247	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 7248	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 7249	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 7250*	Lemma for inlresf1 7251 and inrresf1 7252. (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 7251	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 7252	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 7253	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 7283 and djufun 7294) 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 7275). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.)
|- ( ran (inl |` A ) i^i ran (inr |` B ) ) = (/)
Theorem	djuin 7254	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 7255	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 7256	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 7257	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 7258*	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 7259*	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 7260	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 7261	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 7262	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 7263	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 7264	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 7265	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 7266	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 7267	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 7268	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 7269*	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 7270*	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 7271*	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 7272*	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 7273	Syntax for the "case" construction.
class case ( R , S )
Definition	df-case 7274	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 7272. 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 7275	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 7276	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 7277	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 7278	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 7279	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 7280	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 7281	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 7282	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 7283	Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.)
|- ( ( A ~<_ B /\ C ~<_ D ) -> ( A ⊔ C ) ~<_ ( B ⊔ D ) )
Theorem	omp1eomlem 7284*	Lemma for omp1eom 7285. (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 7285	Adding one to om. (Contributed by Jim Kingdon, 10-Jul-2023.)
|- ( om ⊔ 1o ) ~~ om
Theorem	endjusym 7286	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 7287	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 7288	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 7289*	Lemma for difinfsn 7290. 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 } ) )
Theorem	difinfsn 7290*	An infinite set minus one element is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.)
|- ( ( A. x e. A A. y e. A DECID x = y /\ om ~<_ A /\ B e. A ) -> om ~<_ ( A \ { B } ) )
Theorem	difinfinf 7291*	An infinite set minus a finite subset is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.)
|- ( ( ( A. x e. A A. y e. A DECID x = y /\ om ~<_ A ) /\ ( B C_ A /\ B e. Fin ) ) -> om ~<_ ( A \ B ) )
2.6.36.5  Older definition temporarily kept for comparison, to be deleted
Syntax	cdjud 7292	Syntax for the domain-disjoint-union of two relations.
class ( R ⊔d S )
Definition	df-djud 7293	The "domain-disjoint-union" of two relations: if R C_ ( A X. X ) and S C_ ( B X. X ) are two binary relations, then ( R ⊔d S ) is the binary relation from ( A ⊔ B ) to X having the universal property of disjoint unions (see updjud 7272 in the case of functions). Remark: the restrictions to dom R (resp. dom S) are not necessary since extra stuff would be thrown away in the post-composition with R (resp. S), as in df-case 7274, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.)
|- ( R ⊔d S ) = ( ( R o. `' (inl |` dom R ) ) u. ( S o. `' (inr |` dom S ) ) )
Theorem	djufun 7294	The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.)
|- ( ph -> Fun F )   &    |- ( ph -> Fun G )   =>    |- ( ph -> Fun ( F ⊔d G ) )
Theorem	djudm 7295	The domain of the "domain-disjoint-union" is the disjoint union of the domains. Remark: its range is the (standard) union of the ranges. (Contributed by BJ, 10-Jul-2022.)
|- dom ( F ⊔d G ) = ( dom F ⊔ dom G )
Theorem	djuinj 7296	The "domain-disjoint-union" 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 `' ( R ⊔d S ) )
2.6.36.6  Countable sets
Theorem	0ct 7297	The empty set is countable. Remark of [BauerSwan], p. 14:3 which also has the definition of countable used here. (Contributed by Jim Kingdon, 13-Mar-2023.)
|- E. f f : om -onto-> ( (/) ⊔ 1o )
Theorem	ctmlemr 7298*	Lemma for ctm 7299. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.)
|- ( E. x x e. A -> ( E. f f : om -onto-> A -> E. f f : om -onto-> ( A ⊔ 1o ) ) )
Theorem	ctm 7299*	Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.)
|- ( E. x x e. A -> ( E. f f : om -onto-> ( A ⊔ 1o ) <-> E. f f : om -onto-> A ) )
Theorem	ctssdclemn0 7300*	Lemma for ctssdc 7303. The -. (/) e. S case. (Contributed by Jim Kingdon, 16-Aug-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ph -> -. (/) e. S )   =>    |- ( ph -> E. g g : om -onto-> ( A ⊔ 1o ) )