Description
Derived definitions built from ZFC axioms. Kuratowski ordered pair (a,b) = {{a},{a,b}}; relation as set of pairs; function as single-valued relation; domain, range, image.
Dependency Flowchart
Note: Arrows mean "depends on". Assumes Chart 1 (ZFC axioms, pairing, power set).
graph TD
DefPair["Def: Ordered pair\n(a,b) = {{a},{a,b}}"]
DefRel["Def: Relation\nR ⊆ A×B"]
DefFunc["Def: Function\nf: A→B single-valued"]
DefDom["Def: dom R\nprojection"]
DefRan["Def: ran R\nprojection"]
DefCart["Def: A×B\nCartesian product"]
T1["Thm: (a,b)=(c,d)\niff a=c and b=d"]
DefPair --> T1
DefPair --> DefCart
DefCart --> DefRel
DefRel --> DefFunc
DefRel --> DefDom
DefRel --> DefRan
classDef definition fill:#b197fc,color:#fff,stroke:#9775fa
classDef theorem fill:#51cf66,color:#fff,stroke:#40c057
class DefPair,DefRel,DefFunc,DefDom,DefRan,DefCart definition
class T1 theorem
Color Scheme
Blue
Definitions
Definitions
Teal
Theorems
Theorems
Process Statistics
- Nodes: 7
- Edges: 6
- Definitions: 6
- Theorems: 1