Home | Metamath
Proof Explorer Theorem List (p. 366 of 462) | < 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: | Metamath Proof Explorer
(1-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elfunsALTV5 36501* | Elementhood in the class of functions. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝐹 ∈ FunsALTV ↔ (∀𝑥 ∈ ran 𝐹∀𝑦 ∈ ran 𝐹(𝑥 = 𝑦 ∨ ([𝑥]◡𝐹 ∩ [𝑦]◡𝐹) = ∅) ∧ 𝐹 ∈ Rels )) | ||
Theorem | elfunsALTVfunALTV 36502 | The element of the class of functions and the function predicate are the same when 𝐹 is a set. (Contributed by Peter Mazsa, 26-Jul-2021.) |
⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ FunsALTV ↔ FunALTV 𝐹)) | ||
Theorem | funALTVfun 36503 | Our definition of the function predicate df-funALTV 36487 (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun 6371, are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( FunALTV 𝐹 ↔ Fun 𝐹) | ||
Theorem | funALTVss 36504 | Subclass theorem for function. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( FunALTV 𝐵 → FunALTV 𝐴)) | ||
Theorem | funALTVeq 36505 | Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.) |
⊢ (𝐴 = 𝐵 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Theorem | funALTVeqi 36506 | Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( FunALTV 𝐴 ↔ FunALTV 𝐵) | ||
Theorem | funALTVeqd 36507 | Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( FunALTV 𝐴 ↔ FunALTV 𝐵)) | ||
Definition | df-disjss 36508 | Define the class of all disjoint sets (but not necessarily disjoint relations, cf. df-disjs 36509). It is used only by df-disjs 36509. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjss = {𝑥 ∣ ≀ ◡𝑥 ∈ CnvRefRels } | ||
Definition | df-disjs 36509 |
Define the disjoint relations class, i.e., the class of disjoints. We
need Disjs for the definition of Parts and Part
for the
Partition-Equivalence Theorems: this need for Parts as disjoint relations
on their domain quotients is the reason why we must define Disjs
instead of simply using converse functions (cf. dfdisjALTV 36518).
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 36532. Alternate definitions are dfdisjs 36513, ... , dfdisjs5 36517. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ Disjs = ( Disjss ∩ Rels ) | ||
Definition | df-disjALTV 36510 |
Define the disjoint relation predicate, i.e., the disjoint predicate. A
disjoint relation is a converse function of the relation by dfdisjALTV 36518,
see the comment of df-disjs 36509 why we need disjoint relations instead of
converse functions anyway.
The element of the class of disjoints and the disjoint predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set, see eldisjsdisj 36532. Alternate definitions are dfdisjALTV 36518, ... , dfdisjALTV5 36522. (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( CnvRefRel ≀ ◡𝑅 ∧ Rel 𝑅)) | ||
Definition | df-eldisjs 36511 | Define the disjoint elementhood relations class, i.e., the disjoint elements class. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 36534. (Contributed by Peter Mazsa, 28-Nov-2022.) |
⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs } | ||
Definition | df-eldisj 36512 |
Define the disjoint elementhood relation predicate, i.e., the disjoint
elementhood predicate. Read: the elements of 𝐴 are disjoint. The
element of the disjoint elements class and the disjoint elementhood
predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when
𝐴 is a set, see eleldisjseldisj 36534.
As of now, disjoint elementhood is defined as "partition" in set.mm : compare df-prt 36580 with dfeldisj5 36526. See also the comments of ~? dfmembpart2 and of ~? df-parts . (Contributed by Peter Mazsa, 17-Jul-2021.) |
⊢ ( ElDisj 𝐴 ↔ Disj (◡ E ↾ 𝐴)) | ||
Theorem | dfdisjs 36513 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ∈ CnvRefRels } | ||
Theorem | dfdisjs2 36514 | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ≀ ◡𝑟 ⊆ I } | ||
Theorem | dfdisjs3 36515* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢∀𝑣∀𝑥((𝑢𝑟𝑥 ∧ 𝑣𝑟𝑥) → 𝑢 = 𝑣)} | ||
Theorem | dfdisjs4 36516* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑥∃*𝑢 𝑢𝑟𝑥} | ||
Theorem | dfdisjs5 36517* | Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ Disjs = {𝑟 ∈ Rels ∣ ∀𝑢 ∈ dom 𝑟∀𝑣 ∈ dom 𝑟(𝑢 = 𝑣 ∨ ([𝑢]𝑟 ∩ [𝑣]𝑟) = ∅)} | ||
Theorem | dfdisjALTV 36518 | Alternate definition of the disjoint relation predicate. A disjoint relation is a converse function of the relation, see the comment of df-disjs 36509 why we need disjoint relations instead of converse functions anyway. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( FunALTV ◡𝑅 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV2 36519 | Alternate definition of the disjoint relation predicate, cf. dffunALTV2 36493. (Contributed by Peter Mazsa, 27-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ ( ≀ ◡𝑅 ⊆ I ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV3 36520* | Alternate definition of the disjoint relation predicate, cf. dffunALTV3 36494. (Contributed by Peter Mazsa, 28-Jul-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV4 36521* | Alternate definition of the disjoint relation predicate, cf. dffunALTV4 36495. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ Rel 𝑅)) | ||
Theorem | dfdisjALTV5 36522* | Alternate definition of the disjoint relation predicate, cf. dffunALTV5 36496. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ ( Disj 𝑅 ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ Rel 𝑅)) | ||
Theorem | dfeldisj2 36523 | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ≀ ◡(◡ E ↾ 𝐴) ⊆ I ) | ||
Theorem | dfeldisj3 36524* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 ∀𝑥 ∈ (𝑢 ∩ 𝑣)𝑢 = 𝑣) | ||
Theorem | dfeldisj4 36525* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑥∃*𝑢 ∈ 𝐴 𝑥 ∈ 𝑢) | ||
Theorem | dfeldisj5 36526* | Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021.) |
⊢ ( ElDisj 𝐴 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ (𝑢 ∩ 𝑣) = ∅)) | ||
Theorem | eldisjs 36527 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ∈ CnvRefRels ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs2 36528 | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ ( ≀ ◡𝑅 ⊆ I ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs3 36529* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑢∀𝑣∀𝑥((𝑢𝑅𝑥 ∧ 𝑣𝑅𝑥) → 𝑢 = 𝑣) ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs4 36530* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ Disjs ↔ (∀𝑥∃*𝑢 𝑢𝑅𝑥 ∧ 𝑅 ∈ Rels )) | ||
Theorem | eldisjs5 36531* | Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 5-Sep-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ (∀𝑢 ∈ dom 𝑅∀𝑣 ∈ dom 𝑅(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ 𝑅 ∈ Rels ))) | ||
Theorem | eldisjsdisj 36532 | The element of the class of disjoint relations and the disjoint relation predicate are the same, that is (𝑅 ∈ Disjs ↔ Disj 𝑅) when 𝑅 is a set. (Contributed by Peter Mazsa, 25-Jul-2021.) |
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ Disjs ↔ Disj 𝑅)) | ||
Theorem | eleldisjs 36533 | Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ (◡ E ↾ 𝐴) ∈ Disjs )) | ||
Theorem | eleldisjseldisj 36534 | The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set. (Contributed by Peter Mazsa, 23-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴)) | ||
Theorem | disjrel 36535 | Disjoint relation is a relation. (Contributed by Peter Mazsa, 15-Sep-2021.) |
⊢ ( Disj 𝑅 → Rel 𝑅) | ||
Theorem | disjss 36536 | Subclass theorem for disjoints. (Contributed by Peter Mazsa, 28-Oct-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjssi 36537 | Subclass theorem for disjoints, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( Disj 𝐵 → Disj 𝐴) | ||
Theorem | disjssd 36538 | Subclass theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐵 → Disj 𝐴)) | ||
Theorem | disjeq 36539 | Equality theorem for disjoints. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjeqi 36540 | Equality theorem for disjoints, inference version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( Disj 𝐴 ↔ Disj 𝐵) | ||
Theorem | disjeqd 36541 | Equality theorem for disjoints, deduction version. (Contributed by Peter Mazsa, 22-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( Disj 𝐴 ↔ Disj 𝐵)) | ||
Theorem | disjdmqseqeq1 36542 | Lemma for the equality theorem for partition ~? parteq1 . (Contributed by Peter Mazsa, 5-Oct-2021.) |
⊢ (𝑅 = 𝑆 → (( Disj 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ↔ ( Disj 𝑆 ∧ (dom 𝑆 / 𝑆) = 𝐴))) | ||
Theorem | eldisjss 36543 | Subclass theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 ⊆ 𝐵 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjssi 36544 | Subclass theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ ( ElDisj 𝐵 → ElDisj 𝐴) | ||
Theorem | eldisjssd 36545 | Subclass theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 28-Sep-2021.) |
⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐵 → ElDisj 𝐴)) | ||
Theorem | eldisjeq 36546 | Equality theorem for disjoint elementhood. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | eldisjeqi 36547 | Equality theorem for disjoint elementhood, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ( ElDisj 𝐴 ↔ ElDisj 𝐵) | ||
Theorem | eldisjeqd 36548 | Equality theorem for disjoint elementhood, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ( ElDisj 𝐴 ↔ ElDisj 𝐵)) | ||
Theorem | disjxrn 36549 | Two ways of saying that a range Cartesian product is disjoint. (Contributed by Peter Mazsa, 17-Jun-2020.) (Revised by Peter Mazsa, 21-Sep-2021.) |
⊢ ( Disj (𝑅 ⋉ 𝑆) ↔ ( ≀ ◡𝑅 ∩ ≀ ◡𝑆) ⊆ I ) | ||
Theorem | disjorimxrn 36550 | Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 12-Jul-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ (( Disj 𝑅 ∨ Disj 𝑆) → Disj (𝑅 ⋉ 𝑆)) | ||
Theorem | disjimxrn 36551 | Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 15-Dec-2020.) (Revised by Peter Mazsa, 22-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ 𝑆)) | ||
Theorem | disjimres 36552 | Disjointness condition for restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑅 → Disj (𝑅 ↾ 𝐴)) | ||
Theorem | disjimin 36553 | Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021.) (Revised by Peter Mazsa, 28-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ 𝑆)) | ||
Theorem | disjiminres 36554 | Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ∩ (𝑆 ↾ 𝐴))) | ||
Theorem | disjimxrnres 36555 | Disjointness condition for range Cartesian product with restriction. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ ( Disj 𝑆 → Disj (𝑅 ⋉ (𝑆 ↾ 𝐴))) | ||
Theorem | disjALTV0 36556 | The null class is disjoint. (Contributed by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj ∅ | ||
Theorem | disjALTVid 36557 | The class of identity relations is disjoint. (Contributed by Peter Mazsa, 20-Jun-2021.) |
⊢ Disj I | ||
Theorem | disjALTVidres 36558 | The class of identity relations restricted is disjoint. (Contributed by Peter Mazsa, 28-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj ( I ↾ 𝐴) | ||
Theorem | disjALTVinidres 36559 | The intersection with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.) |
⊢ Disj (𝑅 ∩ ( I ↾ 𝐴)) | ||
Theorem | disjALTVxrnidres 36560 | The class of range Cartesian product with restricted identity relation is disjoint. (Contributed by Peter Mazsa, 25-Jun-2020.) (Revised by Peter Mazsa, 27-Sep-2021.) |
⊢ Disj (𝑅 ⋉ ( I ↾ 𝐴)) | ||
Theorem | prtlem60 36561 | Lemma for prter3 36590. (Contributed by Rodolfo Medina, 9-Oct-2010.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) | ||
Theorem | bicomdd 36562 | Commute two sides of a biconditional in a deduction. (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ↔ 𝜒))) | ||
Theorem | jca2r 36563 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) | ||
Theorem | jca3 36564 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 14-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → (𝜒 ∧ 𝜏)))) | ||
Theorem | prtlem70 36565 | Lemma for prter3 36590: a rearrangement of conjuncts. (Contributed by Rodolfo Medina, 20-Oct-2010.) |
⊢ ((((𝜓 ∧ 𝜂) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜏))) ∧ 𝜑) ↔ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ (𝜃 ∧ 𝜏)))) ∧ 𝜂)) | ||
Theorem | ibdr 36566 | Reverse of ibd 272. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (𝜑 → (𝜒 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | prtlem100 36567 | Lemma for prter3 36590. (Contributed by Rodolfo Medina, 19-Oct-2010.) |
⊢ (∃𝑥 ∈ 𝐴 (𝐵 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑥 ∈ (𝐴 ∖ {∅})(𝐵 ∈ 𝑥 ∧ 𝜑)) | ||
Theorem | prtlem5 36568* | Lemma for prter1 36587, prter2 36589, prter3 36590 and prtex 36588. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Mario Carneiro, 11-Dec-2016.) |
⊢ ([𝑠 / 𝑣][𝑟 / 𝑢]∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝑟 ∈ 𝑥 ∧ 𝑠 ∈ 𝑥)) | ||
Theorem | prtlem80 36569 | Lemma for prter2 36589. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ {𝐴})) | ||
Theorem | brabsb2 36570* | A closed form of brabsb 5401. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} → (𝑧𝑅𝑤 ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
Theorem | eqbrrdv2 36571* | Other version of eqbrrdiv 5653. (Contributed by Rodolfo Medina, 30-Sep-2010.) |
⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)) ⇒ ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵) | ||
Theorem | prtlem9 36572* | Lemma for prter3 36590. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 [𝑥] ∼ = [𝐴] ∼ ) | ||
Theorem | prtlem10 36573* | Lemma for prter3 36590. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ( ∼ Er 𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ )))) | ||
Theorem | prtlem11 36574 | Lemma for prter2 36589. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝐵 ∈ 𝐷 → (𝐶 ∈ 𝐴 → (𝐵 = [𝐶] ∼ → 𝐵 ∈ (𝐴 / ∼ )))) | ||
Theorem | prtlem12 36575* | Lemma for prtex 36588 and prter3 36590. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} → Rel ∼ ) | ||
Theorem | prtlem13 36576* | Lemma for prter1 36587, prter2 36589, prter3 36590 and prtex 36588. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣)) | ||
Theorem | prtlem16 36577* | Lemma for prtex 36588, prter2 36589 and prter3 36590. (Contributed by Rodolfo Medina, 14-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ dom ∼ = ∪ 𝐴 | ||
Theorem | prtlem400 36578* | Lemma for prter2 36589 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ ¬ ∅ ∈ (∪ 𝐴 / ∼ ) | ||
Syntax | wprt 36579 | Extend the definition of a wff to include the partition predicate. |
wff Prt 𝐴 | ||
Definition | df-prt 36580* | Define the partition predicate. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | ||
Theorem | erprt 36581 | The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ ( ∼ Er 𝑋 → Prt (𝐴 / ∼ )) | ||
Theorem | prtlem14 36582* | Lemma for prter1 36587, prter2 36589 and prtex 36588. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦))) | ||
Theorem | prtlem15 36583* | Lemma for prter1 36587 and prtex 36588. (Contributed by Rodolfo Medina, 13-Oct-2010.) |
⊢ (Prt 𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧))) | ||
Theorem | prtlem17 36584* | Lemma for prter2 36589. (Contributed by Rodolfo Medina, 15-Oct-2010.) |
⊢ (Prt 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (∃𝑦 ∈ 𝐴 (𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦) → 𝑤 ∈ 𝑥))) | ||
Theorem | prtlem18 36585* | Lemma for prter2 36589. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → (𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤))) | ||
Theorem | prtlem19 36586* | Lemma for prter2 36589. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ((𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣) → 𝑣 = [𝑧] ∼ )) | ||
Theorem | prter1 36587* | Every partition generates an equivalence relation. (Contributed by Rodolfo Medina, 13-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ∼ Er ∪ 𝐴) | ||
Theorem | prtex 36588* | The equivalence relation generated by a partition is a set if and only if the partition itself is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → ( ∼ ∈ V ↔ 𝐴 ∈ V)) | ||
Theorem | prter2 36589* | The quotient set of the equivalence relation generated by a partition equals the partition itself. (Contributed by Rodolfo Medina, 17-Oct-2010.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ (Prt 𝐴 → (∪ 𝐴 / ∼ ) = (𝐴 ∖ {∅})) | ||
Theorem | prter3 36590* | For every partition there exists a unique equivalence relation whose quotient set equals the partition. (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) |
⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝐴 (𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢)} ⇒ ⊢ ((𝑆 Er ∪ 𝐴 ∧ (∪ 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → ∼ = 𝑆) | ||
We are sad to report the passing of Metamath creator and long-time contributor Norm Megill (1950 - 2021). Norm of course was the author of the Metamath proof language, the specification, all of the early tools (and some of the later ones), and the foundational work in logic and set theory for set.mm. His tools, now at https://github.com/metamath/metamath-exe , include a proof verifier, a proof assistant, a proof minimizer, style checking and reformatting, and tools for searching and displaying proofs. One of his key insights was that formal proofs can exist not only to be verified by computers, but also to be read by humans. Both the specification of the proof format (which stores full proofs, as opposed to the proof templates used by most proof assistants) and the generated web display of Metamath proofs, one of its distinctive features, contribute to this double objective. Metamath innovated both by using a very simple substitution rule (and then using that to build more complicated notions like free and bound variables) and also by taking the axiom schemas found in many theories and taking them to the next level - by making all axioms, theorems and proofs operate in terms of schemas. Not content to create Metamath for his own amusement, he also published it for the world and encouraged the development of a community of people who contributed to it and created their own tools. He was an active participant in the Metamath mailing list and other forums until days before his passing. It is often our custom to supply a quote from someone memorialized in a mathbox entry. And it is difficult to select a quote for someone who has written so much about Metamath over the years. But here is one quote from the Metamath web page which illustrates not just his clear thinking about what Metamath can and cannot do but also his desire to encourage students at all levels: Q: Will Metamath help me learn abstract mathematics? A: Yes, but probably not by itself. In order to follow a proof in an advanced math textbook, you may need to know prerequisites that could take years to learn. Some people find this frustrating. In contrast, Metamath uses a single, simple substitution rule that allows you to follow any proof mechanically. You can actually jump in anywhere and be convinced that the symbol string you see in a proof step is a consequence of the symbol strings in the earlier steps that it references, even if you don't understand what the symbols mean. But this is quite different from understanding the meaning of the math that results. Metamath alone probably will not give you an intuitive feel for abstract math, in the same way it can be hard to grasp a large computer program just by reading its source code, even though you may understand each individual instruction. However, the Bibliographic Cross-Reference lets you compare informal proofs in math textbooks and see all the implicit missing details "left to the reader." | ||
These older axiom schemes are obsolete and should not be used outside of this section. They are proved above as theorems axc4 , sp 2180, axc7 2316, axc10 2382, axc11 2427, axc11n 2423, axc15 2419, axc9 2379, axc14 2460, and axc16 2258. | ||
Axiom | ax-c5 36591 |
Axiom of Specialization. A universally quantified wff implies the wff
without the universal quantifier (i.e., an instance, or special case, of
the generalized wff). In other words, if something is true for all
𝑥, then it is true for any specific
𝑥
(that would typically occur
as a free variable in the wff substituted for 𝜑). (A free variable
is one that does not occur in the scope of a quantifier: 𝑥 and
𝑦
are both free in 𝑥 = 𝑦, but only 𝑥 is free in ∀𝑦𝑥 = 𝑦.)
Axiom scheme C5' in [Megill] p. 448 (p. 16
of the preprint). Also appears
as Axiom B5 of [Tarski] p. 67 (under his
system S2, defined in the last
paragraph on p. 77).
Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1803. Conditional forms of the converse are given by ax-13 2369, ax-c14 36599, ax-c16 36600, and ax-5 1918. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from 𝑥 for the special case. In our axiomatization, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution (see stdpc4 2074). An interesting alternate axiomatization uses axc5c711 36626 and ax-c4 36592 in place of ax-c5 36591, ax-4 1817, ax-10 2141, and ax-11 2158. This axiom is obsolete and should no longer be used. It is proved above as Theorem sp 2180. (Contributed by NM, 3-Jan-1993.) Use sp 2180 instead. (New usage is discouraged.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c4 36592 |
Axiom of Quantified Implication. This axiom moves a universal quantifier
from outside to inside an implication, quantifying 𝜓. Notice that
𝑥 must not be a free variable in the
antecedent of the quantified
implication, and we express this by binding 𝜑 to "protect" the
axiom
from a 𝜑 containing a free 𝑥. Axiom
scheme C4' in [Megill]
p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of
[Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69.
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc4 2320. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Axiom | ax-c7 36593 |
Axiom of Quantified Negation. This axiom is used to manipulate negated
quantifiers. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of
the preprint). An alternate axiomatization could use axc5c711 36626 in place
of ax-c5 36591, ax-c7 36593, and ax-11 2158.
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc7 2316. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Axiom | ax-c10 36594 |
A variant of ax6 2381. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the
preprint).
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc10 2382. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Axiom | ax-c11 36595 |
Axiom ax-c11 36595 was the original version of ax-c11n 36596 ("n" for "new"),
before it was discovered (in May 2008) that the shorter ax-c11n 36596 could
replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of
the preprint).
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11 2427. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Axiom | ax-c11n 36596 |
Axiom of Quantifier Substitution. One of the equality and substitution
axioms of predicate calculus with equality. Appears as Lemma L12 in
[Megill] p. 445 (p. 12 of the preprint).
The original version of this axiom was ax-c11 36595 and was replaced with this shorter ax-c11n 36596 ("n" for "new") in May 2008. The old axiom is proved from this one as Theorem axc11 2427. Conversely, this axiom is proved from ax-c11 36595 as Theorem axc11nfromc11 36634. This axiom was proved redundant in July 2015. See Theorem axc11n 2423. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc11n 2423. (Contributed by NM, 16-May-2008.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) | ||
Axiom | ax-c15 36597 |
Axiom ax-c15 36597 was the original version of ax-12 2175, before it was
discovered (in Jan. 2007) that the shorter ax-12 2175 could replace it. It
appears as Axiom scheme C15' in [Megill]
p. 448 (p. 16 of the preprint).
It is based on Lemma 16 of [Tarski] p. 70
and Axiom C8 of [Monk2] p. 105,
from which it can be proved by cases. To understand this theorem more
easily, think of "¬ ∀𝑥𝑥 = 𝑦 →..." as informally meaning
"if
𝑥 and 𝑦 are distinct variables
then..." The antecedent becomes
false if the same variable is substituted for 𝑥 and 𝑦,
ensuring
the theorem is sound whenever this is the case. In some later theorems,
we call an antecedent of the form ¬ ∀𝑥𝑥 = 𝑦 a "distinctor."
Interestingly, if the wff expression substituted for 𝜑 contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of Axiom ax-c15 36597 (from which the ax-12 2175 instance follows by Theorem ax12 2420.) The proof is by induction on formula length, using ax12eq 36649 and ax12el 36650 for the basis steps and ax12indn 36651, ax12indi 36652, and ax12inda 36656 for the induction steps. (This paragraph is true provided we use ax-c11 36595 in place of ax-c11n 36596.) This axiom is obsolete and should no longer be used. It is proved above as Theorem axc15 2419, which should be used instead. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Axiom | ax-c9 36598 |
Axiom of Quantifier Introduction. One of the equality and substitution
axioms of predicate calculus with equality. Informally, it says that
whenever 𝑧 is distinct from 𝑥 and
𝑦,
and 𝑥 =
𝑦 is true,
then 𝑥 = 𝑦 quantified with 𝑧 is also
true. In other words, 𝑧
is irrelevant to the truth of 𝑥 = 𝑦. Axiom scheme C9' in [Megill]
p. 448 (p. 16 of the preprint). It apparently does not otherwise appear
in the literature but is easily proved from textbook predicate calculus by
cases.
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc9 2379. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) | ||
Axiom | ax-c14 36599 |
Axiom of Quantifier Introduction. One of the equality and substitution
axioms for a non-logical predicate in our predicate calculus with
equality. Axiom scheme C14' in [Megill]
p. 448 (p. 16 of the preprint).
It is redundant if we include ax-5 1918; see Theorem axc14 2460. Alternately,
ax-5 1918 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-5 1918.
We retain ax-c14 36599 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-5 1918, which might be easier to study for some
theoretical
purposes.
This axiom is obsolete and should no longer be used. It is proved above as Theorem axc14 2460. (Contributed by NM, 24-Jun-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦))) | ||
Axiom | ax-c16 36600* |
Axiom of Distinct Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-5 1918
to be a
metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p.
16 of the preprint). It apparently does not otherwise appear in the
literature but is easily proved from textbook predicate calculus by
cases. It is a somewhat bizarre axiom since the antecedent is always
false in set theory (see dtru 5252), but nonetheless it is technically
necessary as you can see from its uses.
This axiom is redundant if we include ax-5 1918; see Theorem axc16 2258. Alternately, ax-5 1918 becomes logically redundant in the presence of this axiom, but without ax-5 1918 we lose the more powerful metalogic that results from being able to express the concept of a setvar variable not occurring in a wff (as opposed to just two setvar variables being distinct). We retain ax-c16 36600 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-5 1918, which might be easier to study for some theoretical purposes. This axiom is obsolete and should no longer be used. It is proved above as Theorem axc16 2258. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |