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	$⊢ G \in Plig \to \neg \{A\} \in G$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ G = ⋃ G$
2	1	l2p	$⊢ (G \in Plig \land \{A\} \in G) \to \exists a \in ⋃ G \exists b \in ⋃ G (a \neq b \land a \in \{A\} \land b \in \{A\})$
3		elsni	$⊢ a \in \{A\} \to a = A$
4		elsni	$⊢ b \in \{A\} \to b = A$
5		eqtr3	$⊢ (a = A \land b = A) \to a = b$
6		eqneqall	$⊢ a = b \to (a \neq b \to \neg \{A\} \in G)$
7	5 6	syl	$⊢ (a = A \land b = A) \to (a \neq b \to \neg \{A\} \in G)$
8	3 4 7	syl2an	$⊢ (a \in \{A\} \land b \in \{A\}) \to (a \neq b \to \neg \{A\} \in G)$
9	8	impcom	$⊢ (a \neq b \land (a \in \{A\} \land b \in \{A\})) \to \neg \{A\} \in G$
10	9	3impb	$⊢ (a \neq b \land a \in \{A\} \land b \in \{A\}) \to \neg \{A\} \in G$
11	10	a1i	$⊢ (a \in ⋃ G \land b \in ⋃ G) \to ((a \neq b \land a \in \{A\} \land b \in \{A\}) \to \neg \{A\} \in G)$
12	11	rexlimivv	$⊢ \exists a \in ⋃ G \exists b \in ⋃ G (a \neq b \land a \in \{A\} \land b \in \{A\}) \to \neg \{A\} \in G$
13	2 12	syl	$⊢ (G \in Plig \land \{A\} \in G) \to \neg \{A\} \in G$
14	13	pm2.01da	$⊢ G \in Plig \to \neg \{A\} \in G$

Metamath Proof Explorer