Thread: Set Term Comprehension

Hello all,

I'm really having a hard time in understanding the term part in the following expression.

Code:

{ a : N; s : PN; t : PN | a <ele> s ^ a <!ele> t )

<=>

{ a : N; s : PN; t : PN | a <ele> s ^ a <!ele> t O (a,s,t) }

What difference is it making the term part on the restriction and comprehension?

Thanks

ssharish

And also in the following expression

Code:

{ s : PN; a : N; t : PN | a <ele> s ^ a <ele> t }

And if i had to exhibit an element for the following set. We get {{2}, 1, {1,2}}

Now the question is, the first element is {2} which is from s which is of type Power set of Natural numbers. But 'a' is not an element of s. As a {2} not equal to 2. Am i right?

And also I’m not sure how the 1 got from a as well. So it seems like there two expression in the set comprehension which apples to s & t but not for a?

Please help me understand.

Thanks
Harish