Theorem lpni 28842

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 28840	. . 3 ⊢ (𝐺 ∈ Plig → ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙))
3		eleq2 2827	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑏 ∈ 𝑙 ↔ 𝑏 ∈ 𝐿))
4		eleq2 2827	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑐 ∈ 𝑙 ↔ 𝑐 ∈ 𝐿))
5		eleq2 2827	. . . . . . . . . 10 ⊢ (𝑙 = 𝐿 → (𝑑 ∈ 𝑙 ↔ 𝑑 ∈ 𝐿))
6	3, 4, 5	3anbi123d 1435	. . . . . . . . 9 ⊢ (𝑙 = 𝐿 → ((𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) ↔ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
7	6	notbid 318	. . . . . . . 8 ⊢ (𝑙 = 𝐿 → (¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) ↔ ¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
8	7	rspccv 3558	. . . . . . 7 ⊢ (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿)))
9		eleq1w 2821	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ 𝐿 ↔ 𝑏 ∈ 𝐿))
10	9	notbid 318	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑏 ∈ 𝐿))
11	10	rspcev 3561	. . . . . . . . . 10 ⊢ ((𝑏 ∈ 𝑃 ∧ ¬ 𝑏 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
12	11	ex 413	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝑃 → (¬ 𝑏 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
13		eleq1w 2821	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (𝑎 ∈ 𝐿 ↔ 𝑐 ∈ 𝐿))
14	13	notbid 318	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑐 ∈ 𝐿))
15	14	rspcev 3561	. . . . . . . . . 10 ⊢ ((𝑐 ∈ 𝑃 ∧ ¬ 𝑐 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
16	15	ex 413	. . . . . . . . 9 ⊢ (𝑐 ∈ 𝑃 → (¬ 𝑐 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
17		eleq1w 2821	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑑 → (𝑎 ∈ 𝐿 ↔ 𝑑 ∈ 𝐿))
18	17	notbid 318	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑑 → (¬ 𝑎 ∈ 𝐿 ↔ ¬ 𝑑 ∈ 𝐿))
19	18	rspcev 3561	. . . . . . . . . 10 ⊢ ((𝑑 ∈ 𝑃 ∧ ¬ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
20	19	ex 413	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝑃 → (¬ 𝑑 ∈ 𝐿 → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
21	12, 16, 20	3jaao 1432	. . . . . . . 8 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → ((¬ 𝑏 ∈ 𝐿 ∨ ¬ 𝑐 ∈ 𝐿 ∨ ¬ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿))
22		3ianor 1106	. . . . . . . 8 ⊢ (¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿) ↔ (¬ 𝑏 ∈ 𝐿 ∨ ¬ 𝑐 ∈ 𝐿 ∨ ¬ 𝑑 ∈ 𝐿))
23		df-nel 3050	. . . . . . . . 9 ⊢ (𝑎 ∉ 𝐿 ↔ ¬ 𝑎 ∈ 𝐿)
24	23	rexbii 3181	. . . . . . . 8 ⊢ (∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿 ↔ ∃𝑎 ∈ 𝑃 ¬ 𝑎 ∈ 𝐿)
25	21, 22, 24	3imtr4g 296	. . . . . . 7 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → (¬ (𝑏 ∈ 𝐿 ∧ 𝑐 ∈ 𝐿 ∧ 𝑑 ∈ 𝐿) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
26	8, 25	syl9r 78	. . . . . 6 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃 ∧ 𝑑 ∈ 𝑃) → (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)))
27	26	3expia 1120	. . . . 5 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃) → (𝑑 ∈ 𝑃 → (∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))))
28	27	rexlimdv 3212	. . . 4 ⊢ ((𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃) → (∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)))
29	28	rexlimivv 3221	. . 3 ⊢ (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙 ∧ 𝑑 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
30	2, 29	syl 17	. 2 ⊢ (𝐺 ∈ Plig → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿))
31	30	imp 407	1 ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ w3o 1085   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ∉ wnel 3049  ∀wral 3064  ∃wrex 3065  ∪ cuni 4839  Pligcplig 28836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-ex 1783  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-plig 28837

This theorem is referenced by: (None)