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