Definition df-i1p 7654

Description: Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by Jim Kingdon, 25-Sep-2019.)

Assertion

Ref	Expression
df-i1p	|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.

Distinct variable group:   u, l

Detailed syntax breakdown of Definition df-i1p

Step	Hyp	Ref	Expression
1		c1p 7479	. 2 class 1P
2		vl	. . . . . 6 setvar l
3	2	cv 1394	. . . . 5 class l
4		c1q 7468	. . . . 5 class 1Q
5		cltq 7472	. . . . 5 class <Q
6	3, 4, 5	wbr 4083	. . . 4 wff l <Q 1Q
7	6, 2	cab 2215	. . 3 class { l | l <Q 1Q }
8		vu	. . . . . 6 setvar u
9	8	cv 1394	. . . . 5 class u
10	4, 9, 5	wbr 4083	. . . 4 wff 1Q <Q u
11	10, 8	cab 2215	. . 3 class { u | 1Q <Q u }
12	7, 11	cop 3669	. 2 class <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
13	1, 12	wceq 1395	1 wff 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.

This definition is referenced by:  1pr  7741  1prl  7742  1pru  7743  addnqpr1  7749  caucvgsr  7989  pitonnlem1  8032  recidpipr  8043  nntopi  8081