Theorem disjiunb

Description: Two ways to say that a collection of index unions C ( i , x ) for i e. A and x e. B is disjoint. (Contributed by AV, 9-Jan-2022)

	Ref	Expression
Hypotheses	disjiunb.1	⊢ ( 𝑖 = 𝑗 → 𝐵 = 𝐷 )
	disjiunb.2	⊢ ( 𝑖 = 𝑗 → 𝐶 = 𝐸 )
Assertion	disjiunb	⊢ ( Disj 𝑖 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ∪ 𝑥 ∈ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ 𝐷 𝐸 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		disjiunb.1	⊢ ( 𝑖 = 𝑗 → 𝐵 = 𝐷 )
2		disjiunb.2	⊢ ( 𝑖 = 𝑗 → 𝐶 = 𝐸 )
3	1 2	iuneq12d	⊢ ( 𝑖 = 𝑗 → ∪ 𝑥 ∈ 𝐵 𝐶 = ∪ 𝑥 ∈ 𝐷 𝐸 )
4	3	disjor	⊢ ( Disj 𝑖 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ∪ 𝑥 ∈ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ 𝐷 𝐸 ) = ∅ ) )