# Metamath Proof Explorer

## 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 ∧ 𝐿𝐺 ) → ∃ 𝑎𝑃 𝑎𝐿 )