HomeHome Intuitionistic Logic Explorer
Theorem List (p. 54 of 95)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 5301-5400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremfvsn 5301 The value of a singleton of an ordered pair is the second member. (Contributed by NM, 12-Aug-1994.)
A V    &   B V       ({⟨A, B⟩}‘A) = B
 
Theoremfvsng 5302 The value of a singleton of an ordered pair is the second member. (Contributed by NM, 26-Oct-2012.)
((A 𝑉 B 𝑊) → ({⟨A, B⟩}‘A) = B)
 
Theoremfvsnun1 5303 The value of a function with one of its ordered pairs replaced, at the replaced ordered pair. See also fvsnun2 5304. (Contributed by NM, 23-Sep-2007.)
A V    &   B V    &   𝐺 = ({⟨A, B⟩} ∪ (𝐹 ↾ (𝐶 ∖ {A})))       (𝐺A) = B
 
Theoremfvsnun2 5304 The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 5303. (Contributed by NM, 23-Sep-2007.)
A V    &   B V    &   𝐺 = ({⟨A, B⟩} ∪ (𝐹 ↾ (𝐶 ∖ {A})))       (𝐷 (𝐶 ∖ {A}) → (𝐺𝐷) = (𝐹𝐷))
 
Theoremfsnunf 5305 Adjoining a point to a function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
((𝐹:𝑆𝑇 (𝑋 𝑉 ¬ 𝑋 𝑆) 𝑌 𝑇) → (𝐹 ∪ {⟨𝑋, 𝑌⟩}):(𝑆 ∪ {𝑋})⟶𝑇)
 
Theoremfsnunfv 5306 Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.)
((𝑋 𝑉 𝑌 𝑊 ¬ 𝑋 dom 𝐹) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)
 
Theoremfsnunres 5307 Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.)
((𝐹 Fn 𝑆 ¬ 𝑋 𝑆) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ 𝑆) = 𝐹)
 
Theoremfvpr1 5308 The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
A V    &   𝐶 V       (AB → ({⟨A, 𝐶⟩, ⟨B, 𝐷⟩}‘A) = 𝐶)
 
Theoremfvpr2 5309 The value of a function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010.)
B V    &   𝐷 V       (AB → ({⟨A, 𝐶⟩, ⟨B, 𝐷⟩}‘B) = 𝐷)
 
Theoremfvpr1g 5310 The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
((A 𝑉 𝐶 𝑊 AB) → ({⟨A, 𝐶⟩, ⟨B, 𝐷⟩}‘A) = 𝐶)
 
Theoremfvpr2g 5311 The value of a function with a domain of (at most) two elements. (Contributed by Alexander van der Vekens, 3-Dec-2017.)
((B 𝑉 𝐷 𝑊 AB) → ({⟨A, 𝐶⟩, ⟨B, 𝐷⟩}‘B) = 𝐷)
 
Theoremfvtp1g 5312 The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
(((A 𝑉 𝐷 𝑊) (AB A𝐶)) → ({⟨A, 𝐷⟩, ⟨B, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘A) = 𝐷)
 
Theoremfvtp2g 5313 The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
(((B 𝑉 𝐸 𝑊) (AB B𝐶)) → ({⟨A, 𝐷⟩, ⟨B, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘B) = 𝐸)
 
Theoremfvtp3g 5314 The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017.)
(((𝐶 𝑉 𝐹 𝑊) (A𝐶 B𝐶)) → ({⟨A, 𝐷⟩, ⟨B, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹)
 
Theoremfvtp1 5315 The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
A V    &   𝐷 V       ((AB A𝐶) → ({⟨A, 𝐷⟩, ⟨B, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘A) = 𝐷)
 
Theoremfvtp2 5316 The second value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
B V    &   𝐸 V       ((AB B𝐶) → ({⟨A, 𝐷⟩, ⟨B, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘B) = 𝐸)
 
Theoremfvtp3 5317 The third value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011.)
𝐶 V    &   𝐹 V       ((A𝐶 B𝐶) → ({⟨A, 𝐷⟩, ⟨B, 𝐸⟩, ⟨𝐶, 𝐹⟩}‘𝐶) = 𝐹)
 
Theoremfvconst2g 5318 The value of a constant function. (Contributed by NM, 20-Aug-2005.)
((B 𝐷 𝐶 A) → ((A × {B})‘𝐶) = B)
 
Theoremfconst2g 5319 A constant function expressed as a cross product. (Contributed by NM, 27-Nov-2007.)
(B 𝐶 → (𝐹:A⟶{B} ↔ 𝐹 = (A × {B})))
 
Theoremfvconst2 5320 The value of a constant function. (Contributed by NM, 16-Apr-2005.)
B V       (𝐶 A → ((A × {B})‘𝐶) = B)
 
Theoremfconst2 5321 A constant function expressed as a cross product. (Contributed by NM, 20-Aug-1999.)
B V       (𝐹:A⟶{B} ↔ 𝐹 = (A × {B}))
 
Theoremfconstfvm 5322* A constant function expressed in terms of its functionality, domain, and value. See also fconst2 5321. (Contributed by Jim Kingdon, 8-Jan-2019.)
(y y A → (𝐹:A⟶{B} ↔ (𝐹 Fn A x A (𝐹x) = B)))
 
Theoremfconst3m 5323* Two ways to express a constant function. (Contributed by Jim Kingdon, 8-Jan-2019.)
(x x A → (𝐹:A⟶{B} ↔ (𝐹 Fn A A ⊆ (𝐹 “ {B}))))
 
Theoremfconst4m 5324* Two ways to express a constant function. (Contributed by NM, 8-Mar-2007.)
(x x A → (𝐹:A⟶{B} ↔ (𝐹 Fn A (𝐹 “ {B}) = A)))
 
Theoremresfunexg 5325 The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. (Contributed by NM, 7-Apr-1995.) (Revised by Mario Carneiro, 22-Jun-2013.)
((Fun A B 𝐶) → (AB) V)
 
Theoremfnex 5326 If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg 5325. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
((𝐹 Fn A A B) → 𝐹 V)
 
Theoremfunex 5327 If the domain of a function exists, so the function. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of fnex 5326. (Note: Any resemblance between F.U.N.E.X. and "Have You Any Eggs" is purely a coincidence originated by Swedish chefs.) (Contributed by NM, 11-Nov-1995.)
((Fun 𝐹 dom 𝐹 B) → 𝐹 V)
 
Theoremopabex 5328* Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996.)
A V    &   (x A∃*yφ)       {⟨x, y⟩ ∣ (x A φ)} V
 
Theoremmptexg 5329* If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
(A 𝑉 → (x AB) V)
 
Theoremmptex 5330* If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by NM, 22-Apr-2005.) (Revised by Mario Carneiro, 20-Dec-2013.)
A V       (x AB) V
 
Theoremfex 5331 If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.)
((𝐹:AB A 𝐶) → 𝐹 V)
 
Theoremeufnfv 5332* A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011.)
A V    &   B V       ∃!f(f Fn A x A (fx) = B)
 
Theoremfunfvima 5333 A function's value in a preimage belongs to the image. (Contributed by NM, 23-Sep-2003.)
((Fun 𝐹 B dom 𝐹) → (B A → (𝐹B) (𝐹A)))
 
Theoremfunfvima2 5334 A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997.)
((Fun 𝐹 A ⊆ dom 𝐹) → (B A → (𝐹B) (𝐹A)))
 
Theoremfunfvima3 5335 A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by NM, 23-Mar-2004.)
((Fun 𝐹 𝐹𝐺) → (A dom 𝐹 → (𝐹A) (𝐺 “ {A})))
 
Theoremfnfvima 5336 The function value of an operand in a set is contained in the image of that set, using the Fn abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015.)
((𝐹 Fn A 𝑆A 𝑋 𝑆) → (𝐹𝑋) (𝐹𝑆))
 
Theoremrexima 5337* Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.)
(x = (𝐹y) → (φψ))       ((𝐹 Fn A BA) → (x (𝐹B)φy B ψ))
 
Theoremralima 5338* Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015.)
(x = (𝐹y) → (φψ))       ((𝐹 Fn A BA) → (x (𝐹B)φy B ψ))
 
Theoremidref 5339* TODO: This is the same as issref 4650 (which has a much longer proof). Should we replace issref 4650 with this one? - NM 9-May-2016.

Two ways to state a relation is reflexive. (Adapted from Tarski.) (Contributed by FL, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) (Proof modification is discouraged.)

(( I ↾ A) ⊆ 𝑅x A x𝑅x)
 
Theoremelabrex 5340* Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014.)
B V       (x AB {yx A y = B})
 
Theoremabrexco 5341* Composition of two image maps 𝐶(y) and B(w). (Contributed by NM, 27-May-2013.)
B V    &   (y = B𝐶 = 𝐷)       {xy {zw A z = B}x = 𝐶} = {xw A x = 𝐷}
 
Theoremimaiun 5342* The image of an indexed union is the indexed union of the images. (Contributed by Mario Carneiro, 18-Jun-2014.)
(A x B 𝐶) = x B (A𝐶)
 
Theoremimauni 5343* The image of a union is the indexed union of the images. Theorem 3K(a) of [Enderton] p. 50. (Contributed by NM, 9-Aug-2004.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
(A B) = x B (Ax)
 
Theoremfniunfv 5344* The indexed union of a function's values is the union of its range. Compare Definition 5.4 of [Monk1] p. 50. (Contributed by NM, 27-Sep-2004.)
(𝐹 Fn A x A (𝐹x) = ran 𝐹)
 
Theoremfuniunfvdm 5345* The indexed union of a function's values is the union of its image under the index class. This theorem is a slight variation of fniunfv 5344. (Contributed by Jim Kingdon, 10-Jan-2019.)
(𝐹 Fn A x A (𝐹x) = (𝐹A))
 
Theoremfuniunfvdmf 5346* The indexed union of a function's values is the union of its image under the index class. This version of funiunfvdm 5345 uses a bound-variable hypothesis in place of a distinct variable condition. (Contributed by Jim Kingdon, 10-Jan-2019.)
x𝐹       (𝐹 Fn A x A (𝐹x) = (𝐹A))
 
Theoremeluniimadm 5347* Membership in the union of an image of a function. (Contributed by Jim Kingdon, 10-Jan-2019.)
(𝐹 Fn A → (B (𝐹A) ↔ x A B (𝐹x)))
 
Theoremelunirn 5348* Membership in the union of the range of a function. (Contributed by NM, 24-Sep-2006.)
(Fun 𝐹 → (A ran 𝐹x dom 𝐹 A (𝐹x)))
 
Theoremfnunirn 5349* Membership in a union of some function-defined family of sets. (Contributed by Stefan O'Rear, 30-Jan-2015.)
(𝐹 Fn 𝐼 → (A ran 𝐹x 𝐼 A (𝐹x)))
 
Theoremdff13 5350* A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 29-Oct-1996.)
(𝐹:A1-1B ↔ (𝐹:AB x A y A ((𝐹x) = (𝐹y) → x = y)))
 
Theoremf1veqaeq 5351 If the values of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
((𝐹:A1-1B (𝐶 A 𝐷 A)) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷))
 
Theoremdff13f 5352* A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 31-Jul-2003.)
x𝐹    &   y𝐹       (𝐹:A1-1B ↔ (𝐹:AB x A y A ((𝐹x) = (𝐹y) → x = y)))
 
Theoremf1mpt 5353* Express injection for a mapping operation. (Contributed by Mario Carneiro, 2-Jan-2017.)
𝐹 = (x A𝐶)    &   (x = y𝐶 = 𝐷)       (𝐹:A1-1B ↔ (x A 𝐶 B x A y A (𝐶 = 𝐷x = y)))
 
Theoremf1fveq 5354 Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997.)
((𝐹:A1-1B (𝐶 A 𝐷 A)) → ((𝐹𝐶) = (𝐹𝐷) ↔ 𝐶 = 𝐷))
 
Theoremf1elima 5355 Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.)
((𝐹:A1-1B 𝑋 A 𝑌A) → ((𝐹𝑋) (𝐹𝑌) ↔ 𝑋 𝑌))
 
Theoremf1imass 5356 Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.)
((𝐹:A1-1B (𝐶A 𝐷A)) → ((𝐹𝐶) ⊆ (𝐹𝐷) ↔ 𝐶𝐷))
 
Theoremf1imaeq 5357 Taking images under a one-to-one function preserves equality. (Contributed by Stefan O'Rear, 30-Oct-2014.)
((𝐹:A1-1B (𝐶A 𝐷A)) → ((𝐹𝐶) = (𝐹𝐷) ↔ 𝐶 = 𝐷))
 
Theoremf1imapss 5358 Taking images under a one-to-one function preserves proper subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.)
((𝐹:A1-1B (𝐶A 𝐷A)) → ((𝐹𝐶) ⊊ (𝐹𝐷) ↔ 𝐶𝐷))
 
Theoremdff1o6 5359* A one-to-one onto function in terms of function values. (Contributed by NM, 29-Mar-2008.)
(𝐹:A1-1-ontoB ↔ (𝐹 Fn A ran 𝐹 = B x A y A ((𝐹x) = (𝐹y) → x = y)))
 
Theoremf1ocnvfv1 5360 The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
((𝐹:A1-1-ontoB 𝐶 A) → (𝐹‘(𝐹𝐶)) = 𝐶)
 
Theoremf1ocnvfv2 5361 The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
((𝐹:A1-1-ontoB 𝐶 B) → (𝐹‘(𝐹𝐶)) = 𝐶)
 
Theoremf1ocnvfv 5362 Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.)
((𝐹:A1-1-ontoB 𝐶 A) → ((𝐹𝐶) = 𝐷 → (𝐹𝐷) = 𝐶))
 
Theoremf1ocnvfvb 5363 Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by NM, 20-May-2004.)
((𝐹:A1-1-ontoB 𝐶 A 𝐷 B) → ((𝐹𝐶) = 𝐷 ↔ (𝐹𝐷) = 𝐶))
 
Theoremf1ocnvdm 5364 The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.)
((𝐹:A1-1-ontoB 𝐶 B) → (𝐹𝐶) A)
 
Theoremf1ocnvfvrneq 5365 If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
((𝐹:A1-1B (𝐶 ran 𝐹 𝐷 ran 𝐹)) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷))
 
Theoremfcof1 5366 An application is injective if a retraction exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 11-Nov-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
((𝐹:AB (𝑅𝐹) = ( I ↾ A)) → 𝐹:A1-1B)
 
Theoremfcofo 5367 An application is surjective if a section exists. Proposition 8 of [BourbakiEns] p. E.II.18. (Contributed by FL, 17-Nov-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
((𝐹:AB 𝑆:BA (𝐹𝑆) = ( I ↾ B)) → 𝐹:AontoB)
 
Theoremcbvfo 5368* Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
((𝐹x) = y → (φψ))       (𝐹:AontoB → (x A φy B ψ))
 
Theoremcbvexfo 5369* Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.)
((𝐹x) = y → (φψ))       (𝐹:AontoB → (x A φy B ψ))
 
Theoremcocan1 5370 An injection is left-cancelable. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.)
((𝐹:B1-1𝐶 𝐻:AB 𝐾:AB) → ((𝐹𝐻) = (𝐹𝐾) ↔ 𝐻 = 𝐾))
 
Theoremcocan2 5371 A surjection is right-cancelable. (Contributed by FL, 21-Nov-2011.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
((𝐹:AontoB 𝐻 Fn B 𝐾 Fn B) → ((𝐻𝐹) = (𝐾𝐹) ↔ 𝐻 = 𝐾))
 
Theoremfcof1o 5372 Show that two functions are inverse to each other by computing their compositions. (Contributed by Mario Carneiro, 21-Mar-2015.)
(((𝐹:AB 𝐺:BA) ((𝐹𝐺) = ( I ↾ B) (𝐺𝐹) = ( I ↾ A))) → (𝐹:A1-1-ontoB 𝐹 = 𝐺))
 
Theoremfoeqcnvco 5373 Condition for function equality in terms of vanishing of the composition with the converse. EDITORIAL: Is there a relation-algebraic proof of this? (Contributed by Stefan O'Rear, 12-Feb-2015.)
((𝐹:AontoB 𝐺:AontoB) → (𝐹 = 𝐺 ↔ (𝐹𝐺) = ( I ↾ B)))
 
Theoremf1eqcocnv 5374 Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015.)
((𝐹:A1-1B 𝐺:A1-1B) → (𝐹 = 𝐺 ↔ (𝐹𝐺) = ( I ↾ A)))
 
Theoremfliftrel 5375* 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       (φ𝐹 ⊆ (𝑅 × 𝑆))
 
Theoremfliftel 5376* Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       (φ → (𝐶𝐹𝐷x 𝑋 (𝐶 = A 𝐷 = B)))
 
Theoremfliftel1 5377* Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       ((φ x 𝑋) → A𝐹B)
 
Theoremfliftcnv 5378* Converse of the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       (φ𝐹 = ran (x 𝑋 ↦ ⟨B, A⟩))
 
Theoremfliftfun 5379* The function 𝐹 is the unique function defined by 𝐹A = B, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)    &   (x = yA = 𝐶)    &   (x = yB = 𝐷)       (φ → (Fun 𝐹x 𝑋 y 𝑋 (A = 𝐶B = 𝐷)))
 
Theoremfliftfund 5380* The function 𝐹 is the unique function defined by 𝐹A = B, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)    &   (x = yA = 𝐶)    &   (x = yB = 𝐷)    &   ((φ (x 𝑋 y 𝑋 A = 𝐶)) → B = 𝐷)       (φ → Fun 𝐹)
 
Theoremfliftfuns 5381* The function 𝐹 is the unique function defined by 𝐹A = B, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       (φ → (Fun 𝐹y 𝑋 z 𝑋 (y / xA = z / xAy / xB = z / xB)))
 
Theoremfliftf 5382* The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       (φ → (Fun 𝐹𝐹:ran (x 𝑋A)⟶𝑆))
 
Theoremfliftval 5383* The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)    &   (x = 𝑌A = 𝐶)    &   (x = 𝑌B = 𝐷)    &   (φ → Fun 𝐹)       ((φ 𝑌 𝑋) → (𝐹𝐶) = 𝐷)
 
Theoremisoeq1 5384 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐺 Isom 𝑅, 𝑆 (A, B)))
 
Theoremisoeq2 5385 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(𝑅 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑇, 𝑆 (A, B)))
 
Theoremisoeq3 5386 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(𝑆 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑅, 𝑇 (A, B)))
 
Theoremisoeq4 5387 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(A = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, B)))
 
Theoremisoeq5 5388 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(B = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑅, 𝑆 (A, 𝐶)))
 
Theoremnfiso 5389 Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
x𝐻    &   x𝑅    &   x𝑆    &   xA    &   xB       x 𝐻 Isom 𝑅, 𝑆 (A, B)
 
Theoremisof1o 5390 An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
(𝐻 Isom 𝑅, 𝑆 (A, B) → 𝐻:A1-1-ontoB)
 
Theoremisorel 5391 An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
((𝐻 Isom 𝑅, 𝑆 (A, B) (𝐶 A 𝐷 A)) → (𝐶𝑅𝐷 ↔ (𝐻𝐶)𝑆(𝐻𝐷)))
 
Theoremisoresbr 5392* A consequence of isomorphism on two relations for a function's restriction. (Contributed by Jim Kingdon, 11-Jan-2019.)
((𝐹A) Isom 𝑅, 𝑆 (A, (𝐹A)) → x A y A (x𝑅y → (𝐹x)𝑆(𝐹y)))
 
Theoremisoid 5393 Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
( I ↾ A) Isom 𝑅, 𝑅 (A, A)
 
Theoremisocnv 5394 Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
(𝐻 Isom 𝑅, 𝑆 (A, B) → 𝐻 Isom 𝑆, 𝑅 (B, A))
 
Theoremisocnv2 5395 Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
(𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑅, 𝑆(A, B))
 
Theoremisores2 5396 An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
(𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑅, (𝑆 ∩ (B × B))(A, B))
 
Theoremisores1 5397 An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
(𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom (𝑅 ∩ (A × A)), 𝑆(A, B))
 
Theoremisores3 5398 Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
((𝐻 Isom 𝑅, 𝑆 (A, B) 𝐾A 𝑋 = (𝐻𝐾)) → (𝐻𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋))
 
Theoremisotr 5399 Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
((𝐻 Isom 𝑅, 𝑆 (A, B) 𝐺 Isom 𝑆, 𝑇 (B, 𝐶)) → (𝐺𝐻) Isom 𝑅, 𝑇 (A, 𝐶))
 
Theoremisoini 5400 Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
((𝐻 Isom 𝑅, 𝑆 (A, B) 𝐷 A) → (𝐻 “ (A ∩ (𝑅 “ {𝐷}))) = (B ∩ (𝑆 “ {(𝐻𝐷)})))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9427
  Copyright terms: Public domain < Previous  Next >