Metamath Proof Explorer
Table of Contents - 2.6.15. Cofinality (without Axiom of Choice)
- cflem
- cfval
- cff
- cfub
- cflm
- cf0
- cardcf
- cflecard
- cfle
- cfon
- cfeq0
- cfsuc
- cff1
- cfflb
- cfval2
- coflim
- cflim3
- cflim2
- cfom
- cfss
- cfslb
- cfslbn
- cfslb2n
- cofsmo
- cfsmolem
- cfsmo
- cfcoflem
- coftr
- cfcof
- cfidm
- alephsing