Definition df-msa

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

	Ref	Expression
Assertion	df-msa	⊢ mSA = ( 𝑡 ∈ V ↦ { 𝑎 ∈ ( mEx ‘ 𝑡 ) ∣ ( ( m0St ‘ 𝑎 ) ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ∧ Fun ( ◡ ( 2nd ‘ 𝑎 ) ↾ ( mVR ‘ 𝑡 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmsa	⊢ mSA
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		va	⊢ 𝑎
4		cmex	⊢ mEx
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mEx ‘ 𝑡 )
7		cm0s	⊢ m0St
8	3	cv	⊢ 𝑎
9	8 7	cfv	⊢ ( m0St ‘ 𝑎 )
10		cmax	⊢ mAx
11	5 10	cfv	⊢ ( mAx ‘ 𝑡 )
12	9 11	wcel	⊢ ( m0St ‘ 𝑎 ) ∈ ( mAx ‘ 𝑡 )
13		c1st	⊢ 1st
14	8 13	cfv	⊢ ( 1st ‘ 𝑎 )
15		cmvt	⊢ mVT
16	5 15	cfv	⊢ ( mVT ‘ 𝑡 )
17	14 16	wcel	⊢ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 )
18		c2nd	⊢ 2nd
19	8 18	cfv	⊢ ( 2nd ‘ 𝑎 )
20	19	ccnv	⊢ ◡ ( 2nd ‘ 𝑎 )
21		cmvar	⊢ mVR
22	5 21	cfv	⊢ ( mVR ‘ 𝑡 )
23	20 22	cres	⊢ ( ◡ ( 2nd ‘ 𝑎 ) ↾ ( mVR ‘ 𝑡 ) )
24	23	wfun	⊢ Fun ( ◡ ( 2nd ‘ 𝑎 ) ↾ ( mVR ‘ 𝑡 ) )
25	12 17 24	w3a	⊢ ( ( m0St ‘ 𝑎 ) ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ∧ Fun ( ◡ ( 2nd ‘ 𝑎 ) ↾ ( mVR ‘ 𝑡 ) ) )
26	25 3 6	crab	⊢ { 𝑎 ∈ ( mEx ‘ 𝑡 ) ∣ ( ( m0St ‘ 𝑎 ) ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ∧ Fun ( ◡ ( 2nd ‘ 𝑎 ) ↾ ( mVR ‘ 𝑡 ) ) ) }
27	1 2 26	cmpt	⊢ ( 𝑡 ∈ V ↦ { 𝑎 ∈ ( mEx ‘ 𝑡 ) ∣ ( ( m0St ‘ 𝑎 ) ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ∧ Fun ( ◡ ( 2nd ‘ 𝑎 ) ↾ ( mVR ‘ 𝑡 ) ) ) } )
28	0 27	wceq	⊢ mSA = ( 𝑡 ∈ V ↦ { 𝑎 ∈ ( mEx ‘ 𝑡 ) ∣ ( ( m0St ‘ 𝑎 ) ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ∧ Fun ( ◡ ( 2nd ‘ 𝑎 ) ↾ ( mVR ‘ 𝑡 ) ) ) } )