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 ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 Rel 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 }
2	1	releqi	⊢ ( Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ Rel { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } )
3		df-rel	⊢ ( Rel { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } ⊆ ( V × V ) )
4		abss	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } ⊆ ( V × V ) ↔ ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) )
5		df-rel	⊢ ( Rel 𝐵 ↔ 𝐵 ⊆ ( V × V ) )
6		dfss2	⊢ ( 𝐵 ⊆ ( V × V ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) )
7	5 6	bitri	⊢ ( Rel 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) )
8	7	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) )
9		ralcom4	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) )
10		r19.23v	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) )
11	10	albii	⊢ ( ∀ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) ↔ ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) )
12	8 9 11	3bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 Rel 𝐵 ↔ ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ ( V × V ) ) )
13	4 12	bitr4i	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } ⊆ ( V × V ) ↔ ∀ 𝑥 ∈ 𝐴 Rel 𝐵 )
14	2 3 13	3bitri	⊢ ( Rel ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 Rel 𝐵 )