Theorem l2p

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

	Ref	Expression
Hypothesis	l2p.1	|- P = U. G
Assertion	l2p	|- ( ( G e. Plig /\ L e. G ) -> E. a e. P E. b e. P ( a =/= b /\ a e. L /\ b e. L ) )

Proof

Step	Hyp	Ref	Expression
1		l2p.1	|- P = U. G
2	1	isplig	|- ( G e. Plig -> ( G e. Plig <-> ( A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) /\ A. l e. G E. a e. P E. b e. P ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. P E. b e. P E. c e. P A. l e. G -. ( a e. l /\ b e. l /\ c e. l ) ) ) )
3		eleq2	|- ( l = L -> ( a e. l <-> a e. L ) )
4		eleq2	|- ( l = L -> ( b e. l <-> b e. L ) )
5	3 4	3anbi23d	|- ( l = L -> ( ( a =/= b /\ a e. l /\ b e. l ) <-> ( a =/= b /\ a e. L /\ b e. L ) ) )
6	5	2rexbidv	|- ( l = L -> ( E. a e. P E. b e. P ( a =/= b /\ a e. l /\ b e. l ) <-> E. a e. P E. b e. P ( a =/= b /\ a e. L /\ b e. L ) ) )
7	6	rspccv	|- ( A. l e. G E. a e. P E. b e. P ( a =/= b /\ a e. l /\ b e. l ) -> ( L e. G -> E. a e. P E. b e. P ( a =/= b /\ a e. L /\ b e. L ) ) )
8	7	3ad2ant2	|- ( ( A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) /\ A. l e. G E. a e. P E. b e. P ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. P E. b e. P E. c e. P A. l e. G -. ( a e. l /\ b e. l /\ c e. l ) ) -> ( L e. G -> E. a e. P E. b e. P ( a =/= b /\ a e. L /\ b e. L ) ) )
9	2 8	syl6bi	|- ( G e. Plig -> ( G e. Plig -> ( L e. G -> E. a e. P E. b e. P ( a =/= b /\ a e. L /\ b e. L ) ) ) )
10	9	pm2.43i	|- ( G e. Plig -> ( L e. G -> E. a e. P E. b e. P ( a =/= b /\ a e. L /\ b e. L ) ) )
11	10	imp	|- ( ( G e. Plig /\ L e. G ) -> E. a e. P E. b e. P ( a =/= b /\ a e. L /\ b e. L ) )