Theorem relbigcup

Description: The Bigcup relationship is a relationship. (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Assertion	relbigcup	⊢ Rel Bigcup

Proof

Step	Hyp	Ref	Expression
1		relxp	⊢ Rel ( V × V )
2		reldif	⊢ ( Rel ( V × V ) → Rel ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) ) )
3	1 2	ax-mp	⊢ Rel ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) )
4		df-bigcup	⊢ Bigcup = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) )
5	4	releqi	⊢ ( Rel Bigcup ↔ Rel ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) ) )
6	3 5	mpbir	⊢ Rel Bigcup