Definition df-i1p 7429

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 = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩

Distinct variable group:   𝑢,𝑙

Detailed syntax breakdown of Definition df-i1p

Step	Hyp	Ref	Expression
1		c1p 7254	. 2 class 1P
2		vl	. . . . . 6 setvar 𝑙
3	2	cv 1347	. . . . 5 class 𝑙
4		c1q 7243	. . . . 5 class 1Q
5		cltq 7247	. . . . 5 class <Q
6	3, 4, 5	wbr 3989	. . . 4 wff 𝑙 <Q 1Q
7	6, 2	cab 2156	. . 3 class {𝑙 ∣ 𝑙 <Q 1Q}
8		vu	. . . . . 6 setvar 𝑢
9	8	cv 1347	. . . . 5 class 𝑢
10	4, 9, 5	wbr 3989	. . . 4 wff 1Q <Q 𝑢
11	10, 8	cab 2156	. . 3 class {𝑢 ∣ 1Q <Q 𝑢}
12	7, 11	cop 3586	. 2 class ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩
13	1, 12	wceq 1348	1 wff 1P = ⟨{𝑙 ∣ 𝑙 <Q 1Q}, {𝑢 ∣ 1Q <Q 𝑢}⟩

This definition is referenced by:  1pr  7516  1prl  7517  1pru  7518  addnqpr1  7524  caucvgsr  7764  pitonnlem1  7807  recidpipr  7818  nntopi  7856