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∈AB↔∀x∈ARel⁡B

Proof

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