Metamath Proof Explorer

Definition df-msa

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

Ref Expression
Assertion df-msa ⊢ mSA = t ∈ V ⟼ a ∈ mEx ⁡ t | m0St ⁡ a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t ∧ Fun ⁡ 2 nd ⁡ a -1 ↾ mVR ⁡ t

Detailed syntax breakdown

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 ∈ 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 ∈ 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 ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t ∧ Fun ⁡ 2 nd ⁡ a -1 ↾ mVR ⁡ t
26 25 3 6 crab class a ∈ mEx ⁡ t | m0St ⁡ a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t ∧ Fun ⁡ 2 nd ⁡ a -1 ↾ mVR ⁡ t
27 1 2 26 cmpt class t ∈ V ⟼ a ∈ mEx ⁡ t | m0St ⁡ a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t ∧ Fun ⁡ 2 nd ⁡ a -1 ↾ mVR ⁡ t
28 0 27 wceq wff mSA = t ∈ V ⟼ a ∈ mEx ⁡ t | m0St ⁡ a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t ∧ Fun ⁡ 2 nd ⁡ a -1 ↾ mVR ⁡ t