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

Metamath Proof Explorer

Theorem disji

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

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

Proof

Step Hyp Ref Expression
1 disji.1 ⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
2 disji.2 ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐷 )
3 inelcm ⊢ ( ( 𝑍 ∈ 𝐶 ∧ 𝑍 ∈ 𝐷 ) → ( 𝐶 ∩ 𝐷 ) ≠ ∅ )
4 1 2 disji2 ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐶 ∩ 𝐷 ) = ∅ )
5 4 3expia ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑋 ≠ 𝑌 → ( 𝐶 ∩ 𝐷 ) = ∅ ) )
6 5 necon1d ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( 𝐶 ∩ 𝐷 ) ≠ ∅ → 𝑋 = 𝑌 ) )
7 6 3impia ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝐶 ∩ 𝐷 ) ≠ ∅ ) → 𝑋 = 𝑌 )
8 3 7 syl3an3 ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑍 ∈ 𝐶 ∧ 𝑍 ∈ 𝐷 ) ) → 𝑋 = 𝑌 )