Metamath Proof Explorer


Table of Contents - 21.38.5.21. Finite relationship composition.

In order for theorems on the transitive closure of a relation to be grouped together before the concept of continuity, we really need an analogue of that works on finite ordinals or finite sets instead of natural numbers.

  1. relexp2
  2. relexpnul
  3. eliunov2
  4. eltrclrec
  5. elrtrclrec
  6. briunov2
  7. brmptiunrelexpd
  8. fvmptiunrelexplb0d
  9. fvmptiunrelexplb0da
  10. fvmptiunrelexplb1d
  11. brfvid
  12. brfvidRP
  13. fvilbd
  14. fvilbdRP
  15. brfvrcld
  16. brfvrcld2
  17. fvrcllb0d
  18. fvrcllb0da
  19. fvrcllb1d
  20. brtrclrec
  21. brrtrclrec
  22. briunov2uz
  23. eliunov2uz
  24. ov2ssiunov2
  25. relexp0eq
  26. iunrelexp0
  27. relexpxpnnidm
  28. relexpiidm
  29. relexpss1d
  30. comptiunov2i
  31. corclrcl
  32. iunrelexpmin1
  33. relexpmulnn
  34. relexpmulg
  35. trclrelexplem
  36. iunrelexpmin2
  37. relexp01min
  38. relexp1idm
  39. relexp0idm
  40. relexp0a
  41. relexpxpmin
  42. relexpaddss
  43. iunrelexpuztr