Theorem disjif2

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, 6-Apr-2017)

	Ref	Expression
Hypotheses	disjif2.1	⊢ Ⅎ 𝑥 𝐴
	disjif2.2	⊢ Ⅎ 𝑥 𝐶
	disjif2.3	⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐶 )
Assertion	disjif2	⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑥 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		disjif2.1	⊢ Ⅎ 𝑥 𝐴
2		disjif2.2	⊢ Ⅎ 𝑥 𝐶
3		disjif2.3	⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐶 )
4		inelcm	⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )
5	1	disjorsf	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
6		equequ1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 𝑧 ↔ 𝑥 = 𝑧 ) )
7		csbeq1	⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑥 / 𝑥 ⦌ 𝐵 )
8		csbid	⊢ ⦋ 𝑥 / 𝑥 ⦌ 𝐵 = 𝐵
9	7 8	eqtrdi	⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
10	9	ineq1d	⊢ ( 𝑦 = 𝑥 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ( 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
11	10	eqeq1d	⊢ ( 𝑦 = 𝑥 → ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
12	6 11	orbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( 𝑥 = 𝑧 ∨ ( 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
13		eqeq2	⊢ ( 𝑧 = 𝑌 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑌 ) )
14		nfcv	⊢ Ⅎ 𝑥 𝑌
15	14 2 3	csbhypf	⊢ ( 𝑧 = 𝑌 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = 𝐶 )
16	15	ineq2d	⊢ ( 𝑧 = 𝑌 → ( 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ( 𝐵 ∩ 𝐶 ) )
17	16	eqeq1d	⊢ ( 𝑧 = 𝑌 → ( ( 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
18	13 17	orbi12d	⊢ ( 𝑧 = 𝑌 → ( ( 𝑥 = 𝑧 ∨ ( 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( 𝑥 = 𝑌 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ) )
19	12 18	rspc2v	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ( 𝑥 = 𝑌 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ) )
20	5 19	syl5bi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( Disj 𝑥 ∈ 𝐴 𝐵 → ( 𝑥 = 𝑌 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) ) )
21	20	impcom	⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑥 = 𝑌 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )
22	21	ord	⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ¬ 𝑥 = 𝑌 → ( 𝐵 ∩ 𝐶 ) = ∅ ) )
23	22	necon1ad	⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( 𝐵 ∩ 𝐶 ) ≠ ∅ → 𝑥 = 𝑌 ) )
24	23	3impia	⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) → 𝑥 = 𝑌 )
25	4 24	syl3an3	⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑥 = 𝑌 )