Theorem lpni

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

	Ref	Expression
Hypothesis	l2p.1	⊢ 𝑃 = ∪ 𝐺
Assertion	lpni	⊢ ( ( 𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺 ) → ∃ 𝑎 ∈ 𝑃 𝑎 ∉ 𝐿 )

Proof

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