Metamath Proof Explorer

Theorem disji2

Description: Property of a disjoint collection: if B ( X ) = C and B ( Y ) = D , and X =/= Y , then C and D are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Hypotheses disji.1 ⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
disji.2 ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐷 )
Assertion disji2 ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐶 ∩ 𝐷 ) = ∅ )

Proof

Step Hyp Ref Expression
1 disji.1 ⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
2 disji.2 ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐷 )
3 df-ne ⊢ ( 𝑋 ≠ 𝑌 ↔ ¬ 𝑋 = 𝑌 )
4 disjors ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
5 eqeq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 = 𝑧 ↔ 𝑋 = 𝑧 ) )
6 nfcv ⊢ Ⅎ 𝑥 𝑋
7 nfcv ⊢ Ⅎ 𝑥 𝐶
8 6 7 1 csbhypf ⊢ ( 𝑦 = 𝑋 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐶 )
9 8 ineq1d ⊢ ( 𝑦 = 𝑋 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ( 𝐶 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
10 9 eqeq1d ⊢ ( 𝑦 = 𝑋 → ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( 𝐶 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
11 5 10 orbi12d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( 𝑋 = 𝑧 ∨ ( 𝐶 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
12 eqeq2 ⊢ ( 𝑧 = 𝑌 → ( 𝑋 = 𝑧 ↔ 𝑋 = 𝑌 ) )
13 nfcv ⊢ Ⅎ 𝑥 𝑌
14 nfcv ⊢ Ⅎ 𝑥 𝐷
15 13 14 2 csbhypf ⊢ ( 𝑧 = 𝑌 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = 𝐷 )
16 15 ineq2d ⊢ ( 𝑧 = 𝑌 → ( 𝐶 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ( 𝐶 ∩ 𝐷 ) )
17 16 eqeq1d ⊢ ( 𝑧 = 𝑌 → ( ( 𝐶 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( 𝐶 ∩ 𝐷 ) = ∅ ) )
18 12 17 orbi12d ⊢ ( 𝑧 = 𝑌 → ( ( 𝑋 = 𝑧 ∨ ( 𝐶 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( 𝑋 = 𝑌 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) )
19 11 18 rspc2v ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ( 𝑋 = 𝑌 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) )
20 4 19 syl5bi ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( Disj 𝑥 ∈ 𝐴 𝐵 → ( 𝑋 = 𝑌 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) )
21 20 impcom ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑋 = 𝑌 ∨ ( 𝐶 ∩ 𝐷 ) = ∅ ) )
22 21 ord ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ¬ 𝑋 = 𝑌 → ( 𝐶 ∩ 𝐷 ) = ∅ ) )
23 3 22 syl5bi ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑋 ≠ 𝑌 → ( 𝐶 ∩ 𝐷 ) = ∅ ) )
24 23 3impia ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐶 ∩ 𝐷 ) = ∅ )