Description: Two ways to say that a collection B ( i ) for i e. A is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | disjors | ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv | ⊢ Ⅎ 𝑖 𝐵 | |
2 | nfcsb1v | ⊢ Ⅎ 𝑥 ⦋ 𝑖 / 𝑥 ⦌ 𝐵 | |
3 | csbeq1a | ⊢ ( 𝑥 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) | |
4 | 1 2 3 | cbvdisj | ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ) |
5 | csbeq1 | ⊢ ( 𝑖 = 𝑗 → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 = ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) | |
6 | 5 | disjor | ⊢ ( Disj 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) |
7 | 4 6 | bitri | ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) |