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 syl5bi ( ( 𝑥𝐴𝑌𝐴 ) → ( Disj 𝑥𝐴 𝐵 → ( 𝑥 = 𝑌 ∨ ( 𝐵𝐶 ) = ∅ ) ) )
20 19 impcom ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ) → ( 𝑥 = 𝑌 ∨ ( 𝐵𝐶 ) = ∅ ) )
21 20 ord ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ) → ( ¬ 𝑥 = 𝑌 → ( 𝐵𝐶 ) = ∅ ) )
22 3 21 syl5bi ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ) → ( 𝑥𝑌 → ( 𝐵𝐶 ) = ∅ ) )
23 22 3impia ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ∧ 𝑥𝑌 ) → ( 𝐵𝐶 ) = ∅ )