Theorem lpni 28743

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 28741	. . 3 ⊢ (𝐺 ∈ Plig → ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙))
3		eleq2 2827	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑏 ∈ 𝑙 ↔ 𝑏 ∈ 𝐿))
4		eleq2 2827	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑐 ∈ 𝑙 ↔ 𝑐 ∈ 𝐿))
5		eleq2 2827	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑑 ∈ 𝑙 ↔ 𝑑 ∈ 𝐿))
6	3, 4, 5	3anbi123d 1434	. . . . . . . . 9 ⊢ (𝑙 = 𝐿 → ((𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) ↔ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
7	6	notbid 317	. . . . . . . 8 ⊢ (𝑙 = 𝐿 → (¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) ↔ ¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
8	7	rspccv 3549	. . . . . . 7 ⊢ (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
9		eleq1w 2821	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ 𝐿 ↔ 𝑏 ∈ 𝐿))
10	9	notbid 317	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑏 ∈ 𝐿))
11	10	rspcev 3552	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝑃 ∧ ¬ 𝑏 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
12	11	ex 412	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝑃 → (¬ 𝑏 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
13		eleq1w 2821	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ 𝐿 ↔ 𝑐 ∈ 𝐿))
14	13	notbid 317	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑐 ∈ 𝐿))
15	14	rspcev 3552	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝑃 ∧ ¬ 𝑐 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
16	15	ex 412	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑃 → (¬ 𝑐 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
17		eleq1w 2821	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝑎 ∈ 𝐿 ↔ 𝑑 ∈ 𝐿))
18	17	notbid 317	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑑 ∈ 𝐿))
19	18	rspcev 3552	. . . . . . . . . 10 ⊢ ((𝑑 ∈ 𝑃 ∧ ¬ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
20	19	ex 412	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝑃 → (¬ 𝑑 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
21	12, 16, 20	3jaao 1431	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → ((¬ 𝑏 ∈ 𝐿 ∨ ¬ 𝑐 ∈ 𝐿 ∨ ¬ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
22		3ianor 1105	. . . . . . . 8 ⊢ (¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿) ↔ (¬ 𝑏 ∈ 𝐿 ∨ ¬ 𝑐 ∈ 𝐿 ∨ ¬ 𝑑 ∈ 𝐿))
23		df-nel 3049	. . . . . . . . 9 ⊢ (𝑎 ∉ 𝐿 ↔ ¬ 𝑎 ∈ 𝐿)
24	23	rexbii 3177	. . . . . . . 8 ⊢ (∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿 ↔ ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
25	21, 22, 24	3imtr4g 295	. . . . . . 7 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → (¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
26	8, 25	syl9r 78	. . . . . 6 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)))
27	26	3expia 1119	. . . . 5 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃) → (𝑑 ∈ 𝑃 → (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))))
28	27	rexlimdv 3211	. . . 4 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃) → (∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)))
29	28	rexlimivv 3220	. . 3 ⊢ (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
30	2, 29	syl 17	. 2 ⊢ (𝐺 ∈ Plig → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
31	30	imp 406	1 ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ w3o 1084   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ∉ wnel 3048  ∀wral 3063  ∃wrex 3064  ∪ cuni 4836  Pligcplig 28737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-plig 28738

This theorem is referenced by: (None)