Metamath Proof Explorer

Table of Contents - 4.2. ZFC Set Theory plus the Tarski-Grothendieck Axiom

  1. Introduce the Tarski-Grothendieck Axiom
    1. ax-groth
    2. axgroth5
    3. axgroth2
  2. Tarski map function
    1. ctskm
    2. df-tskm
    3. tskmval
    4. tskmid
    5. tskmcl
    6. sstskm
    7. eltskm