数学基礎論・数理論理学　その19

書き分けが面倒だから
into:VBα→VBβ:monic
を
α=β
のときに
into=id
とすることにすれば
x:VBξ→B（x∈VBξ+1）
a:VBα→B
について
|x∈a|=a(into(x)) for γ<α, 0 for γ≧α
と簡潔になり
x:VBξ→B（x∈VBξ+1）
a:VBα→B
b:VBβ→B
に対して
|a⊂b|=∧[x∈VBξ+1,ξ<α](a(into(x))c∨|x∈b|)
と簡潔になり
α<β
のときは
|a⊂b|=∧[x∈VBξ+1,ξ<α](a(into(x))c∨b(into(x)))
α=β
のときは
|a⊂b|=∧[x∈VBξ+1,ξ<α](a(into(x))c∨b(into(x)))
α>β
のときは
|a⊂b|=∧[x∈VBξ+1,ξ<β](a(into(x))c∨b(into(x)))
∧∧[x∈VBξ+1,α>ξ≧β]a(into(x))c
と簡潔に書ける