Definition df-gzrep

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)

	Ref	Expression
Assertion	df-gzrep	⊢ AxRep = ( 𝑢 ∈ ( Fmla ‘ ω ) ↦ ( ∀𝑔 3o ∃𝑔 1o ∀𝑔 2o ( ∀𝑔 1o 𝑢 →𝑔 ( 2o =𝑔 1o ) ) →𝑔 ∀𝑔 1o ∀𝑔 2o ( ( 2o ∈𝑔 1o ) ↔𝑔 ∃𝑔 3o ( ( 3o ∈𝑔 ∅ ) ∧𝑔 ∀𝑔 1o 𝑢 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgzr	⊢ AxRep
1		vu	⊢ 𝑢
2		cfmla	⊢ Fmla
3		com	⊢ ω
4	3 2	cfv	⊢ ( Fmla ‘ ω )
5		c3o	⊢ 3o
6		c1o	⊢ 1o
7		c2o	⊢ 2o
8	1	cv	⊢ 𝑢
9	8 6	cgol	⊢ ∀𝑔 1o 𝑢
10		cgoi	⊢ →𝑔
11		cgoq	⊢ =𝑔
12	7 6 11	co	⊢ ( 2o =𝑔 1o )
13	9 12 10	co	⊢ ( ∀𝑔 1o 𝑢 →𝑔 ( 2o =𝑔 1o ) )
14	13 7	cgol	⊢ ∀𝑔 2o ( ∀𝑔 1o 𝑢 →𝑔 ( 2o =𝑔 1o ) )
15	14 6	cgox	⊢ ∃𝑔 1o ∀𝑔 2o ( ∀𝑔 1o 𝑢 →𝑔 ( 2o =𝑔 1o ) )
16	15 5	cgol	⊢ ∀𝑔 3o ∃𝑔 1o ∀𝑔 2o ( ∀𝑔 1o 𝑢 →𝑔 ( 2o =𝑔 1o ) )
17		cgoe	⊢ ∈𝑔
18	7 6 17	co	⊢ ( 2o ∈𝑔 1o )
19		cgob	⊢ ↔𝑔
20		c0	⊢ ∅
21	5 20 17	co	⊢ ( 3o ∈𝑔 ∅ )
22		cgoa	⊢ ∧𝑔
23	21 9 22	co	⊢ ( ( 3o ∈𝑔 ∅ ) ∧𝑔 ∀𝑔 1o 𝑢 )
24	23 5	cgox	⊢ ∃𝑔 3o ( ( 3o ∈𝑔 ∅ ) ∧𝑔 ∀𝑔 1o 𝑢 )
25	18 24 19	co	⊢ ( ( 2o ∈𝑔 1o ) ↔𝑔 ∃𝑔 3o ( ( 3o ∈𝑔 ∅ ) ∧𝑔 ∀𝑔 1o 𝑢 ) )
26	25 7	cgol	⊢ ∀𝑔 2o ( ( 2o ∈𝑔 1o ) ↔𝑔 ∃𝑔 3o ( ( 3o ∈𝑔 ∅ ) ∧𝑔 ∀𝑔 1o 𝑢 ) )
27	26 6	cgol	⊢ ∀𝑔 1o ∀𝑔 2o ( ( 2o ∈𝑔 1o ) ↔𝑔 ∃𝑔 3o ( ( 3o ∈𝑔 ∅ ) ∧𝑔 ∀𝑔 1o 𝑢 ) )
28	16 27 10	co	⊢ ( ∀𝑔 3o ∃𝑔 1o ∀𝑔 2o ( ∀𝑔 1o 𝑢 →𝑔 ( 2o =𝑔 1o ) ) →𝑔 ∀𝑔 1o ∀𝑔 2o ( ( 2o ∈𝑔 1o ) ↔𝑔 ∃𝑔 3o ( ( 3o ∈𝑔 ∅ ) ∧𝑔 ∀𝑔 1o 𝑢 ) ) )
29	1 4 28	cmpt	⊢ ( 𝑢 ∈ ( Fmla ‘ ω ) ↦ ( ∀𝑔 3o ∃𝑔 1o ∀𝑔 2o ( ∀𝑔 1o 𝑢 →𝑔 ( 2o =𝑔 1o ) ) →𝑔 ∀𝑔 1o ∀𝑔 2o ( ( 2o ∈𝑔 1o ) ↔𝑔 ∃𝑔 3o ( ( 3o ∈𝑔 ∅ ) ∧𝑔 ∀𝑔 1o 𝑢 ) ) ) )
30	0 29	wceq	⊢ AxRep = ( 𝑢 ∈ ( Fmla ‘ ω ) ↦ ( ∀𝑔 3o ∃𝑔 1o ∀𝑔 2o ( ∀𝑔 1o 𝑢 →𝑔 ( 2o =𝑔 1o ) ) →𝑔 ∀𝑔 1o ∀𝑔 2o ( ( 2o ∈𝑔 1o ) ↔𝑔 ∃𝑔 3o ( ( 3o ∈𝑔 ∅ ) ∧𝑔 ∀𝑔 1o 𝑢 ) ) ) )