This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-nq

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-2.2 of Gleason p. 117. (Contributed by NM, 16-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion df-nq Q = { 𝑥 ∈ ( N × N ) ∣ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnq ⊢ Q
1 vx ⊢ 𝑥
2 cnpi ⊢ N
3 2 2 cxp ⊢ ( N × N )
4 vy ⊢ 𝑦
5 1 cv ⊢ 𝑥
6 ceq ⊢ ~Q
7 4 cv ⊢ 𝑦
8 5 7 6 wbr ⊢ 𝑥 ~Q 𝑦
9 c2nd ⊢ 2nd
10 7 9 cfv ⊢ ( 2nd ‘ 𝑦 )
11 clti ⊢ <N
12 5 9 cfv ⊢ ( 2nd ‘ 𝑥 )
13 10 12 11 wbr ⊢ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 )
14 13 wn ⊢ ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 )
15 8 14 wi ⊢ ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) )
16 15 4 3 wral ⊢ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) )
17 16 1 3 crab ⊢ { 𝑥 ∈ ( N × N ) ∣ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) }
18 0 17 wceq ⊢ Q = { 𝑥 ∈ ( N × N ) ∣ ∀ 𝑦 ∈ ( N × N ) ( 𝑥 ~Q 𝑦 → ¬ ( 2nd ‘ 𝑦 ) <N ( 2nd ‘ 𝑥 ) ) }