Metamath Proof Explorer

Theorem reliun

Description: An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008)

Ref Expression
Assertion reliun ⊢ Rel ⁡ ⋃ x ∈ A B ↔ ∀ x ∈ A Rel ⁡ B

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ⋃ x ∈ A B = y | ∃ x ∈ A y ∈ B
2 1 releqi ⊢ Rel ⁡ ⋃ x ∈ A B ↔ Rel ⁡ y | ∃ x ∈ A y ∈ B
3 df-rel ⊢ Rel ⁡ y | ∃ x ∈ A y ∈ B ↔ y | ∃ x ∈ A y ∈ B ⊆ V × V
4 abss ⊢ y | ∃ x ∈ A y ∈ B ⊆ V × V ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ V × V
5 df-rel ⊢ Rel ⁡ B ↔ B ⊆ V × V
6 dfss2 ⊢ B ⊆ V × V ↔ ∀ y y ∈ B → y ∈ V × V
7 5 6 bitri ⊢ Rel ⁡ B ↔ ∀ y y ∈ B → y ∈ V × V
8 7 ralbii ⊢ ∀ x ∈ A Rel ⁡ B ↔ ∀ x ∈ A ∀ y y ∈ B → y ∈ V × V
9 ralcom4 ⊢ ∀ x ∈ A ∀ y y ∈ B → y ∈ V × V ↔ ∀ y ∀ x ∈ A y ∈ B → y ∈ V × V
10 r19.23v ⊢ ∀ x ∈ A y ∈ B → y ∈ V × V ↔ ∃ x ∈ A y ∈ B → y ∈ V × V
11 10 albii ⊢ ∀ y ∀ x ∈ A y ∈ B → y ∈ V × V ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ V × V
12 8 9 11 3bitri ⊢ ∀ x ∈ A Rel ⁡ B ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ V × V
13 4 12 bitr4i ⊢ y | ∃ x ∈ A y ∈ B ⊆ V × V ↔ ∀ x ∈ A Rel ⁡ B
14 2 3 13 3bitri ⊢ Rel ⁡ ⋃ x ∈ A B ↔ ∀ x ∈ A Rel ⁡ B