 Home Intuitionistic Logic ExplorerTheorem 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 ∩ (𝑆 “ {(𝐻𝐷)})))

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 >