Description: The union of a class is a relation iff any member is a relation. Exercise 6 of TakeutiZaring p. 25 and its converse. (Contributed by NM, 13-Aug-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | reluni | |- ( Rel U. A <-> A. x e. A Rel x ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniiun | |- U. A = U_ x e. A x |
|
2 | 1 | releqi | |- ( Rel U. A <-> Rel U_ x e. A x ) |
3 | reliun | |- ( Rel U_ x e. A x <-> A. x e. A Rel x ) |
|
4 | 2 3 | bitri | |- ( Rel U. A <-> A. x e. A Rel x ) |