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 U_ x e. A B <-> A. x e. A Rel B )

Proof

Step	Hyp	Ref	Expression
1		df-iun	|- U_ x e. A B = { y | E. x e. A y e. B }
2	1	releqi	|- ( Rel U_ x e. A B <-> Rel { y | E. x e. A y e. B } )
3		df-rel	|- ( Rel { y | E. x e. A y e. B } <-> { y | E. x e. A y e. B } C_ ( _V X. _V ) )
4		abss	|- ( { y | E. x e. A y e. B } C_ ( _V X. _V ) <-> A. y ( E. x e. A y e. B -> y e. ( _V X. _V ) ) )
5		df-rel	|- ( Rel B <-> B C_ ( _V X. _V ) )
6		dfss2	|- ( B C_ ( _V X. _V ) <-> A. y ( y e. B -> y e. ( _V X. _V ) ) )
7	5 6	bitri	|- ( Rel B <-> A. y ( y e. B -> y e. ( _V X. _V ) ) )
8	7	ralbii	|- ( A. x e. A Rel B <-> A. x e. A A. y ( y e. B -> y e. ( _V X. _V ) ) )
9		ralcom4	|- ( A. x e. A A. y ( y e. B -> y e. ( _V X. _V ) ) <-> A. y A. x e. A ( y e. B -> y e. ( _V X. _V ) ) )
10		r19.23v	|- ( A. x e. A ( y e. B -> y e. ( _V X. _V ) ) <-> ( E. x e. A y e. B -> y e. ( _V X. _V ) ) )
11	10	albii	|- ( A. y A. x e. A ( y e. B -> y e. ( _V X. _V ) ) <-> A. y ( E. x e. A y e. B -> y e. ( _V X. _V ) ) )
12	8 9 11	3bitri	|- ( A. x e. A Rel B <-> A. y ( E. x e. A y e. B -> y e. ( _V X. _V ) ) )
13	4 12	bitr4i	|- ( { y | E. x e. A y e. B } C_ ( _V X. _V ) <-> A. x e. A Rel B )
14	2 3 13	3bitri	|- ( Rel U_ x e. A B <-> A. x e. A Rel B )