Definition df-np 3880

Description: Define the class of positive reals. This is a "temporary" set used in the construction of complex numbers df-c 4034, and is intended to be used only by the construction. Definition 9-3.1 of [Gleason] p. 121.

Assertion

Ref	Expression
df-np	|- P. = {x | (((/) (. x /\ x (. Q.) /\ A.y e. x (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z))}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-np

Step	Hyp	Ref	Expression
1		cnp 3779	. 2 class P.
2		c0 1707	. . . . . 6 class (/)
3		vx	. . . . . . 7 set x
4	3	cv 1089	. . . . . 6 class x
5	2, 4	wpss 1488	. . . . 5 wff (/) (. x
6		cnq 3773	. . . . . 6 class Q.
7	4, 6	wpss 1488	. . . . 5 wff x (. Q.
8	5, 7	wa 196	. . . 4 wff ((/) (. x /\ x (. Q.)
9		vz	. . . . . . . . . 10 set z
10	9	cv 1089	. . . . . . . . 9 class z
11		vy	. . . . . . . . . 10 set y
12	11	cv 1089	. . . . . . . . 9 class y
13		cltq 3778	. . . . . . . . 9 class <Q
14	10, 12, 13	wbr 2054	. . . . . . . 8 wff z <Q y
15	9, 3	wel 803	. . . . . . . 8 wff z e. x
16	14, 15	wi 2	. . . . . . 7 wff (z <Q y -> z e. x)
17	16, 9	wal 672	. . . . . 6 wff A.z(z <Q y -> z e. x)
18	12, 10, 13	wbr 2054	. . . . . . 7 wff y <Q z
19	18, 9, 4	wrex 1202	. . . . . 6 wff E.z e. x y <Q z
20	17, 19	wa 196	. . . . 5 wff (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z)
21	20, 11, 4	wral 1201	. . . 4 wff A.y e. x (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z)
22	8, 21	wa 196	. . 3 wff (((/) (. x /\ x (. Q.) /\ A.y e. x (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z))
23	22, 3	cab 1090	. 2 class {x | (((/) (. x /\ x (. Q.) /\ A.y e. x (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z))}
24	1, 23	wceq 1091	1 wff P. = {x | (((/) (. x /\ x (. Q.) /\ A.y e. x (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z))}

This definition is referenced by:  npex 3885  elnp 3886

metamath.org