Theorem l2p 30201

Description: For any line in a planar incidence geometry, there exist two different points on the line. (Contributed by AV, 28-Nov-2021.)

Hypothesis

Ref	Expression
l2p.1	⊢ 𝑃 = ∪ 𝐺

Assertion

Ref	Expression
l2p	⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿))

Distinct variable groups:   𝑎,𝑏,𝐺   𝐿,𝑎,𝑏   𝑃,𝑎,𝑏

Proof of Theorem l2p

Dummy variables 𝑐 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		l2p.1	. . . . 5 ⊢ 𝑃 = ∪ 𝐺
2	1	isplig 30198	. . . 4 ⊢ (𝐺 ∈ Plig → (𝐺 ∈ Plig ↔ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))))
3		eleq2 2814	. . . . . . . 8 ⊢ (𝑙 = 𝐿 → (𝑎 ∈ 𝑙 ↔ 𝑎 ∈ 𝐿))
4		eleq2 2814	. . . . . . . 8 ⊢ (𝑙 = 𝐿 → (𝑏 ∈ 𝑙 ↔ 𝑏 ∈ 𝐿))
5	3, 4	3anbi23d 1435	. . . . . . 7 ⊢ (𝑙 = 𝐿 → ((𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ↔ (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿)))
6	5	2rexbidv 3211	. . . . . 6 ⊢ (𝑙 = 𝐿 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿)))
7	6	rspccv 3601	. . . . 5 ⊢ (∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿)))
8	7	3ad2ant2 1131	. . . 4 ⊢ ((∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐺 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐺 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐺 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙)) → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿)))
9	2, 8	syl6bi 253	. . 3 ⊢ (𝐺 ∈ Plig → (𝐺 ∈ Plig → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿))))
10	9	pm2.43i 52	. 2 ⊢ (𝐺 ∈ Plig → (𝐿 ∈ 𝐺 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿)))
11	10	imp 406	1 ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝐿 ∧ 𝑏 ∈ 𝐿))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2932  ∀wral 3053  ∃wrex 3062  ∃!wreu 3366  ∪ cuni 4899  Pligcplig 30196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-v 3468  df-in 3947  df-ss 3957  df-uni 4900  df-plig 30197

This theorem is referenced by:  nsnlplig  30203  nsnlpligALT  30204  n0lpligALT  30206