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

Definition df-gzinf 30609
 Description: The Godel-set version of the Axiom of Infinity. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzinf AxInf = ∃𝑔1𝑜((∅∈𝑔1𝑜)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))))

Detailed syntax breakdown of Definition df-gzinf
StepHypRef Expression
1 cgzi 30602 . 2 class AxInf
2 c0 3874 . . . . 5 class
3 c1o 7440 . . . . 5 class 1𝑜
4 cgoe 30569 . . . . 5 class 𝑔
52, 3, 4co 6549 . . . 4 class (∅∈𝑔1𝑜)
6 c2o 7441 . . . . . . 7 class 2𝑜
76, 3, 4co 6549 . . . . . 6 class (2𝑜𝑔1𝑜)
86, 2, 4co 6549 . . . . . . . 8 class (2𝑜𝑔∅)
9 cgoa 30583 . . . . . . . 8 class 𝑔
108, 5, 9co 6549 . . . . . . 7 class ((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))
1110, 2cgox 30588 . . . . . 6 class 𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))
12 cgoi 30584 . . . . . 6 class 𝑔
137, 11, 12co 6549 . . . . 5 class ((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜)))
1413, 6cgol 30571 . . . 4 class 𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜)))
155, 14, 9co 6549 . . 3 class ((∅∈𝑔1𝑜)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))))
1615, 3cgox 30588 . 2 class 𝑔1𝑜((∅∈𝑔1𝑜)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))))
171, 16wceq 1475 1 wff AxInf = ∃𝑔1𝑜((∅∈𝑔1𝑜)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator