Metamath Proof Explorer

Theorem segconeu

Description: Existential uniqueness version of segconeq . (Contributed by Scott Fenton, 19-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion segconeu ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → ∃! r ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B

Proof

Step Hyp Ref Expression
1 simpl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → N ∈ ℕ
2 simpr2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N
3 simpr1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
4 axsegcon ⊢ N ∈ ℕ ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ r ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B
5 1 2 3 4 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → ∃ r ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B
6 simpl23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N ∧ D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → C ≠ D
7 simprl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N ∧ D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → D Btwn C r ∧ D r Cgr A B
8 simprr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N ∧ D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → D Btwn C s ∧ D s Cgr A B
9 6 7 8 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N ∧ D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → C ≠ D ∧ D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B
10 9 ex ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → C ≠ D ∧ D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B
11 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → N ∈ ℕ
12 simp22r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
13 simp21l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
14 simp21r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
15 simp22l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
16 simp3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → r ∈ 𝔼 ⁡ N
17 simp3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → s ∈ 𝔼 ⁡ N
18 segconeq ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → C ≠ D ∧ D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → r = s
19 11 12 13 14 15 16 17 18 syl133anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → C ≠ D ∧ D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → r = s
20 10 19 syld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → r = s
21 20 3expa ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D ∧ r ∈ 𝔼 ⁡ N ∧ s ∈ 𝔼 ⁡ N → D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → r = s
22 21 ralrimivva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → ∀ r ∈ 𝔼 ⁡ N ∀ s ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → r = s
23 opeq2 ⊢ r = s → C r = C s
24 23 breq2d ⊢ r = s → D Btwn C r ↔ D Btwn C s
25 opeq2 ⊢ r = s → D r = D s
26 25 breq1d ⊢ r = s → D r Cgr A B ↔ D s Cgr A B
27 24 26 anbi12d ⊢ r = s → D Btwn C r ∧ D r Cgr A B ↔ D Btwn C s ∧ D s Cgr A B
28 27 reu4 ⊢ ∃! r ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B ↔ ∃ r ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B ∧ ∀ r ∈ 𝔼 ⁡ N ∀ s ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B ∧ D Btwn C s ∧ D s Cgr A B → r = s
29 5 22 28 sylanbrc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ≠ D → ∃! r ∈ 𝔼 ⁡ N D Btwn C r ∧ D r Cgr A B