 Home Intuitionistic Logic ExplorerTheorem List (p. 54 of 74) < 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

Theoremfconst3m 5301* Two ways to express a constant function. (Contributed by Jim Kingdon, 8-Jan-2019.)
(x x A → (𝐹:A⟶{B} ↔ (𝐹 Fn A A ⊆ (𝐹 “ {B}))))

Theoremfconst4m 5302* Two ways to express a constant function. (Contributed by NM, 8-Mar-2007.)
(x x A → (𝐹:A⟶{B} ↔ (𝐹 Fn A (𝐹 “ {B}) = A)))

Theoremresfunexg 5303 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 5304 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 5303. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
((𝐹 Fn A A B) → 𝐹 V)

Theoremfunex 5305 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 5304. (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 5306* 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 5307* 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 5308* 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 5309 If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.)
((𝐹:AB A 𝐶) → 𝐹 V)

Theoremeufnfv 5310* 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 5311 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 5312 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 5313 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 5314 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 5315* 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 5316* 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 5317* TODO: This is the same as issref 4630 (which has a much longer proof). Should we replace issref 4630 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 5318* Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014.)
B V       (x AB {yx A y = B})

Theoremabrexco 5319* 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 5320* 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 5321* 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 5322* 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 5323* 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 5322. (Contributed by Jim Kingdon, 10-Jan-2019.)
(𝐹 Fn A x A (𝐹x) = (𝐹A))

Theoremfuniunfvdmf 5324* The indexed union of a function's values is the union of its image under the index class. This version of funiunfvdm 5323 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 5325* 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 5326* Membership in the union of the range of a function. (Contributed by NM, 24-Sep-2006.)
(Fun 𝐹 → (A ran 𝐹x dom 𝐹 A (𝐹x)))

Theoremfnunirn 5327* 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 5328* 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 5329 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 5330* 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 5331* 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 5332 Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997.)
((𝐹:A1-1B (𝐶 A 𝐷 A)) → ((𝐹𝐶) = (𝐹𝐷) ↔ 𝐶 = 𝐷))

Theoremf1elima 5333 Membership in the image of a 1-1 map. (Contributed by Jeff Madsen, 2-Sep-2009.)
((𝐹:A1-1B 𝑋 A 𝑌A) → ((𝐹𝑋) (𝐹𝑌) ↔ 𝑋 𝑌))

Theoremf1imass 5334 Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.)
((𝐹:A1-1B (𝐶A 𝐷A)) → ((𝐹𝐶) ⊆ (𝐹𝐷) ↔ 𝐶𝐷))

Theoremf1imaeq 5335 Taking images under a one-to-one function preserves equality. (Contributed by Stefan O'Rear, 30-Oct-2014.)
((𝐹:A1-1B (𝐶A 𝐷A)) → ((𝐹𝐶) = (𝐹𝐷) ↔ 𝐶 = 𝐷))

Theoremf1imapss 5336 Taking images under a one-to-one function preserves proper subsets. (Contributed by Stefan O'Rear, 30-Oct-2014.)
((𝐹:A1-1B (𝐶A 𝐷A)) → ((𝐹𝐶) ⊊ (𝐹𝐷) ↔ 𝐶𝐷))

Theoremdff1o6 5337* 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 5338 The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
((𝐹:A1-1-ontoB 𝐶 A) → (𝐹‘(𝐹𝐶)) = 𝐶)

Theoremf1ocnvfv2 5339 The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
((𝐹:A1-1-ontoB 𝐶 B) → (𝐹‘(𝐹𝐶)) = 𝐶)

Theoremf1ocnvfv 5340 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 5341 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 5342 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 5343 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 5344 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 5345 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 5346* 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 5347* Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997.)
((𝐹x) = y → (φψ))       (𝐹:AontoB → (x A φy B ψ))

Theoremcocan1 5348 An injection is left-cancelable. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.)
((𝐹:B1-1𝐶 𝐻:AB 𝐾:AB) → ((𝐹𝐻) = (𝐹𝐾) ↔ 𝐻 = 𝐾))

Theoremcocan2 5349 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 5350 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 5351 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 5352 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 5353* 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       (φ𝐹 ⊆ (𝑅 × 𝑆))

Theoremfliftel 5354* Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       (φ → (𝐶𝐹𝐷x 𝑋 (𝐶 = A 𝐷 = B)))

Theoremfliftel1 5355* Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       ((φ x 𝑋) → A𝐹B)

Theoremfliftcnv 5356* Converse of the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨A, B⟩)    &   ((φ x 𝑋) → A 𝑅)    &   ((φ x 𝑋) → B 𝑆)       (φ𝐹 = ran (x 𝑋 ↦ ⟨B, A⟩))

Theoremfliftfun 5357* 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 5358* 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 5359* 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 5360* 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 5361* 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 5362 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐺 Isom 𝑅, 𝑆 (A, B)))

Theoremisoeq2 5363 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(𝑅 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑇, 𝑆 (A, B)))

Theoremisoeq3 5364 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(𝑆 = 𝑇 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑅, 𝑇 (A, B)))

Theoremisoeq4 5365 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(A = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, B)))

Theoremisoeq5 5366 Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
(B = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑅, 𝑆 (A, 𝐶)))

Theoremnfiso 5367 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 5368 An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
(𝐻 Isom 𝑅, 𝑆 (A, B) → 𝐻:A1-1-ontoB)

Theoremisorel 5369 An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
((𝐻 Isom 𝑅, 𝑆 (A, B) (𝐶 A 𝐷 A)) → (𝐶𝑅𝐷 ↔ (𝐻𝐶)𝑆(𝐻𝐷)))

Theoremisoresbr 5370* 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 5371 Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
( I ↾ A) Isom 𝑅, 𝑅 (A, A)

Theoremisocnv 5372 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 5373 Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
(𝐻 Isom 𝑅, 𝑆 (A, B) ↔ 𝐻 Isom 𝑅, 𝑆(A, B))

Theoremisores2 5374 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 5375 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 5376 Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
((𝐻 Isom 𝑅, 𝑆 (A, B) 𝐾A 𝑋 = (𝐻𝐾)) → (𝐻𝐾) Isom 𝑅, 𝑆 (𝐾, 𝑋))

Theoremisotr 5377 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 5378 Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
((𝐻 Isom 𝑅, 𝑆 (A, B) 𝐷 A) → (𝐻 “ (A ∩ (𝑅 “ {𝐷}))) = (B ∩ (𝑆 “ {(𝐻𝐷)})))

Theoremisoini2 5379 Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
𝐶 = (A ∩ (𝑅 “ {𝑋}))    &   𝐷 = (B ∩ (𝑆 “ {(𝐻𝑋)}))       ((𝐻 Isom 𝑅, 𝑆 (A, B) 𝑋 A) → (𝐻𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷))

Theoremisoselem 5380* Lemma for isose 5381. (Contributed by Mario Carneiro, 23-Jun-2015.)
(φ𝐻 Isom 𝑅, 𝑆 (A, B))    &   (φ → (𝐻x) V)       (φ → (𝑅 Se A𝑆 Se B))

Theoremisose 5381 An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.)
(𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑅 Se A𝑆 Se B))

Theoremisopolem 5382 Lemma for isopo 5383. (Contributed by Stefan O'Rear, 16-Nov-2014.)
(𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑆 Po B𝑅 Po A))

Theoremisopo 5383 An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
(𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑅 Po A𝑆 Po B))

Theoremisosolem 5384 Lemma for isoso 5385. (Contributed by Stefan O'Rear, 16-Nov-2014.)
(𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑆 Or B𝑅 Or A))

Theoremisoso 5385 An isomorphism preserves strict ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
(𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑅 Or A𝑆 Or B))

Theoremf1oiso 5386* Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.)
((𝐻:A1-1-ontoB 𝑆 = {⟨z, w⟩ ∣ x A y A ((z = (𝐻x) w = (𝐻y)) x𝑅y)}) → 𝐻 Isom 𝑅, 𝑆 (A, B))

Theoremf1oiso2 5387* Any one-to-one onto function determines an isomorphism with an induced relation 𝑆. (Contributed by Mario Carneiro, 9-Mar-2013.)
𝑆 = {⟨x, y⟩ ∣ ((x B y B) (𝐻x)𝑅(𝐻y))}       (𝐻:A1-1-ontoB𝐻 Isom 𝑅, 𝑆 (A, B))

2.6.9  Restricted iota (description binder)

Syntaxcrio 5388 Extend class notation with restricted description binder.
class (x A φ)

Definitiondf-riota 5389 Define restricted description binder. In case there is no unique x such that (x A φ) holds, it evaluates to the empty set. See also comments for df-iota 4790. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
(x A φ) = (℩x(x A φ))

Theoremriotaeqdv 5390* Formula-building deduction rule for iota. (Contributed by NM, 15-Sep-2011.)
(φA = B)       (φ → (x A ψ) = (x B ψ))

Theoremriotabidv 5391* Formula-building deduction rule for restricted iota. (Contributed by NM, 15-Sep-2011.)
(φ → (ψχ))       (φ → (x A ψ) = (x A χ))

Theoremriotaeqbidv 5392* Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
(φA = B)    &   (φ → (ψχ))       (φ → (x A ψ) = (x B χ))

Theoremriotav 5393 An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.)
(x V φ) = (℩xφ)

Theoremriotauni 5394 Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.)
(∃!x A φ → (x A φ) = {x Aφ})

Theoremnfriota1 5395* The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
x(x A φ)

Theoremnfriotadxy 5396* Deduction version of nfriota 5397. (Contributed by Jim Kingdon, 12-Jan-2019.)
yφ    &   (φ → Ⅎxψ)    &   (φxA)       (φx(y A ψ))

Theoremnfriota 5397* A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
xφ    &   xA       x(y A φ)

Theoremcbvriota 5398* Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
yφ    &   xψ    &   (x = y → (φψ))       (x A φ) = (y A ψ)

Theoremcbvriotav 5399* Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
(x = y → (φψ))       (x A φ) = (y A ψ)

Theoremcsbriotag 5400* Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.)
(A 𝑉A / x(y B φ) = (y B [A / x]φ))

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-7354
 Copyright terms: Public domain < Previous  Next >