Definition df-line3 38682

Description: Define the set of all lines. A line is an infinite subset of RR3 that satisfies a PtDf property. (Contributed by Andrew Salmon, 15-Jul-2012.)

Assertion

Ref	Expression
df-line3	|- line3 = { x e. ~P RR3 | ( 2o ~<_ x /\ A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x ) ) }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-line3

Step	Hyp	Ref	Expression
1		cline3 38666	. 2 class line3
2		c2o 7554	. . . . 5 class 2o
3		vx	. . . . . 6 setvar x
4	3	cv 1482	. . . . 5 class x
5		cdom 7953	. . . . 5 class ~<_
6	2, 4, 5	wbr 4653	. . . 4 wff 2o ~<_ x
7		vz	. . . . . . . . 9 setvar z
8	7	cv 1482	. . . . . . . 8 class z
9		vy	. . . . . . . . 9 setvar y
10	9	cv 1482	. . . . . . . 8 class y
11	8, 10	wne 2794	. . . . . . 7 wff z =/= y
12	10, 8	cptdfc 38664	. . . . . . . . 9 class PtDf ( y , z )
13	12	crn 5115	. . . . . . . 8 class ran PtDf ( y , z )
14	13, 4	wceq 1483	. . . . . . 7 wff ran PtDf ( y , z ) = x
15	11, 14	wi 4	. . . . . 6 wff ( z =/= y -> ran PtDf ( y , z ) = x )
16	15, 7, 4	wral 2912	. . . . 5 wff A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x )
17	16, 9, 4	wral 2912	. . . 4 wff A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x )
18	6, 17	wa 384	. . 3 wff ( 2o ~<_ x /\ A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x ) )
19		crr3c 38665	. . . 4 class RR3
20	19	cpw 4158	. . 3 class ~P RR3
21	18, 3, 20	crab 2916	. 2 class { x e. ~P RR3 | ( 2o ~<_ x /\ A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x ) ) }
22	1, 21	wceq 1483	1 wff line3 = { x e. ~P RR3 | ( 2o ~<_ x /\ A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x ) ) }

This definition is referenced by: (None)