Theorem relun

Description: The union of two relations is a relation. Compare Exercise 5 of TakeutiZaring p. 25. (Contributed by NM, 12-Aug-1994)

	Ref	Expression
Assertion	relun	⊢ ( Rel ( 𝐴 ∪ 𝐵 ) ↔ ( Rel 𝐴 ∧ Rel 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		unss	⊢ ( ( 𝐴 ⊆ ( V × V ) ∧ 𝐵 ⊆ ( V × V ) ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( V × V ) )
2		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
3		df-rel	⊢ ( Rel 𝐵 ↔ 𝐵 ⊆ ( V × V ) )
4	2 3	anbi12i	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) ↔ ( 𝐴 ⊆ ( V × V ) ∧ 𝐵 ⊆ ( V × V ) ) )
5		df-rel	⊢ ( Rel ( 𝐴 ∪ 𝐵 ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( V × V ) )
6	1 4 5	3bitr4ri	⊢ ( Rel ( 𝐴 ∪ 𝐵 ) ↔ ( Rel 𝐴 ∧ Rel 𝐵 ) )