Step |
Hyp |
Ref |
Expression |
1 |
|
maxsta.a |
⊢ 𝐴 = ( mAx ‘ 𝑇 ) |
2 |
|
maxsta.s |
⊢ 𝑆 = ( mStat ‘ 𝑇 ) |
3 |
|
eqid |
⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 ) |
4 |
|
eqid |
⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 ) |
5 |
|
eqid |
⊢ ( mType ‘ 𝑇 ) = ( mType ‘ 𝑇 ) |
6 |
|
eqid |
⊢ ( mVT ‘ 𝑇 ) = ( mVT ‘ 𝑇 ) |
7 |
|
eqid |
⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 ) |
8 |
3 4 5 6 7 1 2
|
ismfs |
⊢ ( 𝑇 ∈ mFS → ( 𝑇 ∈ mFS ↔ ( ( ( ( mCN ‘ 𝑇 ) ∩ ( mVR ‘ 𝑇 ) ) = ∅ ∧ ( mType ‘ 𝑇 ) : ( mVR ‘ 𝑇 ) ⟶ ( mTC ‘ 𝑇 ) ) ∧ ( 𝐴 ⊆ 𝑆 ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑇 ) ¬ ( ◡ ( mType ‘ 𝑇 ) “ { 𝑣 } ) ∈ Fin ) ) ) ) |
9 |
8
|
ibi |
⊢ ( 𝑇 ∈ mFS → ( ( ( ( mCN ‘ 𝑇 ) ∩ ( mVR ‘ 𝑇 ) ) = ∅ ∧ ( mType ‘ 𝑇 ) : ( mVR ‘ 𝑇 ) ⟶ ( mTC ‘ 𝑇 ) ) ∧ ( 𝐴 ⊆ 𝑆 ∧ ∀ 𝑣 ∈ ( mVT ‘ 𝑇 ) ¬ ( ◡ ( mType ‘ 𝑇 ) “ { 𝑣 } ) ∈ Fin ) ) ) |
10 |
9
|
simprld |
⊢ ( 𝑇 ∈ mFS → 𝐴 ⊆ 𝑆 ) |