Metamath Proof Explorer


Theorem disjif

Description: Property of a disjoint collection: if B ( x ) and B ( Y ) = D have a common element Z , then x = Y . (Contributed by Thierry Arnoux, 30-Dec-2016)

Ref Expression
Hypotheses disjif.1 𝑥 𝐶
disjif.2 ( 𝑥 = 𝑌𝐵 = 𝐶 )
Assertion disjif ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ∧ ( 𝑍𝐵𝑍𝐶 ) ) → 𝑥 = 𝑌 )

Proof

Step Hyp Ref Expression
1 disjif.1 𝑥 𝐶
2 disjif.2 ( 𝑥 = 𝑌𝐵 = 𝐶 )
3 inelcm ( ( 𝑍𝐵𝑍𝐶 ) → ( 𝐵𝐶 ) ≠ ∅ )
4 1 2 disji2f ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ∧ 𝑥𝑌 ) → ( 𝐵𝐶 ) = ∅ )
5 4 3expia ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ) → ( 𝑥𝑌 → ( 𝐵𝐶 ) = ∅ ) )
6 5 necon1d ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ) → ( ( 𝐵𝐶 ) ≠ ∅ → 𝑥 = 𝑌 ) )
7 6 3impia ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ∧ ( 𝐵𝐶 ) ≠ ∅ ) → 𝑥 = 𝑌 )
8 3 7 syl3an3 ( ( Disj 𝑥𝐴 𝐵 ∧ ( 𝑥𝐴𝑌𝐴 ) ∧ ( 𝑍𝐵𝑍𝐶 ) ) → 𝑥 = 𝑌 )