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-1v∈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-1v=Y-1v
29 28 eleq1d ⊢t=T→mType⁡t-1v∈Fin↔Y-1v∈Fin
30 29 notbid ⊢t=T→¬mType⁡t-1v∈Fin↔¬Y-1v∈Fin
31 26 30 raleqbidv ⊢t=T→∀v∈mVT⁡t¬mType⁡t-1v∈Fin↔∀v∈F¬Y-1v∈Fin
32 24 31 anbi12d ⊢t=T→mAx⁡t⊆mStat⁡t∧∀v∈mVT⁡t¬mType⁡t-1v∈Fin↔A⊆S∧∀v∈F¬Y-1v∈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-1v∈Fin↔C∩V=∅∧Y:V⟶K∧A⊆S∧∀v∈F¬Y-1v∈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-1v∈Fin
35 33 34 elab2g ⊢T∈W→T∈mFS↔C∩V=∅∧Y:V⟶K∧A⊆S∧∀v∈F¬Y-1v∈Fin