This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑖 ∈ 𝐴 ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ∪ 𝑥 ∈ 𝐵 𝐶 ∩ ∪ 𝑥 ∈ 𝐷 𝐸 ) = ∅ ) )