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