Theorem nsnlplig

Description: There is no "one-point line" in a planar incidence geometry. (Contributed by BJ, 2-Dec-2021) (Proof shortened by AV, 5-Dec-2021)

	Ref	Expression
Assertion	nsnlplig	⊢ ( 𝐺 ∈ Plig → ¬ { 𝐴 } ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐺 = ∪ 𝐺
2	1	l2p	⊢ ( ( 𝐺 ∈ Plig ∧ { 𝐴 } ∈ 𝐺 ) → ∃ 𝑎 ∈ ∪ 𝐺 ∃ 𝑏 ∈ ∪ 𝐺 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) )
3		elsni	⊢ ( 𝑎 ∈ { 𝐴 } → 𝑎 = 𝐴 )
4		elsni	⊢ ( 𝑏 ∈ { 𝐴 } → 𝑏 = 𝐴 )
5		eqtr3	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐴 ) → 𝑎 = 𝑏 )
6		eqneqall	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ≠ 𝑏 → ¬ { 𝐴 } ∈ 𝐺 ) )
7	5 6	syl	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐴 ) → ( 𝑎 ≠ 𝑏 → ¬ { 𝐴 } ∈ 𝐺 ) )
8	3 4 7	syl2an	⊢ ( ( 𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) → ( 𝑎 ≠ 𝑏 → ¬ { 𝐴 } ∈ 𝐺 ) )
9	8	impcom	⊢ ( ( 𝑎 ≠ 𝑏 ∧ ( 𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) ) → ¬ { 𝐴 } ∈ 𝐺 )
10	9	3impb	⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) → ¬ { 𝐴 } ∈ 𝐺 )
11	10	a1i	⊢ ( ( 𝑎 ∈ ∪ 𝐺 ∧ 𝑏 ∈ ∪ 𝐺 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) → ¬ { 𝐴 } ∈ 𝐺 ) )
12	11	rexlimivv	⊢ ( ∃ 𝑎 ∈ ∪ 𝐺 ∃ 𝑏 ∈ ∪ 𝐺 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) → ¬ { 𝐴 } ∈ 𝐺 )
13	2 12	syl	⊢ ( ( 𝐺 ∈ Plig ∧ { 𝐴 } ∈ 𝐺 ) → ¬ { 𝐴 } ∈ 𝐺 )
14	13	pm2.01da	⊢ ( 𝐺 ∈ Plig → ¬ { 𝐴 } ∈ 𝐺 )