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

Definition df-gzrep 30605
 Description: The Godel-set version of the Axiom Scheme of Replacement. Since this is a scheme and not a single axiom, it manifests as a function on wffs, each giving rise to a different axiom. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzrep AxRep = (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3𝑜𝑔1𝑜𝑔2𝑜(∀𝑔1𝑜𝑢𝑔 (2𝑜=𝑔1𝑜)) →𝑔𝑔1𝑜𝑔2𝑜((2𝑜𝑔1𝑜) ↔𝑔𝑔3𝑜((3𝑜𝑔∅)∧𝑔𝑔1𝑜𝑢))))

Detailed syntax breakdown of Definition df-gzrep
StepHypRef Expression
1 cgzr 30598 . 2 class AxRep
2 vu . . 3 setvar 𝑢
3 com 6957 . . . 4 class ω
4 cfmla 30573 . . . 4 class Fmla
53, 4cfv 5804 . . 3 class (Fmla‘ω)
62cv 1474 . . . . . . . . 9 class 𝑢
7 c1o 7440 . . . . . . . . 9 class 1𝑜
86, 7cgol 30571 . . . . . . . 8 class 𝑔1𝑜𝑢
9 c2o 7441 . . . . . . . . 9 class 2𝑜
10 cgoq 30587 . . . . . . . . 9 class =𝑔
119, 7, 10co 6549 . . . . . . . 8 class (2𝑜=𝑔1𝑜)
12 cgoi 30584 . . . . . . . 8 class 𝑔
138, 11, 12co 6549 . . . . . . 7 class (∀𝑔1𝑜𝑢𝑔 (2𝑜=𝑔1𝑜))
1413, 9cgol 30571 . . . . . 6 class 𝑔2𝑜(∀𝑔1𝑜𝑢𝑔 (2𝑜=𝑔1𝑜))
1514, 7cgox 30588 . . . . 5 class 𝑔1𝑜𝑔2𝑜(∀𝑔1𝑜𝑢𝑔 (2𝑜=𝑔1𝑜))
16 c3o 7442 . . . . 5 class 3𝑜
1715, 16cgol 30571 . . . 4 class 𝑔3𝑜𝑔1𝑜𝑔2𝑜(∀𝑔1𝑜𝑢𝑔 (2𝑜=𝑔1𝑜))
18 cgoe 30569 . . . . . . . 8 class 𝑔
199, 7, 18co 6549 . . . . . . 7 class (2𝑜𝑔1𝑜)
20 c0 3874 . . . . . . . . . 10 class
2116, 20, 18co 6549 . . . . . . . . 9 class (3𝑜𝑔∅)
22 cgoa 30583 . . . . . . . . 9 class 𝑔
2321, 8, 22co 6549 . . . . . . . 8 class ((3𝑜𝑔∅)∧𝑔𝑔1𝑜𝑢)
2423, 16cgox 30588 . . . . . . 7 class 𝑔3𝑜((3𝑜𝑔∅)∧𝑔𝑔1𝑜𝑢)
25 cgob 30586 . . . . . . 7 class 𝑔
2619, 24, 25co 6549 . . . . . 6 class ((2𝑜𝑔1𝑜) ↔𝑔𝑔3𝑜((3𝑜𝑔∅)∧𝑔𝑔1𝑜𝑢))
2726, 9cgol 30571 . . . . 5 class 𝑔2𝑜((2𝑜𝑔1𝑜) ↔𝑔𝑔3𝑜((3𝑜𝑔∅)∧𝑔𝑔1𝑜𝑢))
2827, 7cgol 30571 . . . 4 class 𝑔1𝑜𝑔2𝑜((2𝑜𝑔1𝑜) ↔𝑔𝑔3𝑜((3𝑜𝑔∅)∧𝑔𝑔1𝑜𝑢))
2917, 28, 12co 6549 . . 3 class (∀𝑔3𝑜𝑔1𝑜𝑔2𝑜(∀𝑔1𝑜𝑢𝑔 (2𝑜=𝑔1𝑜)) →𝑔𝑔1𝑜𝑔2𝑜((2𝑜𝑔1𝑜) ↔𝑔𝑔3𝑜((3𝑜𝑔∅)∧𝑔𝑔1𝑜𝑢)))
302, 5, 29cmpt 4643 . 2 class (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3𝑜𝑔1𝑜𝑔2𝑜(∀𝑔1𝑜𝑢𝑔 (2𝑜=𝑔1𝑜)) →𝑔𝑔1𝑜𝑔2𝑜((2𝑜𝑔1𝑜) ↔𝑔𝑔3𝑜((3𝑜𝑔∅)∧𝑔𝑔1𝑜𝑢))))
311, 30wceq 1475 1 wff AxRep = (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3𝑜𝑔1𝑜𝑔2𝑜(∀𝑔1𝑜𝑢𝑔 (2𝑜=𝑔1𝑜)) →𝑔𝑔1𝑜𝑔2𝑜((2𝑜𝑔1𝑜) ↔𝑔𝑔3𝑜((3𝑜𝑔∅)∧𝑔𝑔1𝑜𝑢))))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator