ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-0nq0 Structured version   GIF version

Definition df-0nq0 6408
Description: Define non-negative fraction constant 0. 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, 5-Nov-2019.)
Assertion
Ref Expression
df-0nq0 0Q0 = [⟨∅, 1𝑜⟩] ~Q0

Detailed syntax breakdown of Definition df-0nq0
StepHypRef Expression
1 c0q0 6272 . 2 class 0Q0
2 c0 3218 . . . 4 class
3 c1o 5933 . . . 4 class 1𝑜
42, 3cop 3370 . . 3 class ⟨∅, 1𝑜
5 ceq0 6270 . . 3 class ~Q0
64, 5cec 6040 . 2 class [⟨∅, 1𝑜⟩] ~Q0
71, 6wceq 1242 1 wff 0Q0 = [⟨∅, 1𝑜⟩] ~Q0
Colors of variables: wff set class
This definition is referenced by:  nq0m0r  6438  nq0a0  6439  prarloclem5  6482
  Copyright terms: Public domain W3C validator