df-msa

Description: Define the set of syntax axioms. (Contributed by Mario Carneiro, 14-Jul-2016)

		Ref	Expression
	Assertion	df-msa	$⊢ mSA = (t \in V ⟼ \{a \in mEx (t) \| (m0St (a) \in mAx (t) \land 1^{st} (a) \in mVT (t) \land Fun ({{2^{nd} (a)}^{-1} ↾}_{mVR (t)}))\})$

Step	Hyp	Ref	Expression
0		cmsa	$class mSA$
1		vt	$setvar t$
2		cvv	$class V$
3		va	$setvar a$
4		cmex	$class mEx$
5	1	cv	$setvar t$
6	5 4	cfv	$class mEx (t)$
7		cm0s	$class m0St$
8	3	cv	$setvar a$
9	8 7	cfv	$class m0St (a)$
10		cmax	$class mAx$
11	5 10	cfv	$class mAx (t)$
12	9 11	wcel	$wff m0St (a) \in mAx (t)$
13		c1st	$class 1^{st}$
14	8 13	cfv	$class 1^{st} (a)$
15		cmvt	$class mVT$
16	5 15	cfv	$class mVT (t)$
17	14 16	wcel	$wff 1^{st} (a) \in mVT (t)$
18		c2nd	$class 2^{nd}$
19	8 18	cfv	$class 2^{nd} (a)$
20	19	ccnv	$class {2^{nd} (a)}^{-1}$
21		cmvar	$class mVR$
22	5 21	cfv	$class mVR (t)$
23	20 22	cres	$class ({{2^{nd} (a)}^{-1} ↾}_{mVR (t)})$
24	23	wfun	$wff Fun ({{2^{nd} (a)}^{-1} ↾}_{mVR (t)})$
25	12 17 24	w3a	$wff (m0St (a) \in mAx (t) \land 1^{st} (a) \in mVT (t) \land Fun ({{2^{nd} (a)}^{-1} ↾}_{mVR (t)}))$
26	25 3 6	crab	$class \{a \in mEx (t) \| (m0St (a) \in mAx (t) \land 1^{st} (a) \in mVT (t) \land Fun ({{2^{nd} (a)}^{-1} ↾}_{mVR (t)}))\}$
27	1 2 26	cmpt	$class (t \in V ⟼ \{a \in mEx (t) \| (m0St (a) \in mAx (t) \land 1^{st} (a) \in mVT (t) \land Fun ({{2^{nd} (a)}^{-1} ↾}_{mVR (t)}))\})$
28	0 27	wceq	$wff mSA = (t \in V ⟼ \{a \in mEx (t) \| (m0St (a) \in mAx (t) \land 1^{st} (a) \in mVT (t) \land Fun ({{2^{nd} (a)}^{-1} ↾}_{mVR (t)}))\})$

Metamath Proof Explorer