Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gzreg Structured version   Visualization version   GIF version

Definition df-gzreg 30608
 Description: The Godel-set version of the Axiom of Regularity. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzreg AxReg = (∃𝑔1𝑜(1𝑜𝑔∅) →𝑔𝑔1𝑜((1𝑜𝑔∅)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔 ¬𝑔(2𝑜𝑔∅))))

Detailed syntax breakdown of Definition df-gzreg
StepHypRef Expression
1 cgzg 30601 . 2 class AxReg
2 c1o 7440 . . . . 5 class 1𝑜
3 c0 3874 . . . . 5 class
4 cgoe 30569 . . . . 5 class 𝑔
52, 3, 4co 6549 . . . 4 class (1𝑜𝑔∅)
65, 2cgox 30588 . . 3 class 𝑔1𝑜(1𝑜𝑔∅)
7 c2o 7441 . . . . . . . 8 class 2𝑜
87, 2, 4co 6549 . . . . . . 7 class (2𝑜𝑔1𝑜)
97, 3, 4co 6549 . . . . . . . 8 class (2𝑜𝑔∅)
109cgon 30582 . . . . . . 7 class ¬𝑔(2𝑜𝑔∅)
11 cgoi 30584 . . . . . . 7 class 𝑔
128, 10, 11co 6549 . . . . . 6 class ((2𝑜𝑔1𝑜) →𝑔 ¬𝑔(2𝑜𝑔∅))
1312, 7cgol 30571 . . . . 5 class 𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔 ¬𝑔(2𝑜𝑔∅))
14 cgoa 30583 . . . . 5 class 𝑔
155, 13, 14co 6549 . . . 4 class ((1𝑜𝑔∅)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔 ¬𝑔(2𝑜𝑔∅)))
1615, 2cgox 30588 . . 3 class 𝑔1𝑜((1𝑜𝑔∅)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔 ¬𝑔(2𝑜𝑔∅)))
176, 16, 11co 6549 . 2 class (∃𝑔1𝑜(1𝑜𝑔∅) →𝑔𝑔1𝑜((1𝑜𝑔∅)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔 ¬𝑔(2𝑜𝑔∅))))
181, 17wceq 1475 1 wff AxReg = (∃𝑔1𝑜(1𝑜𝑔∅) →𝑔𝑔1𝑜((1𝑜𝑔∅)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔 ¬𝑔(2𝑜𝑔∅))))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator