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

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 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑥 = 𝑌 )