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

Metamath Proof Explorer

Theorem disji2f

Description: Property of a disjoint collection: if B ( x ) = C and B ( Y ) = D , and x =/= Y , then B and C are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016)

Ref Expression
Hypotheses disjif.1 ⊢ Ⅎ 𝑥 𝐶
disjif.2 ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐶 )
Assertion disji2f ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑌 ) → ( 𝐵 ∩ 𝐶 ) = ∅ )

Proof

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