Metamath Proof Explorer

Theorem isplig

Description: The predicate "is a planar incidence geometry" for sets. (Contributed by FL, 2-Aug-2009)

Ref

Expression

Hypothesis

isplig.1

|- P = U. G

Assertion

|- ( G e. A -> ( 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 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isplig.1	\|- P = U. G
2		unieq	\|- ( x = G -> U. x = U. G )
3	2 1	eqtr4di	\|- ( x = G -> U. x = P )
4		reueq1	\|- ( x = G -> ( E! l e. x ( a e. l /\ b e. l ) <-> E! l e. G ( a e. l /\ b e. l ) ) )
5	4	imbi2d	\|- ( x = G -> ( ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) ) <-> ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) ) )
6	3 5	raleqbidv	\|- ( x = G -> ( A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) ) <-> A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) ) )
7	3 6	raleqbidv	\|- ( x = G -> ( A. a e. U. x A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) ) <-> A. a e. P A. b e. P ( a =/= b -> E! l e. G ( a e. l /\ b e. l ) ) ) )
8	3	rexeqdv	\|- ( x = G -> ( E. b e. U. x ( a =/= b /\ a e. l /\ b e. l ) <-> E. b e. P ( a =/= b /\ a e. l /\ b e. l ) ) )
9	3 8	rexeqbidv	\|- ( x = G -> ( E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l ) <-> E. a e. P E. b e. P ( a =/= b /\ a e. l /\ b e. l ) ) )
10	9	raleqbi1dv	\|- ( x = G -> ( A. l e. x E. a e. U. x E. b e. U. x ( a =/= b /\ 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 ) ) )
11		raleq	\|- ( x = G -> ( A. l e. x -. ( a e. l /\ b e. l /\ c e. l ) <-> A. l e. G -. ( a e. l /\ b e. l /\ c e. l ) ) )
12	3 11	rexeqbidv	\|- ( x = G -> ( E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l ) <-> E. c e. P A. l e. G -. ( a e. l /\ b e. l /\ c e. l ) ) )
13	3 12	rexeqbidv	\|- ( x = G -> ( E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l ) <-> E. b e. P E. c e. P A. l e. G -. ( a e. l /\ b e. l /\ c e. l ) ) )
14	3 13	rexeqbidv	\|- ( x = G -> ( E. a e. U. x E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c 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 ) ) )
15	7 10 14	3anbi123d	\|- ( x = G -> ( ( A. a e. U. x A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) ) /\ A. l e. x E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. U. x E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l ) ) <-> ( 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 ) ) ) )
16		df-plig	\|- Plig = { x \| ( A. a e. U. x A. b e. U. x ( a =/= b -> E! l e. x ( a e. l /\ b e. l ) ) /\ A. l e. x E. a e. U. x E. b e. U. x ( a =/= b /\ a e. l /\ b e. l ) /\ E. a e. U. x E. b e. U. x E. c e. U. x A. l e. x -. ( a e. l /\ b e. l /\ c e. l ) ) }
17	15 16	elab2g	\|- ( G e. A -> ( 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 ) ) ) )