| Step | Hyp | Ref
| Expression |
| 1 | | tglnpt2.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | tglnpt2.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
| 3 | | tglnpt2.l |
. . . . . 6
⊢ 𝐿 = (LineG‘𝐺) |
| 4 | | tglnpt2.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 5 | 4 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → 𝐺 ∈ TarskiG) |
| 6 | | simp-4r 784 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → 𝑥 ∈ 𝑃) |
| 7 | | simpllr 776 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → 𝑧 ∈ 𝑃) |
| 8 | | simplrr 778 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → 𝑥 ≠ 𝑧) |
| 9 | 1, 2, 3, 5, 6, 7, 8 | tglinerflx2 28642 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → 𝑧 ∈ (𝑥𝐿𝑧)) |
| 10 | | simplrl 777 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → 𝐴 = (𝑥𝐿𝑧)) |
| 11 | 9, 10 | eleqtrrd 2844 |
. . . 4
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → 𝑧 ∈ 𝐴) |
| 12 | | simpr 484 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → 𝑋 = 𝑥) |
| 13 | 12, 8 | eqnetrd 3008 |
. . . 4
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → 𝑋 ≠ 𝑧) |
| 14 | | neeq2 3004 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑧)) |
| 15 | 14 | rspcev 3622 |
. . . 4
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑋 ≠ 𝑧) → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦) |
| 16 | 11, 13, 15 | syl2anc 584 |
. . 3
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 = 𝑥) → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦) |
| 17 | 4 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 ≠ 𝑥) → 𝐺 ∈ TarskiG) |
| 18 | | simp-4r 784 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 ≠ 𝑥) → 𝑥 ∈ 𝑃) |
| 19 | | simpllr 776 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 ≠ 𝑥) → 𝑧 ∈ 𝑃) |
| 20 | | simplrr 778 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 ≠ 𝑥) → 𝑥 ≠ 𝑧) |
| 21 | 1, 2, 3, 17, 18, 19, 20 | tglinerflx1 28641 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 ≠ 𝑥) → 𝑥 ∈ (𝑥𝐿𝑧)) |
| 22 | | simplrl 777 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 ≠ 𝑥) → 𝐴 = (𝑥𝐿𝑧)) |
| 23 | 21, 22 | eleqtrrd 2844 |
. . . 4
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 ≠ 𝑥) → 𝑥 ∈ 𝐴) |
| 24 | | simpr 484 |
. . . 4
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 ≠ 𝑥) → 𝑋 ≠ 𝑥) |
| 25 | | neeq2 3004 |
. . . . 5
⊢ (𝑦 = 𝑥 → (𝑋 ≠ 𝑦 ↔ 𝑋 ≠ 𝑥)) |
| 26 | 25 | rspcev 3622 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑋 ≠ 𝑥) → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦) |
| 27 | 23, 24, 26 | syl2anc 584 |
. . 3
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) ∧ 𝑋 ≠ 𝑥) → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦) |
| 28 | 16, 27 | pm2.61dane 3029 |
. 2
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦) |
| 29 | | tglnpt2.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ran 𝐿) |
| 30 | 1, 2, 3, 4, 29 | tgisline 28635 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝐴 = (𝑥𝐿𝑧) ∧ 𝑥 ≠ 𝑧)) |
| 31 | 28, 30 | r19.29vva 3216 |
1
⊢ (𝜑 → ∃𝑦 ∈ 𝐴 𝑋 ≠ 𝑦) |