 Home Intuitionistic Logic ExplorerTheorem List (p. 62 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 - 6101-6200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremqsss 6101 A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
(φ𝑅 Er A)       (φ → (A / 𝑅) ⊆ 𝒫 A)

Theoremuniqs2 6102 The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.)
(φ𝑅 Er A)    &   (φ𝑅 𝑉)       (φ (A / 𝑅) = A)

Theoremsnec 6103 The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
A V       {[A]𝑅} = ({A} / 𝑅)

Theoremecqs 6104 Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
𝑅 V       [A]𝑅 = ({A} / 𝑅)

Theoremecid 6105 A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
A V       [A] E = A

Theoremecidg 6106 A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.)
(A 𝑉 → [A] E = A)

Theoremqsid 6107 A set is equal to its quotient set mod converse epsilon. (Note: converse epsilon is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
(A / E ) = A

Theoremectocld 6108* Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
𝑆 = (B / 𝑅)    &   ([x]𝑅 = A → (φψ))    &   ((χ x B) → φ)       ((χ A 𝑆) → ψ)

Theoremectocl 6109* Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
𝑆 = (B / 𝑅)    &   ([x]𝑅 = A → (φψ))    &   (x Bφ)       (A 𝑆ψ)

Theoremelqsn0m 6110* An element of a quotient set is inhabited. (Contributed by Jim Kingdon, 21-Aug-2019.)
((dom 𝑅 = A B (A / 𝑅)) → x x B)

Theoremelqsn0 6111 A quotient set doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.)
((dom 𝑅 = A B (A / 𝑅)) → B ≠ ∅)

Theoremecelqsdm 6112 Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.)
((dom 𝑅 = A [B]𝑅 (A / 𝑅)) → B A)

Theoremxpiderm 6113* A square Cartesian product is an equivalence relation (in general it's not a poset). (Contributed by Jim Kingdon, 22-Aug-2019.)
(x x A → (A × A) Er A)

Theoremiinerm 6114* The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
((y y A x A 𝑅 Er B) → x A 𝑅 Er B)

Theoremriinerm 6115* The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
((y y A x A 𝑅 Er B) → ((B × B) ∩ x A 𝑅) Er B)

Theoremerinxp 6116 A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
(φ𝑅 Er A)    &   (φBA)       (φ → (𝑅 ∩ (B × B)) Er B)

Theoremecinxp 6117 Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.)
(((𝑅A) ⊆ A B A) → [B]𝑅 = [B](𝑅 ∩ (A × A)))

Theoremqsinxp 6118 Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
((𝑅A) ⊆ A → (A / 𝑅) = (A / (𝑅 ∩ (A × A))))

Theoremqsel 6119 If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.)
((𝑅 Er 𝑋 B (A / 𝑅) 𝐶 B) → B = [𝐶]𝑅)

Theoremqliftlem 6120* 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨[x]𝑅, A⟩)    &   ((φ x 𝑋) → A 𝑌)    &   (φ𝑅 Er 𝑋)    &   (φ𝑋 V)       ((φ x 𝑋) → [x]𝑅 (𝑋 / 𝑅))

Theoremqliftrel 6121* 𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨[x]𝑅, A⟩)    &   ((φ x 𝑋) → A 𝑌)    &   (φ𝑅 Er 𝑋)    &   (φ𝑋 V)       (φ𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌))

Theoremqliftel 6122* Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨[x]𝑅, A⟩)    &   ((φ x 𝑋) → A 𝑌)    &   (φ𝑅 Er 𝑋)    &   (φ𝑋 V)       (φ → ([𝐶]𝑅𝐹𝐷x 𝑋 (𝐶𝑅x 𝐷 = A)))

Theoremqliftel1 6123* Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨[x]𝑅, A⟩)    &   ((φ x 𝑋) → A 𝑌)    &   (φ𝑅 Er 𝑋)    &   (φ𝑋 V)       ((φ x 𝑋) → [x]𝑅𝐹A)

Theoremqliftfun 6124* The function 𝐹 is the unique function defined by 𝐹‘[x] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨[x]𝑅, A⟩)    &   ((φ x 𝑋) → A 𝑌)    &   (φ𝑅 Er 𝑋)    &   (φ𝑋 V)    &   (x = yA = B)       (φ → (Fun 𝐹xy(x𝑅yA = B)))

Theoremqliftfund 6125* The function 𝐹 is the unique function defined by 𝐹‘[x] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨[x]𝑅, A⟩)    &   ((φ x 𝑋) → A 𝑌)    &   (φ𝑅 Er 𝑋)    &   (φ𝑋 V)    &   (x = yA = B)    &   ((φ x𝑅y) → A = B)       (φ → Fun 𝐹)

Theoremqliftfuns 6126* The function 𝐹 is the unique function defined by 𝐹‘[x] = A, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨[x]𝑅, A⟩)    &   ((φ x 𝑋) → A 𝑌)    &   (φ𝑅 Er 𝑋)    &   (φ𝑋 V)       (φ → (Fun 𝐹yz(y𝑅zy / xA = z / xA)))

Theoremqliftf 6127* The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨[x]𝑅, A⟩)    &   ((φ x 𝑋) → A 𝑌)    &   (φ𝑅 Er 𝑋)    &   (φ𝑋 V)       (φ → (Fun 𝐹𝐹:(𝑋 / 𝑅)⟶𝑌))

Theoremqliftval 6128* The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.)
𝐹 = ran (x 𝑋 ↦ ⟨[x]𝑅, A⟩)    &   ((φ x 𝑋) → A 𝑌)    &   (φ𝑅 Er 𝑋)    &   (φ𝑋 V)    &   (x = 𝐶A = B)    &   (φ → Fun 𝐹)       ((φ 𝐶 𝑋) → (𝐹‘[𝐶]𝑅) = B)

Theoremecoptocl 6129* Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.)
𝑆 = ((B × 𝐶) / 𝑅)    &   ([⟨x, y⟩]𝑅 = A → (φψ))    &   ((x B y 𝐶) → φ)       (A 𝑆ψ)

Theorem2ecoptocl 6130* Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.)
𝑆 = ((𝐶 × 𝐷) / 𝑅)    &   ([⟨x, y⟩]𝑅 = A → (φψ))    &   ([⟨z, w⟩]𝑅 = B → (ψχ))    &   (((x 𝐶 y 𝐷) (z 𝐶 w 𝐷)) → φ)       ((A 𝑆 B 𝑆) → χ)

Theorem3ecoptocl 6131* Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.)
𝑆 = ((𝐷 × 𝐷) / 𝑅)    &   ([⟨x, y⟩]𝑅 = A → (φψ))    &   ([⟨z, w⟩]𝑅 = B → (ψχ))    &   ([⟨v, u⟩]𝑅 = 𝐶 → (χθ))    &   (((x 𝐷 y 𝐷) (z 𝐷 w 𝐷) (v 𝐷 u 𝐷)) → φ)       ((A 𝑆 B 𝑆 𝐶 𝑆) → θ)

Theorembrecop 6132* Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.)
V    &    Er (𝐺 × 𝐺)    &   𝐻 = ((𝐺 × 𝐺) / )    &    = {⟨x, y⟩ ∣ ((x 𝐻 y 𝐻) zwvu((x = [⟨z, w⟩] y = [⟨v, u⟩] ) φ))}    &   ((((z 𝐺 w 𝐺) (A 𝐺 B 𝐺)) ((v 𝐺 u 𝐺) (𝐶 𝐺 𝐷 𝐺))) → (([⟨z, w⟩] = [⟨A, B⟩] [⟨v, u⟩] = [⟨𝐶, 𝐷⟩] ) → (φψ)))       (((A 𝐺 B 𝐺) (𝐶 𝐺 𝐷 𝐺)) → ([⟨A, B⟩] [⟨𝐶, 𝐷⟩] ψ))

Theoremeroveu 6133* Lemma for eroprf 6135. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
𝐽 = (A / 𝑅)    &   𝐾 = (B / 𝑆)    &   (φ𝑇 𝑍)    &   (φ𝑅 Er 𝑈)    &   (φ𝑆 Er 𝑉)    &   (φ𝑇 Er 𝑊)    &   (φA𝑈)    &   (φB𝑉)    &   (φ𝐶𝑊)    &   (φ+ :(A × B)⟶𝐶)    &   ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((𝑟𝑅𝑠 𝑡𝑆u) → (𝑟 + 𝑡)𝑇(𝑠 + u)))       ((φ (𝑋 𝐽 𝑌 𝐾)) → ∃!z𝑝 A 𝑞 B ((𝑋 = [𝑝]𝑅 𝑌 = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))

Theoremerovlem 6134* Lemma for eroprf 6135. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
𝐽 = (A / 𝑅)    &   𝐾 = (B / 𝑆)    &   (φ𝑇 𝑍)    &   (φ𝑅 Er 𝑈)    &   (φ𝑆 Er 𝑉)    &   (φ𝑇 Er 𝑊)    &   (φA𝑈)    &   (φB𝑉)    &   (φ𝐶𝑊)    &   (φ+ :(A × B)⟶𝐶)    &   ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((𝑟𝑅𝑠 𝑡𝑆u) → (𝑟 + 𝑡)𝑇(𝑠 + u)))    &    = {⟨⟨x, y⟩, z⟩ ∣ 𝑝 A 𝑞 B ((x = [𝑝]𝑅 y = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇)}       (φ = (x 𝐽, y 𝐾 ↦ (℩z𝑝 A 𝑞 B ((x = [𝑝]𝑅 y = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇))))

Theoremeroprf 6135* Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
𝐽 = (A / 𝑅)    &   𝐾 = (B / 𝑆)    &   (φ𝑇 𝑍)    &   (φ𝑅 Er 𝑈)    &   (φ𝑆 Er 𝑉)    &   (φ𝑇 Er 𝑊)    &   (φA𝑈)    &   (φB𝑉)    &   (φ𝐶𝑊)    &   (φ+ :(A × B)⟶𝐶)    &   ((φ ((𝑟 A 𝑠 A) (𝑡 B u B))) → ((𝑟𝑅𝑠 𝑡𝑆u) → (𝑟 + 𝑡)𝑇(𝑠 + u)))    &    = {⟨⟨x, y⟩, z⟩ ∣ 𝑝 A 𝑞 B ((x = [𝑝]𝑅 y = [𝑞]𝑆) z = [(𝑝 + 𝑞)]𝑇)}    &   (φ𝑅 𝑋)    &   (φ𝑆 𝑌)    &   𝐿 = (𝐶 / 𝑇)       (φ :(𝐽 × 𝐾)⟶𝐿)

Theoremeroprf2 6136* Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.)
𝐽 = (A / )    &    = {⟨⟨x, y⟩, z⟩ ∣ 𝑝 A 𝑞 A ((x = [𝑝] y = [𝑞] ) z = [(𝑝 + 𝑞)] )}    &   (φ 𝑋)    &   (φ Er 𝑈)    &   (φA𝑈)    &   (φ+ :(A × A)⟶A)    &   ((φ ((𝑟 A 𝑠 A) (𝑡 A u A))) → ((𝑟 𝑠 𝑡 u) → (𝑟 + 𝑡) (𝑠 + u)))       (φ :(𝐽 × 𝐽)⟶𝐽)

Theoremecopoveq 6137* This is the first of several theorems about equivalence relations of the kind used in construction of fractions and signed reals, involving operations on equivalent classes of ordered pairs. This theorem expresses the relation (specified by the hypothesis) in terms of its operation 𝐹. (Contributed by NM, 16-Aug-1995.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}       (((A 𝑆 B 𝑆) (𝐶 𝑆 𝐷 𝑆)) → (⟨A, B𝐶, 𝐷⟩ ↔ (A + 𝐷) = (B + 𝐶)))

Theoremecopovsym 6138* Assuming the operation 𝐹 is commutative, show that the relation , specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}    &   (x + y) = (y + x)       (A BB A)

Theoremecopovtrn 6139* Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}    &   (x + y) = (y + x)    &   ((x 𝑆 y 𝑆) → (x + y) 𝑆)    &   ((x + y) + z) = (x + (y + z))    &   ((x 𝑆 y 𝑆) → ((x + y) = (x + z) → y = z))       ((A B B 𝐶) → A 𝐶)

Theoremecopover 6140* Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is an equivalence relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}    &   (x + y) = (y + x)    &   ((x 𝑆 y 𝑆) → (x + y) 𝑆)    &   ((x + y) + z) = (x + (y + z))    &   ((x 𝑆 y 𝑆) → ((x + y) = (x + z) → y = z))        Er (𝑆 × 𝑆)

Theoremecopovsymg 6141* Assuming the operation 𝐹 is commutative, show that the relation , specified by the first hypothesis, is symmetric. (Contributed by Jim Kingdon, 1-Sep-2019.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}    &   ((x 𝑆 y 𝑆) → (x + y) = (y + x))       (A BB A)

Theoremecopovtrng 6142* Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is transitive. (Contributed by Jim Kingdon, 1-Sep-2019.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}    &   ((x 𝑆 y 𝑆) → (x + y) = (y + x))    &   ((x 𝑆 y 𝑆) → (x + y) 𝑆)    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x + y) + z) = (x + (y + z)))    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x + y) = (x + z) → y = z))       ((A B B 𝐶) → A 𝐶)

Theoremecopoverg 6143* Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is an equivalence relation. (Contributed by Jim Kingdon, 1-Sep-2019.)
= {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z + u) = (w + v)))}    &   ((x 𝑆 y 𝑆) → (x + y) = (y + x))    &   ((x 𝑆 y 𝑆) → (x + y) 𝑆)    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x + y) + z) = (x + (y + z)))    &   ((x 𝑆 y 𝑆 z 𝑆) → ((x + y) = (x + z) → y = z))        Er (𝑆 × 𝑆)

Theoremth3qlem1 6144* Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption. (Contributed by NM, 3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
Er 𝑆    &   (((y 𝑆 w 𝑆) (z 𝑆 v 𝑆)) → ((y w z v) → (y + z) (w + v)))       ((A (𝑆 / ) B (𝑆 / )) → ∃*xyz((A = [y] B = [z] ) x = [(y + z)] ))

Theoremth3qlem2 6145* Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
V    &    Er (𝑆 × 𝑆)    &   ((((w 𝑆 v 𝑆) (u 𝑆 𝑡 𝑆)) ((𝑠 𝑆 f 𝑆) (g 𝑆 𝑆))) → ((⟨w, vu, 𝑡𝑠, fg, ⟩) → (⟨w, v+𝑠, f⟩) (⟨u, 𝑡+g, ⟩)))       ((A ((𝑆 × 𝑆) / ) B ((𝑆 × 𝑆) / )) → ∃*zwvu𝑡((A = [⟨w, v⟩] B = [⟨u, 𝑡⟩] ) z = [(⟨w, v+u, 𝑡⟩)] ))

Theoremth3qcor 6146* Corollary of Theorem 3Q of [Enderton] p. 60. (Contributed by NM, 12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
V    &    Er (𝑆 × 𝑆)    &   ((((w 𝑆 v 𝑆) (u 𝑆 𝑡 𝑆)) ((𝑠 𝑆 f 𝑆) (g 𝑆 𝑆))) → ((⟨w, vu, 𝑡𝑠, fg, ⟩) → (⟨w, v+𝑠, f⟩) (⟨u, 𝑡+g, ⟩)))    &   𝐺 = {⟨⟨x, y⟩, z⟩ ∣ ((x ((𝑆 × 𝑆) / ) y ((𝑆 × 𝑆) / )) wvu𝑡((x = [⟨w, v⟩] y = [⟨u, 𝑡⟩] ) z = [(⟨w, v+u, 𝑡⟩)] ))}       Fun 𝐺

Theoremth3q 6147* Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
V    &    Er (𝑆 × 𝑆)    &   ((((w 𝑆 v 𝑆) (u 𝑆 𝑡 𝑆)) ((𝑠 𝑆 f 𝑆) (g 𝑆 𝑆))) → ((⟨w, vu, 𝑡𝑠, fg, ⟩) → (⟨w, v+𝑠, f⟩) (⟨u, 𝑡+g, ⟩)))    &   𝐺 = {⟨⟨x, y⟩, z⟩ ∣ ((x ((𝑆 × 𝑆) / ) y ((𝑆 × 𝑆) / )) wvu𝑡((x = [⟨w, v⟩] y = [⟨u, 𝑡⟩] ) z = [(⟨w, v+u, 𝑡⟩)] ))}       (((A 𝑆 B 𝑆) (𝐶 𝑆 𝐷 𝑆)) → ([⟨A, B⟩] 𝐺[⟨𝐶, 𝐷⟩] ) = [(⟨A, B+𝐶, 𝐷⟩)] )

Theoremoviec 6148* Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. See iset.mm for additional comments describing the hypotheses. (Unnecessary distinct variable restrictions were removed by David Abernethy, 4-Jun-2013.) (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 4-Jun-2013.)
(((A 𝑆 B 𝑆) (𝐶 𝑆 𝐷 𝑆)) → 𝐻 (𝑆 × 𝑆))    &   (((𝑎 𝑆 𝑏 𝑆) (g 𝑆 𝑆)) → 𝐾 (𝑆 × 𝑆))    &   (((𝑐 𝑆 𝑑 𝑆) (𝑡 𝑆 𝑠 𝑆)) → 𝐿 (𝑆 × 𝑆))    &    V    &    Er (𝑆 × 𝑆)    &    = {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) φ))}    &   (((z = 𝑎 w = 𝑏) (v = 𝑐 u = 𝑑)) → (φψ))    &   (((z = g w = ) (v = 𝑡 u = 𝑠)) → (φχ))    &    + = {⟨⟨x, y⟩, z⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) wvuf((x = ⟨w, v y = ⟨u, f⟩) z = 𝐽))}    &   (((w = 𝑎 v = 𝑏) (u = g f = )) → 𝐽 = 𝐾)    &   (((w = 𝑐 v = 𝑑) (u = 𝑡 f = 𝑠)) → 𝐽 = 𝐿)    &   (((w = A v = B) (u = 𝐶 f = 𝐷)) → 𝐽 = 𝐻)    &    = {⟨⟨x, y⟩, z⟩ ∣ ((x 𝑄 y 𝑄) 𝑎𝑏𝑐𝑑((x = [⟨𝑎, 𝑏⟩] y = [⟨𝑐, 𝑑⟩] ) z = [(⟨𝑎, 𝑏+𝑐, 𝑑⟩)] ))}    &   𝑄 = ((𝑆 × 𝑆) / )    &   ((((𝑎 𝑆 𝑏 𝑆) (𝑐 𝑆 𝑑 𝑆)) ((g 𝑆 𝑆) (𝑡 𝑆 𝑠 𝑆))) → ((ψ χ) → 𝐾 𝐿))       (((A 𝑆 B 𝑆) (𝐶 𝑆 𝐷 𝑆)) → ([⟨A, B⟩] [⟨𝐶, 𝐷⟩] ) = [𝐻] )

Theoremecovcom 6149* Lemma used to transfer a commutative law via an equivalence relation. Most uses will want ecovicom 6150 instead. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
𝐶 = ((𝑆 × 𝑆) / )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → ([⟨x, y⟩] + [⟨z, w⟩] ) = [⟨𝐷, 𝐺⟩] )    &   (((z 𝑆 w 𝑆) (x 𝑆 y 𝑆)) → ([⟨z, w⟩] + [⟨x, y⟩] ) = [⟨𝐻, 𝐽⟩] )    &   𝐷 = 𝐻    &   𝐺 = 𝐽       ((A 𝐶 B 𝐶) → (A + B) = (B + A))

Theoremecovicom 6150* Lemma used to transfer a commutative law via an equivalence relation. (Contributed by Jim Kingdon, 15-Sep-2019.)
𝐶 = ((𝑆 × 𝑆) / )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → ([⟨x, y⟩] + [⟨z, w⟩] ) = [⟨𝐷, 𝐺⟩] )    &   (((z 𝑆 w 𝑆) (x 𝑆 y 𝑆)) → ([⟨z, w⟩] + [⟨x, y⟩] ) = [⟨𝐻, 𝐽⟩] )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → 𝐷 = 𝐻)    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → 𝐺 = 𝐽)       ((A 𝐶 B 𝐶) → (A + B) = (B + A))

Theoremecovass 6151* Lemma used to transfer an associative law via an equivalence relation. In most cases ecoviass 6152 will be more useful. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → ([⟨x, y⟩] + [⟨z, w⟩] ) = [⟨𝐺, 𝐻⟩] )    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → ([⟨z, w⟩] + [⟨v, u⟩] ) = [⟨𝑁, 𝑄⟩] )    &   (((𝐺 𝑆 𝐻 𝑆) (v 𝑆 u 𝑆)) → ([⟨𝐺, 𝐻⟩] + [⟨v, u⟩] ) = [⟨𝐽, 𝐾⟩] )    &   (((x 𝑆 y 𝑆) (𝑁 𝑆 𝑄 𝑆)) → ([⟨x, y⟩] + [⟨𝑁, 𝑄⟩] ) = [⟨𝐿, 𝑀⟩] )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → (𝐺 𝑆 𝐻 𝑆))    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → (𝑁 𝑆 𝑄 𝑆))    &   𝐽 = 𝐿    &   𝐾 = 𝑀       ((A 𝐷 B 𝐷 𝐶 𝐷) → ((A + B) + 𝐶) = (A + (B + 𝐶)))

Theoremecoviass 6152* Lemma used to transfer an associative law via an equivalence relation. (Contributed by Jim Kingdon, 16-Sep-2019.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → ([⟨x, y⟩] + [⟨z, w⟩] ) = [⟨𝐺, 𝐻⟩] )    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → ([⟨z, w⟩] + [⟨v, u⟩] ) = [⟨𝑁, 𝑄⟩] )    &   (((𝐺 𝑆 𝐻 𝑆) (v 𝑆 u 𝑆)) → ([⟨𝐺, 𝐻⟩] + [⟨v, u⟩] ) = [⟨𝐽, 𝐾⟩] )    &   (((x 𝑆 y 𝑆) (𝑁 𝑆 𝑄 𝑆)) → ([⟨x, y⟩] + [⟨𝑁, 𝑄⟩] ) = [⟨𝐿, 𝑀⟩] )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → (𝐺 𝑆 𝐻 𝑆))    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → (𝑁 𝑆 𝑄 𝑆))    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → 𝐽 = 𝐿)    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → 𝐾 = 𝑀)       ((A 𝐷 B 𝐷 𝐶 𝐷) → ((A + B) + 𝐶) = (A + (B + 𝐶)))

Theoremecovdi 6153* Lemma used to transfer a distributive law via an equivalence relation. Most likely ecovidi 6154 will be more helpful. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → ([⟨z, w⟩] + [⟨v, u⟩] ) = [⟨𝑀, 𝑁⟩] )    &   (((x 𝑆 y 𝑆) (𝑀 𝑆 𝑁 𝑆)) → ([⟨x, y⟩] · [⟨𝑀, 𝑁⟩] ) = [⟨𝐻, 𝐽⟩] )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → ([⟨x, y⟩] · [⟨z, w⟩] ) = [⟨𝑊, 𝑋⟩] )    &   (((x 𝑆 y 𝑆) (v 𝑆 u 𝑆)) → ([⟨x, y⟩] · [⟨v, u⟩] ) = [⟨𝑌, 𝑍⟩] )    &   (((𝑊 𝑆 𝑋 𝑆) (𝑌 𝑆 𝑍 𝑆)) → ([⟨𝑊, 𝑋⟩] + [⟨𝑌, 𝑍⟩] ) = [⟨𝐾, 𝐿⟩] )    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → (𝑀 𝑆 𝑁 𝑆))    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → (𝑊 𝑆 𝑋 𝑆))    &   (((x 𝑆 y 𝑆) (v 𝑆 u 𝑆)) → (𝑌 𝑆 𝑍 𝑆))    &   𝐻 = 𝐾    &   𝐽 = 𝐿       ((A 𝐷 B 𝐷 𝐶 𝐷) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))

Theoremecovidi 6154* Lemma used to transfer a distributive law via an equivalence relation. (Contributed by Jim Kingdon, 17-Sep-2019.)
𝐷 = ((𝑆 × 𝑆) / )    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → ([⟨z, w⟩] + [⟨v, u⟩] ) = [⟨𝑀, 𝑁⟩] )    &   (((x 𝑆 y 𝑆) (𝑀 𝑆 𝑁 𝑆)) → ([⟨x, y⟩] · [⟨𝑀, 𝑁⟩] ) = [⟨𝐻, 𝐽⟩] )    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → ([⟨x, y⟩] · [⟨z, w⟩] ) = [⟨𝑊, 𝑋⟩] )    &   (((x 𝑆 y 𝑆) (v 𝑆 u 𝑆)) → ([⟨x, y⟩] · [⟨v, u⟩] ) = [⟨𝑌, 𝑍⟩] )    &   (((𝑊 𝑆 𝑋 𝑆) (𝑌 𝑆 𝑍 𝑆)) → ([⟨𝑊, 𝑋⟩] + [⟨𝑌, 𝑍⟩] ) = [⟨𝐾, 𝐿⟩] )    &   (((z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → (𝑀 𝑆 𝑁 𝑆))    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆)) → (𝑊 𝑆 𝑋 𝑆))    &   (((x 𝑆 y 𝑆) (v 𝑆 u 𝑆)) → (𝑌 𝑆 𝑍 𝑆))    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → 𝐻 = 𝐾)    &   (((x 𝑆 y 𝑆) (z 𝑆 w 𝑆) (v 𝑆 u 𝑆)) → 𝐽 = 𝐿)       ((A 𝐷 B 𝐷 𝐶 𝐷) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))

2.6.25  Equinumerosity

Syntaxcen 6155 Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class

Syntaxcdom 6156 Extend class definition to include the dominance relation (curly less-than-or-equal)
class

Syntaxcfn 6157 Extend class definition to include the class of all finite sets.
class Fin

Definitiondf-en 6158* Define the equinumerosity relation. Definition of [Enderton] p. 129. We define to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 6164. (Contributed by NM, 28-Mar-1998.)
≈ = {⟨x, y⟩ ∣ f f:x1-1-ontoy}

Definitiondf-dom 6159* Define the dominance relation. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 6167 and domen 6168. (Contributed by NM, 28-Mar-1998.)
≼ = {⟨x, y⟩ ∣ f f:x1-1y}

Definitiondf-fin 6160* Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "𝑎 Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 9406. (Contributed by NM, 22-Aug-2008.)
Fin = {xy 𝜔 xy}

Theoremrelen 6161 Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
Rel ≈

Theoremreldom 6162 Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
Rel ≼

Theoremencv 6163 If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
(AB → (A V B V))

Theorembren 6164* Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
(ABf f:A1-1-ontoB)

Theorembrdomg 6165* Dominance relation. (Contributed by NM, 15-Jun-1998.)
(B 𝐶 → (ABf f:A1-1B))

Theorembrdomi 6166* Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
(ABf f:A1-1B)

Theorembrdom 6167* Dominance relation. (Contributed by NM, 15-Jun-1998.)
B V       (ABf f:A1-1B)

Theoremdomen 6168* Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.)
B V       (ABx(Ax xB))

Theoremdomeng 6169* Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of [Enderton] p. 146. (Contributed by NM, 24-Apr-2004.)
(B 𝐶 → (ABx(Ax xB)))

Theoremf1oen3g 6170 The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6173 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)
((𝐹 𝑉 𝐹:A1-1-ontoB) → AB)

Theoremf1oen2g 6171 The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6173 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
((A 𝑉 B 𝑊 𝐹:A1-1-ontoB) → AB)

Theoremf1dom2g 6172 The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 6174 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
((A 𝑉 B 𝑊 𝐹:A1-1B) → AB)

Theoremf1oeng 6173 The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
((A 𝐶 𝐹:A1-1-ontoB) → AB)

Theoremf1domg 6174 The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)
(B 𝐶 → (𝐹:A1-1BAB))

Theoremf1oen 6175 The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
A V       (𝐹:A1-1-ontoBAB)

Theoremf1dom 6176 The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)
B V       (𝐹:A1-1BAB)

Theoremisfi 6177* Express "A is finite." Definition 10.29 of [TakeutiZaring] p. 91 (whose "Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.)
(A Fin ↔ x 𝜔 Ax)

Theoremenssdom 6178 Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
≈ ⊆ ≼

Theoremendom 6179 Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
(ABAB)

Theoremenrefg 6180 Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
(A 𝑉AA)

Theoremenref 6181 Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
A V       AA

Theoremeqeng 6182 Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
(A 𝑉 → (A = BAB))

Theoremdomrefg 6183 Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
(A 𝑉AA)

Theoremen2d 6184* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)
(φA V)    &   (φB V)    &   (φ → (x A𝐶 V))    &   (φ → (y B𝐷 V))    &   (φ → ((x A y = 𝐶) ↔ (y B x = 𝐷)))       (φAB)

Theoremen3d 6185* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.)
(φA V)    &   (φB V)    &   (φ → (x A𝐶 B))    &   (φ → (y B𝐷 A))    &   (φ → ((x A y B) → (x = 𝐷y = 𝐶)))       (φAB)

Theoremen2i 6186* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)
A V    &   B V    &   (x A𝐶 V)    &   (y B𝐷 V)    &   ((x A y = 𝐶) ↔ (y B x = 𝐷))       AB

Theoremen3i 6187* Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.)
A V    &   B V    &   (x A𝐶 B)    &   (y B𝐷 A)    &   ((x A y B) → (x = 𝐷y = 𝐶))       AB

Theoremdom2lem 6188* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004.)
(φ → (x A𝐶 B))    &   (φ → ((x A y A) → (𝐶 = 𝐷x = y)))       (φ → (x A𝐶):A1-1B)

Theoremdom2d 6189* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 20-May-2013.)
(φ → (x A𝐶 B))    &   (φ → ((x A y A) → (𝐶 = 𝐷x = y)))       (φ → (B 𝑅AB))

Theoremdom3d 6190* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by Mario Carneiro, 20-May-2013.)
(φ → (x A𝐶 B))    &   (φ → ((x A y A) → (𝐶 = 𝐷x = y)))    &   (φA 𝑉)    &   (φB 𝑊)       (φAB)

Theoremdom2 6191* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. 𝐶 and 𝐷 can be read 𝐶(x) and 𝐷(y), as can be inferred from their distinct variable conditions. (Contributed by NM, 26-Oct-2003.)
(x A𝐶 B)    &   ((x A y A) → (𝐶 = 𝐷x = y))       (B 𝑉AB)

Theoremdom3 6192* A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. 𝐶 and 𝐷 can be read 𝐶(x) and 𝐷(y), as can be inferred from their distinct variable conditions. (Contributed by Mario Carneiro, 20-May-2013.)
(x A𝐶 B)    &   ((x A y A) → (𝐶 = 𝐷x = y))       ((A 𝑉 B 𝑊) → AB)

Theoremidssen 6193 Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
I ⊆ ≈

Theoremssdomg 6194 A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.)
(B 𝑉 → (ABAB))

Theoremener 6195 Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
≈ Er V

Theoremensymb 6196 Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)
(ABBA)

Theoremensym 6197 Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
(ABBA)

Theoremensymi 6198 Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
AB       BA

Theoremensymd 6199 Symmetry of equinumerosity. Deduction form of ensym 6197. (Contributed by David Moews, 1-May-2017.)
(φAB)       (φBA)

Theorementr 6200 Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
((AB B𝐶) → A𝐶)

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 >