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 ⊢ P = ⋃ G
Assertion lpni ⊢ G ∈ Plig ∧ L ∈ G → ∃ a ∈ P a ∉ L

Proof

Step Hyp Ref Expression
1 l2p.1 ⊢ P = ⋃ G
2 1 tncp ⊢ G ∈ Plig → ∃ b ∈ P ∃ c ∈ P ∃ d ∈ P ∀ l ∈ G ¬ b ∈ l ∧ c ∈ l ∧ d ∈ l
3 eleq2 ⊢ l = L → b ∈ l ↔ b ∈ L
4 eleq2 ⊢ l = L → c ∈ l ↔ c ∈ L
5 eleq2 ⊢ l = L → d ∈ l ↔ d ∈ L
6 3 4 5 3anbi123d ⊢ l = L → b ∈ l ∧ c ∈ l ∧ d ∈ l ↔ b ∈ L ∧ c ∈ L ∧ d ∈ L
7 6 notbid ⊢ l = L → ¬ b ∈ l ∧ c ∈ l ∧ d ∈ l ↔ ¬ b ∈ L ∧ c ∈ L ∧ d ∈ L
8 7 rspccv ⊢ ∀ l ∈ G ¬ b ∈ l ∧ c ∈ l ∧ d ∈ l → L ∈ G → ¬ b ∈ L ∧ c ∈ L ∧ d ∈ L
9 eleq1w ⊢ a = b → a ∈ L ↔ b ∈ L
10 9 notbid ⊢ a = b → ¬ a ∈ L ↔ ¬ b ∈ L
11 10 rspcev ⊢ b ∈ P ∧ ¬ b ∈ L → ∃ a ∈ P ¬ a ∈ L
12 11 ex ⊢ b ∈ P → ¬ b ∈ L → ∃ a ∈ P ¬ a ∈ L
13 eleq1w ⊢ a = c → a ∈ L ↔ c ∈ L
14 13 notbid ⊢ a = c → ¬ a ∈ L ↔ ¬ c ∈ L
15 14 rspcev ⊢ c ∈ P ∧ ¬ c ∈ L → ∃ a ∈ P ¬ a ∈ L
16 15 ex ⊢ c ∈ P → ¬ c ∈ L → ∃ a ∈ P ¬ a ∈ L
17 eleq1w ⊢ a = d → a ∈ L ↔ d ∈ L
18 17 notbid ⊢ a = d → ¬ a ∈ L ↔ ¬ d ∈ L
19 18 rspcev ⊢ d ∈ P ∧ ¬ d ∈ L → ∃ a ∈ P ¬ a ∈ L
20 19 ex ⊢ d ∈ P → ¬ d ∈ L → ∃ a ∈ P ¬ a ∈ L
21 12 16 20 3jaao ⊢ b ∈ P ∧ c ∈ P ∧ d ∈ P → ¬ b ∈ L ∨ ¬ c ∈ L ∨ ¬ d ∈ L → ∃ a ∈ P ¬ a ∈ L
22 3ianor ⊢ ¬ b ∈ L ∧ c ∈ L ∧ d ∈ L ↔ ¬ b ∈ L ∨ ¬ c ∈ L ∨ ¬ d ∈ L
23 df-nel ⊢ a ∉ L ↔ ¬ a ∈ L
24 23 rexbii ⊢ ∃ a ∈ P a ∉ L ↔ ∃ a ∈ P ¬ a ∈ L
25 21 22 24 3imtr4g ⊢ b ∈ P ∧ c ∈ P ∧ d ∈ P → ¬ b ∈ L ∧ c ∈ L ∧ d ∈ L → ∃ a ∈ P a ∉ L
26 8 25 syl9r ⊢ b ∈ P ∧ c ∈ P ∧ d ∈ P → ∀ l ∈ G ¬ b ∈ l ∧ c ∈ l ∧ d ∈ l → L ∈ G → ∃ a ∈ P a ∉ L
27 26 3expia ⊢ b ∈ P ∧ c ∈ P → d ∈ P → ∀ l ∈ G ¬ b ∈ l ∧ c ∈ l ∧ d ∈ l → L ∈ G → ∃ a ∈ P a ∉ L
28 27 rexlimdv ⊢ b ∈ P ∧ c ∈ P → ∃ d ∈ P ∀ l ∈ G ¬ b ∈ l ∧ c ∈ l ∧ d ∈ l → L ∈ G → ∃ a ∈ P a ∉ L
29 28 rexlimivv ⊢ ∃ b ∈ P ∃ c ∈ P ∃ d ∈ P ∀ l ∈ G ¬ b ∈ l ∧ c ∈ l ∧ d ∈ l → L ∈ G → ∃ a ∈ P a ∉ L
30 2 29 syl ⊢ G ∈ Plig → L ∈ G → ∃ a ∈ P a ∉ L
31 30 imp ⊢ G ∈ Plig ∧ L ∈ G → ∃ a ∈ P a ∉ L