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

Metamath Proof Explorer

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