Metamath Proof Explorer

Theorem ismfs

Description: A formal system is a tuple <. mCN , mVR , mType , mVT , mTC , mAx >. such that: mCN and mVR are disjoint; mType is a function from mVR to mVT ; mVT is a subset of mTC ; mAx is a set of statements; and for each variable typecode, there are infinitely many variables of that type. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses ismfs.c ⊢ C = mCN ⁡ T
ismfs.v ⊢ V = mVR ⁡ T
ismfs.y ⊢ Y = mType ⁡ T
ismfs.f ⊢ F = mVT ⁡ T
ismfs.k ⊢ K = mTC ⁡ T
ismfs.a ⊢ A = mAx ⁡ T
ismfs.s ⊢ S = mStat ⁡ T
Assertion ismfs ⊢ T ∈ W → T ∈ mFS ↔ C ∩ V = ∅ ∧ Y : V ⟶ K ∧ A ⊆ S ∧ ∀ v ∈ F ¬ Y -1 v ∈ Fin

Proof

Step Hyp Ref Expression
1 ismfs.c ⊢ C = mCN ⁡ T
2 ismfs.v ⊢ V = mVR ⁡ T
3 ismfs.y ⊢ Y = mType ⁡ T
4 ismfs.f ⊢ F = mVT ⁡ T
5 ismfs.k ⊢ K = mTC ⁡ T
6 ismfs.a ⊢ A = mAx ⁡ T
7 ismfs.s ⊢ S = mStat ⁡ T
8 fveq2 ⊢ t = T → mCN ⁡ t = mCN ⁡ T
9 8 1 eqtr4di ⊢ t = T → mCN ⁡ t = C
10 fveq2 ⊢ t = T → mVR ⁡ t = mVR ⁡ T
11 10 2 eqtr4di ⊢ t = T → mVR ⁡ t = V
12 9 11 ineq12d ⊢ t = T → mCN ⁡ t ∩ mVR ⁡ t = C ∩ V
13 12 eqeq1d ⊢ t = T → mCN ⁡ t ∩ mVR ⁡ t = ∅ ↔ C ∩ V = ∅
14 fveq2 ⊢ t = T → mType ⁡ t = mType ⁡ T
15 14 3 eqtr4di ⊢ t = T → mType ⁡ t = Y
16 fveq2 ⊢ t = T → mTC ⁡ t = mTC ⁡ T
17 16 5 eqtr4di ⊢ t = T → mTC ⁡ t = K
18 15 11 17 feq123d ⊢ t = T → mType ⁡ t : mVR ⁡ t ⟶ mTC ⁡ t ↔ Y : V ⟶ K
19 13 18 anbi12d ⊢ t = T → mCN ⁡ t ∩ mVR ⁡ t = ∅ ∧ mType ⁡ t : mVR ⁡ t ⟶ mTC ⁡ t ↔ C ∩ V = ∅ ∧ Y : V ⟶ K
20 fveq2 ⊢ t = T → mAx ⁡ t = mAx ⁡ T
21 20 6 eqtr4di ⊢ t = T → mAx ⁡ t = A
22 fveq2 ⊢ t = T → mStat ⁡ t = mStat ⁡ T
23 22 7 eqtr4di ⊢ t = T → mStat ⁡ t = S
24 21 23 sseq12d ⊢ t = T → mAx ⁡ t ⊆ mStat ⁡ t ↔ A ⊆ S
25 fveq2 ⊢ t = T → mVT ⁡ t = mVT ⁡ T
26 25 4 eqtr4di ⊢ t = T → mVT ⁡ t = F
27 15 cnveqd ⊢ t = T → mType ⁡ t -1 = Y -1
28 27 imaeq1d ⊢ t = T → mType ⁡ t -1 v = Y -1 v
29 28 eleq1d ⊢ t = T → mType ⁡ t -1 v ∈ Fin ↔ Y -1 v ∈ Fin
30 29 notbid ⊢ t = T → ¬ mType ⁡ t -1 v ∈ Fin ↔ ¬ Y -1 v ∈ Fin
31 26 30 raleqbidv ⊢ t = T → ∀ v ∈ mVT ⁡ t ¬ mType ⁡ t -1 v ∈ Fin ↔ ∀ v ∈ F ¬ Y -1 v ∈ Fin
32 24 31 anbi12d ⊢ t = T → mAx ⁡ t ⊆ mStat ⁡ t ∧ ∀ v ∈ mVT ⁡ t ¬ mType ⁡ t -1 v ∈ Fin ↔ A ⊆ S ∧ ∀ v ∈ F ¬ Y -1 v ∈ Fin
33 19 32 anbi12d ⊢ t = T → mCN ⁡ t ∩ mVR ⁡ t = ∅ ∧ mType ⁡ t : mVR ⁡ t ⟶ mTC ⁡ t ∧ mAx ⁡ t ⊆ mStat ⁡ t ∧ ∀ v ∈ mVT ⁡ t ¬ mType ⁡ t -1 v ∈ Fin ↔ C ∩ V = ∅ ∧ Y : V ⟶ K ∧ A ⊆ S ∧ ∀ v ∈ F ¬ Y -1 v ∈ Fin
34 df-mfs ⊢ mFS = t | mCN ⁡ t ∩ mVR ⁡ t = ∅ ∧ mType ⁡ t : mVR ⁡ t ⟶ mTC ⁡ t ∧ mAx ⁡ t ⊆ mStat ⁡ t ∧ ∀ v ∈ mVT ⁡ t ¬ mType ⁡ t -1 v ∈ Fin
35 33 34 elab2g ⊢ T ∈ W → T ∈ mFS ↔ C ∩ V = ∅ ∧ Y : V ⟶ K ∧ A ⊆ S ∧ ∀ v ∈ F ¬ Y -1 v ∈ Fin