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 = \{m \| ((Tr m \land m ⊧ AxExt \land m ⊧ AxPow) \land (m ⊧ AxUn \land m ⊧ AxReg \land m ⊧ AxInf) \land \forall u \in Fmla (ω) m ⊧ AxRep (u))\}$

Step	Hyp	Ref	Expression
0		cgzf	$class ZF$
1		vm	$setvar m$
2	1	cv	$setvar m$
3	2	wtr	$wff Tr m$
4		cprv	$class ⊧$
5		cgze	$class AxExt$
6	2 5 4	wbr	$wff m ⊧ AxExt$
7		cgzp	$class AxPow$
8	2 7 4	wbr	$wff m ⊧ AxPow$
9	3 6 8	w3a	$wff (Tr m \land m ⊧ AxExt \land m ⊧ AxPow)$
10		cgzu	$class AxUn$
11	2 10 4	wbr	$wff m ⊧ AxUn$
12		cgzg	$class AxReg$
13	2 12 4	wbr	$wff m ⊧ AxReg$
14		cgzi	$class AxInf$
15	2 14 4	wbr	$wff m ⊧ AxInf$
16	11 13 15	w3a	$wff (m ⊧ AxUn \land m ⊧ AxReg \land m ⊧ AxInf)$
17		vu	$setvar u$
18		cfmla	$class Fmla$
19		com	$class ω$
20	19 18	cfv	$class Fmla (ω)$
21		cgzr	$class AxRep$
22	17	cv	$setvar u$
23	22 21	cfv	$class AxRep (u)$
24	2 23 4	wbr	$wff m ⊧ AxRep (u)$
25	24 17 20	wral	$wff \forall u \in Fmla (ω) m ⊧ AxRep (u)$
26	9 16 25	w3a	$wff ((Tr m \land m ⊧ AxExt \land m ⊧ AxPow) \land (m ⊧ AxUn \land m ⊧ AxReg \land m ⊧ AxInf) \land \forall u \in Fmla (ω) m ⊧ AxRep (u))$
27	26 1	cab	$class \{m \| ((Tr m \land m ⊧ AxExt \land m ⊧ AxPow) \land (m ⊧ AxUn \land m ⊧ AxReg \land m ⊧ AxInf) \land \forall u \in Fmla (ω) m ⊧ AxRep (u))\}$
28	0 27	wceq	$wff ZF = \{m \| ((Tr m \land m ⊧ AxExt \land m ⊧ AxPow) \land (m ⊧ AxUn \land m ⊧ AxReg \land m ⊧ AxInf) \land \forall u \in Fmla (ω) m ⊧ AxRep (u))\}$

Metamath Proof Explorer