This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reluni

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 ⁡ ⋃ A ↔ ∀ x ∈ A Rel ⁡ x

Proof

Step Hyp Ref Expression
1 uniiun ⊢ ⋃ A = ⋃ x ∈ A x
2 1 releqi ⊢ Rel ⁡ ⋃ A ↔ Rel ⁡ ⋃ x ∈ A x
3 reliun ⊢ Rel ⁡ ⋃ x ∈ A x ↔ ∀ x ∈ A Rel ⁡ x
4 2 3 bitri ⊢ Rel ⁡ ⋃ A ↔ ∀ x ∈ A Rel ⁡ x