Theorem lpni 28515

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 28513	. . 3 ⊢ (𝐺 ∈ Plig → ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙))
3		eleq2 2819	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑏 ∈ 𝑙 ↔ 𝑏 ∈ 𝐿))
4		eleq2 2819	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑐 ∈ 𝑙 ↔ 𝑐 ∈ 𝐿))
5		eleq2 2819	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑑 ∈ 𝑙 ↔ 𝑑 ∈ 𝐿))
6	3, 4, 5	3anbi123d 1438	. . . . . . . . 9 ⊢ (𝑙 = 𝐿 → ((𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) ↔ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
7	6	notbid 321	. . . . . . . 8 ⊢ (𝑙 = 𝐿 → (¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) ↔ ¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
8	7	rspccv 3524	. . . . . . 7 ⊢ (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
9		eleq1w 2813	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ 𝐿 ↔ 𝑏 ∈ 𝐿))
10	9	notbid 321	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑏 ∈ 𝐿))
11	10	rspcev 3527	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝑃 ∧ ¬ 𝑏 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
12	11	ex 416	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝑃 → (¬ 𝑏 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
13		eleq1w 2813	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ 𝐿 ↔ 𝑐 ∈ 𝐿))
14	13	notbid 321	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑐 ∈ 𝐿))
15	14	rspcev 3527	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝑃 ∧ ¬ 𝑐 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
16	15	ex 416	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑃 → (¬ 𝑐 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
17		eleq1w 2813	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝑎 ∈ 𝐿 ↔ 𝑑 ∈ 𝐿))
18	17	notbid 321	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑑 ∈ 𝐿))
19	18	rspcev 3527	. . . . . . . . . 10 ⊢ ((𝑑 ∈ 𝑃 ∧ ¬ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
20	19	ex 416	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝑃 → (¬ 𝑑 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
21	12, 16, 20	3jaao 1435	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → ((¬ 𝑏 ∈ 𝐿 ∨ ¬ 𝑐 ∈ 𝐿 ∨ ¬ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
22		3ianor 1109	. . . . . . . 8 ⊢ (¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿) ↔ (¬ 𝑏 ∈ 𝐿 ∨ ¬ 𝑐 ∈ 𝐿 ∨ ¬ 𝑑 ∈ 𝐿))
23		df-nel 3037	. . . . . . . . 9 ⊢ (𝑎 ∉ 𝐿 ↔ ¬ 𝑎 ∈ 𝐿)
24	23	rexbii 3160	. . . . . . . 8 ⊢ (∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿 ↔ ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
25	21, 22, 24	3imtr4g 299	. . . . . . 7 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → (¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
26	8, 25	syl9r 78	. . . . . 6 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)))
27	26	3expia 1123	. . . . 5 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃) → (𝑑 ∈ 𝑃 → (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))))
28	27	rexlimdv 3192	. . . 4 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃) → (∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)))
29	28	rexlimivv 3201	. . 3 ⊢ (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
30	2, 29	syl 17	. 2 ⊢ (𝐺 ∈ Plig → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
31	30	imp 410	1 ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ w3o 1088   ∧ w3a 1089   = wceq 1543   ∈ wcel 2112   ∉ wnel 3036  ∀wral 3051  ∃wrex 3052  ∪ cuni 4805  Pligcplig 28509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-ex 1788  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-v 3400  df-in 3860  df-ss 3870  df-uni 4806  df-plig 28510

This theorem is referenced by: (None)