![]() |
Metamath
Proof Explorer Theorem List (p. 395 of 445) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28382) |
![]() (28383-29905) |
![]() (29906-44433) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ensucne0 39401 | A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof shortened by SN, 16-Nov-2023.) |
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅) | ||
Theorem | ensucne0OLD 39402 | A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅) | ||
Theorem | nndomog 39403 | Cardinal ordering agrees with ordinal number ordering when the smaller number is a natural number. Compare with nndomo 8565 when both are natural numbers. (Originally by NM, 17-Jun-1998.) (Contributed by RP, 5-Nov-2023.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
Theorem | dfom6 39404 | Let ω be defined to be the union of the set of all finite ordinals. (Contributed by RP, 27-Sep-2023.) |
⊢ ω = ∪ (On ∩ Fin) | ||
Theorem | infordmin 39405 | ω is the smallest infinite ordinal. (Contributed by RP, 27-Sep-2023.) |
⊢ ∀𝑥 ∈ (On ∖ Fin)ω ⊆ 𝑥 | ||
Theorem | iscard4 39406 | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
⊢ ((card‘𝐴) = 𝐴 ↔ 𝐴 ∈ ran card) | ||
Theorem | iscard5 39407* | Two ways to express the property of being a cardinal number. (Contributed by RP, 8-Nov-2023.) |
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴)) | ||
Theorem | elrncard 39408* | Let us define a cardinal number to be an element 𝐴 ∈ On such that 𝐴 is not equipotent with any 𝑥 ∈ 𝐴. (Contributed by RP, 1-Oct-2023.) |
⊢ (𝐴 ∈ ran card ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ≈ 𝐴)) | ||
Theorem | harsucnn 39409 | The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.) |
⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴) | ||
Theorem | harval3 39410* | (har‘𝐴) is the least cardinal that is greater than 𝐴. (Contributed by RP, 4-Nov-2023.) |
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | harval3on 39411* | For any ordinal number 𝐴 let (har‘𝐴) denote the least cardinal that is greater than 𝐴; (Contributed by RP, 4-Nov-2023.) |
⊢ (𝐴 ∈ On → (har‘𝐴) = ∩ {𝑥 ∈ ran card ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | en2pr 39412* | A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023.) |
⊢ (𝐴 ≈ 2o ↔ ∃𝑥∃𝑦(𝐴 = {𝑥, 𝑦} ∧ 𝑥 ≠ 𝑦)) | ||
Theorem | pr2cv 39413 | If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | pr2el1 39414 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ {𝐴, 𝐵}) | ||
Theorem | pr2cv1 39415 | If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ V) | ||
Theorem | pr2el2 39416 | If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ {𝐴, 𝐵}) | ||
Theorem | pr2cv2 39417 | If an unordered pair is equinumerous to ordinal two, then a part is a set. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ V) | ||
Theorem | pren2 39418 | An unordered pair is equinumerous to ordinal two iff both parts are sets not equal to each other. (Contributed by RP, 8-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴 ≠ 𝐵)) | ||
Theorem | pr2eldif1 39419 | If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐴 ∈ ({𝐴, 𝐵} ∖ {𝐵})) | ||
Theorem | pr2eldif2 39420 | If an unordered pair is equinumerous to ordinal two, then a part is an element of the difference of the pair and the singleton of the other part. (Contributed by RP, 21-Oct-2023.) |
⊢ ({𝐴, 𝐵} ≈ 2o → 𝐵 ∈ ({𝐴, 𝐵} ∖ {𝐴})) | ||
Theorem | pren2d 39421 | A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) | ||
Theorem | aleph1min 39422 | (ℵ‘1o) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023.) |
⊢ (ℵ‘1o) = ∩ {𝑥 ∈ On ∣ ω ≺ 𝑥} | ||
Theorem | alephiso2 39423 | ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.) |
⊢ ℵ Isom E , ≺ (On, {𝑥 ∈ ran card ∣ ω ⊆ 𝑥}) | ||
Theorem | alephiso3 39424 | ℵ is a strictly order-preserving mapping of On onto the class of all infinite cardinal numbers. (Contributed by RP, 18-Nov-2023.) |
⊢ ℵ Isom E , ≺ (On, (ran card ∖ ω)) | ||
Theorem | pwelg 39425* | The powerclass is an element of a class closed under union and powerclass operations iff the element is a member of that class. (Contributed by RP, 21-Mar-2020.) |
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝒫 𝐴 ∈ 𝐵)) | ||
Theorem | pwinfig 39426* | The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝐵 is a class which is closed under both the union and the powerclass operations and which may have infinite sets as members. (Contributed by RP, 21-Mar-2020.) |
⊢ (∀𝑥 ∈ 𝐵 (∪ 𝑥 ∈ 𝐵 ∧ 𝒫 𝑥 ∈ 𝐵) → (𝐴 ∈ (𝐵 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝐵 ∖ Fin))) | ||
Theorem | pwinfi2 39427 | The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑈 is a weak universe. (Contributed by RP, 21-Mar-2020.) |
⊢ (𝑈 ∈ WUni → (𝐴 ∈ (𝑈 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑈 ∖ Fin))) | ||
Theorem | pwinfi3 39428 | The powerclass of an infinite set is an infinite set, and vice-versa. Here 𝑇 is a transitive Tarski universe. (Contributed by RP, 21-Mar-2020.) |
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → (𝐴 ∈ (𝑇 ∖ Fin) ↔ 𝒫 𝐴 ∈ (𝑇 ∖ Fin))) | ||
Theorem | pwinfi 39429 | The powerclass of an infinite set is an infinite set, and vice-versa. (Contributed by RP, 21-Mar-2020.) |
⊢ (𝐴 ∈ (V ∖ Fin) ↔ 𝒫 𝐴 ∈ (V ∖ Fin)) | ||
While there is not yet a definition, the finite intersection property of a class is introduced by fiint 8648 where two textbook definitions are shown to be equivalent. This property is seen often with ordinal numbers (onin 6104, ordelinel 6171), chains of sets ordered by the proper subset relation (sorpssin 7322), various sets in the field of topology (inopn 21195, incld 21339, innei 21421, ... ) and "universal" classes like weak universes (wunin 9988, tskin 10034) and the class of all sets (inex1g 5121). | ||
Theorem | fipjust 39430* | A definition of the finite intersection property of a class based on closure under pairwise intersection of its elements is independent of the dummy variables. (Contributed by RP, 1-Jan-2020.) |
⊢ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 ∩ 𝑣) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴) | ||
Theorem | cllem0 39431* | The class of all sets with property 𝜑(𝑧) is closed under the binary operation on sets defined in 𝑅(𝑥, 𝑦). (Contributed by RP, 3-Jan-2020.) |
⊢ 𝑉 = {𝑧 ∣ 𝜑} & ⊢ 𝑅 ∈ 𝑈 & ⊢ (𝑧 = 𝑅 → (𝜑 ↔ 𝜓)) & ⊢ (𝑧 = 𝑥 → (𝜑 ↔ 𝜒)) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜃)) & ⊢ ((𝜒 ∧ 𝜃) → 𝜓) ⇒ ⊢ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑅 ∈ 𝑉 | ||
Theorem | superficl 39432* | The class of all supersets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 | ||
Theorem | superuncl 39433* | The class of all supersets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝐵 ⊆ 𝑧} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
Theorem | ssficl 39434* | The class of all subsets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020.) (Proof shortened by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 | ||
Theorem | ssuncl 39435* | The class of all subsets of a class is closed under binary union. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∪ 𝑦) ∈ 𝐴 | ||
Theorem | ssdifcl 39436* | The class of all subsets of a class is closed under class difference. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∖ 𝑦) ∈ 𝐴 | ||
Theorem | sssymdifcl 39437* | The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020.) |
⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵} ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴 | ||
Theorem | fiinfi 39438* | If two classes have the finite intersection property, then so does their intersection. (Contributed by RP, 1-Jan-2020.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = (𝐴 ∩ 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥 ∩ 𝑦) ∈ 𝐶) | ||
Theorem | rababg 39439 | Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020.) |
⊢ (∀𝑥(𝜑 → 𝑥 ∈ 𝐴) ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ 𝜑}) | ||
Theorem | elintabg 39440* | Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | ||
Theorem | elinintab 39441* | Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∈ (𝐵 ∩ ∩ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | ||
Theorem | elmapintrab 39442* | Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020.) |
⊢ 𝐶 ∈ V & ⊢ 𝐶 ⊆ 𝐵 ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = 𝐶 ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐶)))) | ||
Theorem | elinintrab 39443* | Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 14-Aug-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ {𝑤 ∈ 𝒫 𝐵 ∣ ∃𝑥(𝑤 = (𝐵 ∩ 𝑥) ∧ 𝜑)} ↔ ((∃𝑥𝜑 → 𝐴 ∈ 𝐵) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))) | ||
Theorem | inintabss 39444* | Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝐴 ∩ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜑)} | ||
Theorem | inintabd 39445* | Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → (𝐴 ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 𝐴 ∣ ∃𝑥(𝑤 = (𝐴 ∩ 𝑥) ∧ 𝜓)}) | ||
Theorem | xpinintabd 39446* | Value of the intersection of cross-product with the intersection of a nonempty class. (Contributed by RP, 12-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ((𝐴 × 𝐵) ∩ ∩ {𝑥 ∣ 𝜓}) = ∩ {𝑤 ∈ 𝒫 (𝐴 × 𝐵) ∣ ∃𝑥(𝑤 = ((𝐴 × 𝐵) ∩ 𝑥) ∧ 𝜓)}) | ||
Theorem | relintabex 39447 | If the intersection of a class is a relation, then the class is nonempty. (Contributed by RP, 12-Aug-2020.) |
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑) | ||
Theorem | elcnvcnvintab 39448* | Two ways of saying a set is an element of the converse of the converse of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝐴 ∈ ◡◡∩ {𝑥 ∣ 𝜑} ↔ (𝐴 ∈ (V × V) ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))) | ||
Theorem | relintab 39449* | Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020.) |
⊢ (Rel ∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)}) | ||
Theorem | nonrel 39450 | A non-relation is equal to the base class with all ordered pairs removed. (Contributed by RP, 25-Oct-2020.) |
⊢ (𝐴 ∖ ◡◡𝐴) = (𝐴 ∖ (V × V)) | ||
Theorem | elnonrel 39451 | Only an ordered pair where not both entries are sets could be an element of the non-relation part of class. (Contributed by RP, 25-Oct-2020.) |
⊢ (〈𝑋, 𝑌〉 ∈ (𝐴 ∖ ◡◡𝐴) ↔ (∅ ∈ 𝐴 ∧ ¬ (𝑋 ∈ V ∧ 𝑌 ∈ V))) | ||
Theorem | cnvssb 39452 | Subclass theorem for converse. (Contributed by RP, 22-Oct-2020.) |
⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ◡𝐴 ⊆ ◡𝐵)) | ||
Theorem | relnonrel 39453 | The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ (Rel 𝐴 ↔ (𝐴 ∖ ◡◡𝐴) = ∅) | ||
Theorem | cnvnonrel 39454 | The converse of the non-relation part of a class is empty. (Contributed by RP, 18-Oct-2020.) |
⊢ ◡(𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | brnonrel 39455 | A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020.) |
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋(𝐴 ∖ ◡◡𝐴)𝑌) | ||
Theorem | dmnonrel 39456 | The domain of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ dom (𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | rnnonrel 39457 | The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ran (𝐴 ∖ ◡◡𝐴) = ∅ | ||
Theorem | resnonrel 39458 | A restriction of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) ↾ 𝐵) = ∅ | ||
Theorem | imanonrel 39459 | An image under the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) “ 𝐵) = ∅ | ||
Theorem | cononrel1 39460 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴) ∘ 𝐵) = ∅ | ||
Theorem | cononrel2 39461 | Composition with the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020.) |
⊢ (𝐴 ∘ (𝐵 ∖ ◡◡𝐵)) = ∅ | ||
See also idssxp 5803 by Thierry Arnoux. | ||
Theorem | elmapintab 39462* | Two ways to say a set is an element of mapped intersection of a class. Here 𝐹 maps elements of 𝐶 to elements of ∩ {𝑥 ∣ 𝜑} or 𝑥. (Contributed by RP, 19-Aug-2020.) |
⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ 𝐶 ∧ (𝐹‘𝐴) ∈ ∩ {𝑥 ∣ 𝜑})) & ⊢ (𝐴 ∈ 𝐸 ↔ (𝐴 ∈ 𝐶 ∧ (𝐹‘𝐴) ∈ 𝑥)) ⇒ ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ 𝐶 ∧ ∀𝑥(𝜑 → 𝐴 ∈ 𝐸))) | ||
Theorem | fvnonrel 39463 | The function value of any class under a non-relation is empty. (Contributed by RP, 23-Oct-2020.) |
⊢ ((𝐴 ∖ ◡◡𝐴)‘𝑋) = ∅ | ||
Theorem | elinlem 39464 | Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020.) |
⊢ (𝐴 ∈ (𝐵 ∩ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ( I ‘𝐴) ∈ 𝐶)) | ||
Theorem | elcnvcnvlem 39465 | Two ways to say a set is a member of the converse of the converse of a class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝐴 ∈ ◡◡𝐵 ↔ (𝐴 ∈ (V × V) ∧ ( I ‘𝐴) ∈ 𝐵)) | ||
Original probably needs new subsection for Relation-related existence theorems. | ||
Theorem | cnvcnvintabd 39466* | Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜓)}) | ||
Theorem | elcnvlem 39467 | Two ways to say a set is a member of the converse of a class. (Contributed by RP, 19-Aug-2020.) |
⊢ 𝐹 = (𝑥 ∈ (V × V) ↦ 〈(2nd ‘𝑥), (1st ‘𝑥)〉) ⇒ ⊢ (𝐴 ∈ ◡𝐵 ↔ (𝐴 ∈ (V × V) ∧ (𝐹‘𝐴) ∈ 𝐵)) | ||
Theorem | elcnvintab 39468* | Two ways of saying a set is an element of the converse of the intersection of a class. (Contributed by RP, 19-Aug-2020.) |
⊢ (𝐴 ∈ ◡∩ {𝑥 ∣ 𝜑} ↔ (𝐴 ∈ (V × V) ∧ ∀𝑥(𝜑 → 𝐴 ∈ ◡𝑥))) | ||
Theorem | cnvintabd 39469* | Value of the converse of the intersection of a nonempty class. (Contributed by RP, 20-Aug-2020.) |
⊢ (𝜑 → ∃𝑥𝜓) ⇒ ⊢ (𝜑 → ◡∩ {𝑥 ∣ 𝜓} = ∩ {𝑤 ∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡𝑥 ∧ 𝜓)}) | ||
Theorem | undmrnresiss 39470* | Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg 39471. (Contributed by RP, 26-Sep-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦))) | ||
Theorem | reflexg 39471* | Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐴𝑥 ∧ 𝑦𝐴𝑦))) | ||
Theorem | cnvssco 39472* | A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020.) |
⊢ (◡𝐴 ⊆ ◡(𝐵 ∘ 𝐶) ↔ ∀𝑥∀𝑦∃𝑧(𝑥𝐴𝑦 → (𝑥𝐶𝑧 ∧ 𝑧𝐵𝑦))) | ||
Theorem | refimssco 39473 | Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020.) |
⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐴 → ◡𝐴 ⊆ ◡(𝐴 ∘ 𝐴)) | ||
Theorem | cleq2lem 39474 | Equality implies bijection. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ 𝜑) ↔ (𝑅 ⊆ 𝐵 ∧ 𝜓))) | ||
Theorem | cbvcllem 39475* | Change of bound variable in class of supersets of a with a property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜑)} = {𝑦 ∣ (𝑋 ⊆ 𝑦 ∧ 𝜓)} | ||
Theorem | clublem 39476* | If a superset 𝑌 of 𝑋 possesses the property parameterized in 𝑥 in 𝜓, then 𝑌 is a superset of the closure of that property for the set 𝑋. (Contributed by RP, 23-Jul-2020.) |
⊢ (𝜑 → 𝑌 ∈ V) & ⊢ (𝑥 = 𝑌 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ 𝑌) | ||
Theorem | clss2lem 39477* | The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → (𝜒 → 𝜓)) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} ⊆ ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜒)}) | ||
Theorem | dfid7 39478* | Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020.) |
⊢ I = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | mptrcllem 39479* | Show two versions of a closure with reflexive properties are equal. (Contributed by RP, 19-Oct-2020.) |
⊢ (𝑥 ∈ 𝑉 → ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (𝜑 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} ∈ V) & ⊢ (𝑥 ∈ 𝑉 → ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)} ∈ V) & ⊢ (𝑥 ∈ 𝑉 → 𝜒) & ⊢ (𝑥 ∈ 𝑉 → 𝜃) & ⊢ (𝑥 ∈ 𝑉 → 𝜏) & ⊢ (𝑦 = ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)} → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 = ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)} → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ↔ 𝜃)) & ⊢ (𝑧 = ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (𝜑 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} → (𝜓 ↔ 𝜏)) ⇒ ⊢ (𝑥 ∈ 𝑉 ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (𝜑 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) = (𝑥 ∈ 𝑉 ↦ ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ 𝜓)}) | ||
Theorem | cotrintab 39480 | The intersection of a class is a transitive relation if membership in the class implies the member is a transitive relation. (Contributed by RP, 28-Oct-2020.) |
⊢ (𝜑 → (𝑥 ∘ 𝑥) ⊆ 𝑥) ⇒ ⊢ (∩ {𝑥 ∣ 𝜑} ∘ ∩ {𝑥 ∣ 𝜑}) ⊆ ∩ {𝑥 ∣ 𝜑} | ||
Theorem | rclexi 39481* | The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexlem 39482 | Existence of relation implies existence of union with Cartesian product of domain and range. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∪ ((dom 𝑅 ∪ ran 𝑅) × (dom 𝑅 ∪ ran 𝑅))) ∈ V) | ||
Theorem | rtrclex 39483* | The reflexive-transitive closure of a set exists. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝐴 ∈ V ↔ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V) | ||
Theorem | trclubgNEW 39484* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (𝑅 ∪ (dom 𝑅 × ran 𝑅))) | ||
Theorem | trclubNEW 39485* | If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020.) |
⊢ (𝜑 → 𝑅 ∈ V) & ⊢ (𝜑 → Rel 𝑅) ⇒ ⊢ (𝜑 → ∩ {𝑥 ∣ (𝑅 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ⊆ (dom 𝑅 × ran 𝑅)) | ||
Theorem | trclexi 39486* | The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} ∈ V | ||
Theorem | rtrclexi 39487* | The reflexive-transitive closure of a set exists. (Contributed by RP, 27-Oct-2020.) |
⊢ 𝐴 ∈ 𝑉 ⇒ ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ ((𝑥 ∘ 𝑥) ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥))} ∈ V | ||
Theorem | clrellem 39488* | When the property 𝜓 holds for a relation substituted for 𝑥, then the closure on that property is a relation if the base set is a relation. (Contributed by RP, 30-Jul-2020.) |
⊢ (𝜑 → 𝑌 ∈ V) & ⊢ (𝜑 → Rel 𝑋) & ⊢ (𝑥 = ◡◡𝑌 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → Rel ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)}) | ||
Theorem | clcnvlem 39489* | When 𝐴, an upper bound of the closure, exists and certain substitutions hold the converse of the closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ ((𝜑 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (𝜒 → 𝜓)) & ⊢ ((𝜑 ∧ 𝑦 = ◡𝑥) → (𝜓 → 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ 𝜓)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ 𝜒)}) | ||
Theorem | cnvtrucl0 39490* | The converse of the trivial closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ⊤)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ⊤)}) | ||
Theorem | cnvrcl0 39491* | The converse of the reflexive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)}) | ||
Theorem | cnvtrcl0 39492* | The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.) |
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)}) | ||
Theorem | dmtrcl 39493* | The domain of the transitive closure is equal to the domain of its base relation. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝑋 ∈ 𝑉 → dom ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = dom 𝑋) | ||
Theorem | rntrcl 39494* | The range of the transitive closure is equal to the range of its base relation. (Contributed by RP, 1-Nov-2020.) |
⊢ (𝑋 ∈ 𝑉 → ran ∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ (𝑥 ∘ 𝑥) ⊆ 𝑥)} = ran 𝑋) | ||
Theorem | dfrtrcl5 39495* | Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020.) |
⊢ t* = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))}) | ||
Theorem | trcleq2lemRP 39496 | Equality implies bijection. (Contributed by RP, 5-May-2020.) (Proof modification is discouraged.) |
⊢ (𝐴 = 𝐵 → ((𝑅 ⊆ 𝐴 ∧ (𝐴 ∘ 𝐴) ⊆ 𝐴) ↔ (𝑅 ⊆ 𝐵 ∧ (𝐵 ∘ 𝐵) ⊆ 𝐵))) | ||
Theorem | al3im 39497 | Version of ax-4 1795 for a nested implication. (Contributed by RP, 13-Apr-2020.) |
⊢ (∀𝑥(𝜑 → (𝜓 → (𝜒 → 𝜃))) → (∀𝑥𝜑 → (∀𝑥𝜓 → (∀𝑥𝜒 → ∀𝑥𝜃)))) | ||
Theorem | intima0 39498* | Two ways of expressing the intersection of images of a class. (Contributed by RP, 13-Apr-2020.) |
⊢ ∩ 𝑎 ∈ 𝐴 (𝑎 “ 𝐵) = ∩ {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = (𝑎 “ 𝐵)} | ||
Theorem | elimaint 39499* | Element of image of intersection. (Contributed by RP, 13-Apr-2020.) |
⊢ (𝑦 ∈ (∩ 𝐴 “ 𝐵) ↔ ∃𝑏 ∈ 𝐵 ∀𝑎 ∈ 𝐴 〈𝑏, 𝑦〉 ∈ 𝑎) | ||
Theorem | csbcog 39500 | Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∘ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∘ ⦋𝐴 / 𝑥⦌𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |