Definition df-gzf

Description: Define the class of all (transitive) models of ZF. (Contributed by Mario Carneiro, 14-Jul-2013)

	Ref	Expression
Assertion	df-gzf	⊢ ZF = { 𝑚 ∣ ( ( Tr 𝑚 ∧ 𝑚 ⊧ AxExt ∧ 𝑚 ⊧ AxPow ) ∧ ( 𝑚 ⊧ AxUn ∧ 𝑚 ⊧ AxReg ∧ 𝑚 ⊧ AxInf ) ∧ ∀ 𝑢 ∈ ( Fmla ‘ ω ) 𝑚 ⊧ ( AxRep ‘ 𝑢 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgzf	⊢ ZF
1		vm	⊢ 𝑚
2	1	cv	⊢ 𝑚
3	2	wtr	⊢ Tr 𝑚
4		cprv	⊢ ⊧
5		cgze	⊢ AxExt
6	2 5 4	wbr	⊢ 𝑚 ⊧ AxExt
7		cgzp	⊢ AxPow
8	2 7 4	wbr	⊢ 𝑚 ⊧ AxPow
9	3 6 8	w3a	⊢ ( Tr 𝑚 ∧ 𝑚 ⊧ AxExt ∧ 𝑚 ⊧ AxPow )
10		cgzu	⊢ AxUn
11	2 10 4	wbr	⊢ 𝑚 ⊧ AxUn
12		cgzg	⊢ AxReg
13	2 12 4	wbr	⊢ 𝑚 ⊧ AxReg
14		cgzi	⊢ AxInf
15	2 14 4	wbr	⊢ 𝑚 ⊧ AxInf
16	11 13 15	w3a	⊢ ( 𝑚 ⊧ AxUn ∧ 𝑚 ⊧ AxReg ∧ 𝑚 ⊧ AxInf )
17		vu	⊢ 𝑢
18		cfmla	⊢ Fmla
19		com	⊢ ω
20	19 18	cfv	⊢ ( Fmla ‘ ω )
21		cgzr	⊢ AxRep
22	17	cv	⊢ 𝑢
23	22 21	cfv	⊢ ( AxRep ‘ 𝑢 )
24	2 23 4	wbr	⊢ 𝑚 ⊧ ( AxRep ‘ 𝑢 )
25	24 17 20	wral	⊢ ∀ 𝑢 ∈ ( Fmla ‘ ω ) 𝑚 ⊧ ( AxRep ‘ 𝑢 )
26	9 16 25	w3a	⊢ ( ( Tr 𝑚 ∧ 𝑚 ⊧ AxExt ∧ 𝑚 ⊧ AxPow ) ∧ ( 𝑚 ⊧ AxUn ∧ 𝑚 ⊧ AxReg ∧ 𝑚 ⊧ AxInf ) ∧ ∀ 𝑢 ∈ ( Fmla ‘ ω ) 𝑚 ⊧ ( AxRep ‘ 𝑢 ) )
27	26 1	cab	⊢ { 𝑚 ∣ ( ( Tr 𝑚 ∧ 𝑚 ⊧ AxExt ∧ 𝑚 ⊧ AxPow ) ∧ ( 𝑚 ⊧ AxUn ∧ 𝑚 ⊧ AxReg ∧ 𝑚 ⊧ AxInf ) ∧ ∀ 𝑢 ∈ ( Fmla ‘ ω ) 𝑚 ⊧ ( AxRep ‘ 𝑢 ) ) }
28	0 27	wceq	⊢ ZF = { 𝑚 ∣ ( ( Tr 𝑚 ∧ 𝑚 ⊧ AxExt ∧ 𝑚 ⊧ AxPow ) ∧ ( 𝑚 ⊧ AxUn ∧ 𝑚 ⊧ AxReg ∧ 𝑚 ⊧ AxInf ) ∧ ∀ 𝑢 ∈ ( Fmla ‘ ω ) 𝑚 ⊧ ( AxRep ‘ 𝑢 ) ) }