Theorem lpni 31075

Description: For any line in a planar incidence geometry, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.)

Hypothesis

Ref	Expression
l2p.1	⊢ 𝑃 = ∪ 𝐺

Assertion

Ref	Expression
lpni	⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)

Distinct variable groups:   𝐺,𝑎   𝐿,𝑎   𝑃,𝑎

Proof of Theorem lpni

Dummy variables 𝑏 𝑐 𝑙 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		l2p.1	. . . 4 ⊢ 𝑃 = ∪ 𝐺
2	1	tncp 31073	. . 3 ⊢ (𝐺 ∈ Plig → ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙))
3		eleq2 2850	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑏 ∈ 𝑙 ↔ 𝑏 ∈ 𝐿))
4		eleq2 2850	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑐 ∈ 𝑙 ↔ 𝑐 ∈ 𝐿))
5		eleq2 2850	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑑 ∈ 𝑙 ↔ 𝑑 ∈ 𝐿))
6	3, 4, 5	3anbi123d 1464	. . . . . . . . 9 ⊢ (𝑙 = 𝐿 → ((𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) ↔ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
7	6	notbid 321	. . . . . . . 8 ⊢ (𝑙 = 𝐿 → (¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) ↔ ¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
8	7	rspccv 3574	. . . . . . 7 ⊢ (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
9		eleq1w 2844	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ 𝐿 ↔ 𝑏 ∈ 𝐿))
10	9	notbid 321	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑏 ∈ 𝐿))
11	10	rspcev 3577	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝑃 ∧ ¬ 𝑏 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
12	11	ex 418	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝑃 → (¬ 𝑏 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
13		eleq1w 2844	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ 𝐿 ↔ 𝑐 ∈ 𝐿))
14	13	notbid 321	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑐 ∈ 𝐿))
15	14	rspcev 3577	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝑃 ∧ ¬ 𝑐 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
16	15	ex 418	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑃 → (¬ 𝑐 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
17		eleq1w 2844	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝑎 ∈ 𝐿 ↔ 𝑑 ∈ 𝐿))
18	17	notbid 321	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑑 ∈ 𝐿))
19	18	rspcev 3577	. . . . . . . . . 10 ⊢ ((𝑑 ∈ 𝑃 ∧ ¬ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
20	19	ex 418	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝑃 → (¬ 𝑑 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
21	12, 16, 20	3jaao 1460	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → ((¬ 𝑏 ∈ 𝐿 ∨ ¬ 𝑐 ∈ 𝐿 ∨ ¬ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
22		3ianor 1124	. . . . . . . 8 ⊢ (¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿) ↔ (¬ 𝑏 ∈ 𝐿 ∨ ¬ 𝑐 ∈ 𝐿 ∨ ¬ 𝑑 ∈ 𝐿))
23		df-nel 3063	. . . . . . . . 9 ⊢ (𝑎 ∉ 𝐿 ↔ ¬ 𝑎 ∈ 𝐿)
24	23	rexbii 3110	. . . . . . . 8 ⊢ (∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿 ↔ ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
25	21, 22, 24	3imtr4g 299	. . . . . . 7 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → (¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
26	8, 25	syl9r 79	. . . . . 6 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)))
27	26	3expia 1139	. . . . 5 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃) → (𝑑 ∈ 𝑃 → (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))))
28	27	rexlimdv 3162	. . . 4 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃) → (∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)))
29	28	rexlimivv 3205	. . 3 ⊢ (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
30	2, 29	syl 18	. 2 ⊢ (𝐺 ∈ Plig → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
31	30	imp 412	1 ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ∉ wnel 3062  ∀wral 3077  ∃wrex 3087  ∪ cuni 4867  Pligcplig 31069

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-v 3453  df-ss 3916  df-uni 4868  df-plig 31070

This theorem is used by: (None)