| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | abid 2718 | . . . . . . . 8
⊢ (𝑐 ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ↔ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))) | 
| 2 |  | intss1 4963 | . . . . . . . 8
⊢ (𝑐 ∈ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} → ∩
{𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝑐) | 
| 3 | 1, 2 | sylbir 235 | . . . . . . 7
⊢ (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → ∩
{𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝑐) | 
| 4 |  | mclsval.d | . . . . . . . . 9
⊢ 𝐷 = (mDV‘𝑇) | 
| 5 |  | mclsval.e | . . . . . . . . 9
⊢ 𝐸 = (mEx‘𝑇) | 
| 6 |  | mclsval.c | . . . . . . . . 9
⊢ 𝐶 = (mCls‘𝑇) | 
| 7 |  | mclsval.1 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ mFS) | 
| 8 |  | mclsval.2 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ⊆ 𝐷) | 
| 9 |  | mclsval.3 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆ 𝐸) | 
| 10 |  | mclsax.h | . . . . . . . . 9
⊢ 𝐻 = (mVH‘𝑇) | 
| 11 |  | mclsax.a | . . . . . . . . 9
⊢ 𝐴 = (mAx‘𝑇) | 
| 12 |  | mclsax.l | . . . . . . . . 9
⊢ 𝐿 = (mSubst‘𝑇) | 
| 13 |  | mclsax.w | . . . . . . . . 9
⊢ 𝑊 = (mVars‘𝑇) | 
| 14 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | mclsval 35568 | . . . . . . . 8
⊢ (𝜑 → (𝐾𝐶𝐵) = ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))}) | 
| 15 | 14 | sseq1d 4015 | . . . . . . 7
⊢ (𝜑 → ((𝐾𝐶𝐵) ⊆ 𝑐 ↔ ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ⊆ 𝑐)) | 
| 16 | 3, 15 | imbitrrid 246 | . . . . . 6
⊢ (𝜑 → (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → (𝐾𝐶𝐵) ⊆ 𝑐)) | 
| 17 |  | sstr2 3990 | . . . . . . . . . . . . . . 15
⊢ ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) → ((𝐾𝐶𝐵) ⊆ 𝑐 → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐)) | 
| 18 | 17 | com12 32 | . . . . . . . . . . . . . 14
⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐)) | 
| 19 | 18 | anim1d 611 | . . . . . . . . . . . . 13
⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)))) | 
| 20 | 19 | imim1d 82 | . . . . . . . . . . . 12
⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → ((((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) | 
| 21 | 20 | ralimdv 3169 | . . . . . . . . . . 11
⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) | 
| 22 | 21 | imim2d 57 | . . . . . . . . . 10
⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → ((〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))) | 
| 23 | 22 | alimdv 1916 | . . . . . . . . 9
⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → (∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → ∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))) | 
| 24 | 23 | 2alimdv 1918 | . . . . . . . 8
⊢ ((𝐾𝐶𝐵) ⊆ 𝑐 → (∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))) | 
| 25 | 24 | com12 32 | . . . . . . 7
⊢
(∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → ((𝐾𝐶𝐵) ⊆ 𝑐 → ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))) | 
| 26 | 25 | adantl 481 | . . . . . 6
⊢ (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → ((𝐾𝐶𝐵) ⊆ 𝑐 → ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))) | 
| 27 | 16, 26 | sylcom 30 | . . . . 5
⊢ (𝜑 → (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))) | 
| 28 |  | eqid 2737 | . . . . . . . 8
⊢
(mPreSt‘𝑇) =
(mPreSt‘𝑇) | 
| 29 |  | eqid 2737 | . . . . . . . 8
⊢
(mStat‘𝑇) =
(mStat‘𝑇) | 
| 30 | 28, 29 | mstapst 35552 | . . . . . . 7
⊢
(mStat‘𝑇)
⊆ (mPreSt‘𝑇) | 
| 31 | 11, 29 | maxsta 35559 | . . . . . . . . 9
⊢ (𝑇 ∈ mFS → 𝐴 ⊆ (mStat‘𝑇)) | 
| 32 | 7, 31 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ (mStat‘𝑇)) | 
| 33 |  | mclsax.4 | . . . . . . . 8
⊢ (𝜑 → 〈𝑀, 𝑂, 𝑃〉 ∈ 𝐴) | 
| 34 | 32, 33 | sseldd 3984 | . . . . . . 7
⊢ (𝜑 → 〈𝑀, 𝑂, 𝑃〉 ∈ (mStat‘𝑇)) | 
| 35 | 30, 34 | sselid 3981 | . . . . . 6
⊢ (𝜑 → 〈𝑀, 𝑂, 𝑃〉 ∈ (mPreSt‘𝑇)) | 
| 36 | 28 | mpstrcl 35546 | . . . . . 6
⊢
(〈𝑀, 𝑂, 𝑃〉 ∈ (mPreSt‘𝑇) → (𝑀 ∈ V ∧ 𝑂 ∈ V ∧ 𝑃 ∈ V)) | 
| 37 |  | simp1 1137 | . . . . . . . . . 10
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → 𝑚 = 𝑀) | 
| 38 |  | simp2 1138 | . . . . . . . . . 10
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → 𝑜 = 𝑂) | 
| 39 |  | simp3 1139 | . . . . . . . . . 10
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) | 
| 40 | 37, 38, 39 | oteq123d 4888 | . . . . . . . . 9
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → 〈𝑚, 𝑜, 𝑝〉 = 〈𝑀, 𝑂, 𝑃〉) | 
| 41 | 40 | eleq1d 2826 | . . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 ↔ 〈𝑀, 𝑂, 𝑃〉 ∈ 𝐴)) | 
| 42 | 38 | uneq1d 4167 | . . . . . . . . . . . . 13
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (𝑜 ∪ ran 𝐻) = (𝑂 ∪ ran 𝐻)) | 
| 43 | 42 | imaeq2d 6078 | . . . . . . . . . . . 12
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (𝑠 “ (𝑜 ∪ ran 𝐻)) = (𝑠 “ (𝑂 ∪ ran 𝐻))) | 
| 44 | 43 | sseq1d 4015 | . . . . . . . . . . 11
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ↔ (𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵))) | 
| 45 | 37 | breqd 5154 | . . . . . . . . . . . . 13
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (𝑥𝑚𝑦 ↔ 𝑥𝑀𝑦)) | 
| 46 | 45 | imbi1d 341 | . . . . . . . . . . . 12
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) ↔ (𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾))) | 
| 47 | 46 | 2albidv 1923 | . . . . . . . . . . 11
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) ↔ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾))) | 
| 48 | 44, 47 | anbi12d 632 | . . . . . . . . . 10
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) ↔ ((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)))) | 
| 49 | 39 | fveq2d 6910 | . . . . . . . . . . 11
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (𝑠‘𝑝) = (𝑠‘𝑃)) | 
| 50 | 49 | eleq1d 2826 | . . . . . . . . . 10
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((𝑠‘𝑝) ∈ 𝑐 ↔ (𝑠‘𝑃) ∈ 𝑐)) | 
| 51 | 48, 50 | imbi12d 344 | . . . . . . . . 9
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) ↔ (((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐))) | 
| 52 | 51 | ralbidv 3178 | . . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐) ↔ ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐))) | 
| 53 | 41, 52 | imbi12d 344 | . . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑜 = 𝑂 ∧ 𝑝 = 𝑃) → ((〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) ↔ (〈𝑀, 𝑂, 𝑃〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐)))) | 
| 54 | 53 | spc3gv 3604 | . . . . . 6
⊢ ((𝑀 ∈ V ∧ 𝑂 ∈ V ∧ 𝑃 ∈ V) → (∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → (〈𝑀, 𝑂, 𝑃〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐)))) | 
| 55 | 35, 36, 54 | 3syl 18 | . . . . 5
⊢ (𝜑 → (∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)) → (〈𝑀, 𝑂, 𝑃〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐)))) | 
| 56 |  | elun 4153 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑂 ∪ ran 𝐻) ↔ (𝑥 ∈ 𝑂 ∨ 𝑥 ∈ ran 𝐻)) | 
| 57 |  | mclsax.6 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) | 
| 58 |  | mclsax.7 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)) | 
| 59 | 58 | ralrimiva 3146 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑣 ∈ 𝑉 (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵)) | 
| 60 |  | mclsax.v | . . . . . . . . . . . . . . . . 17
⊢ 𝑉 = (mVR‘𝑇) | 
| 61 | 60, 5, 10 | mvhf 35563 | . . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸) | 
| 62 | 7, 61 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻:𝑉⟶𝐸) | 
| 63 |  | ffn 6736 | . . . . . . . . . . . . . . 15
⊢ (𝐻:𝑉⟶𝐸 → 𝐻 Fn 𝑉) | 
| 64 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝐻‘𝑣) → (𝑆‘𝑥) = (𝑆‘(𝐻‘𝑣))) | 
| 65 | 64 | eleq1d 2826 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐻‘𝑣) → ((𝑆‘𝑥) ∈ (𝐾𝐶𝐵) ↔ (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵))) | 
| 66 | 65 | ralrn 7108 | . . . . . . . . . . . . . . 15
⊢ (𝐻 Fn 𝑉 → (∀𝑥 ∈ ran 𝐻(𝑆‘𝑥) ∈ (𝐾𝐶𝐵) ↔ ∀𝑣 ∈ 𝑉 (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵))) | 
| 67 | 62, 63, 66 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (∀𝑥 ∈ ran 𝐻(𝑆‘𝑥) ∈ (𝐾𝐶𝐵) ↔ ∀𝑣 ∈ 𝑉 (𝑆‘(𝐻‘𝑣)) ∈ (𝐾𝐶𝐵))) | 
| 68 | 59, 67 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ ran 𝐻(𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) | 
| 69 | 68 | r19.21bi 3251 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝐻) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) | 
| 70 | 57, 69 | jaodan 960 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑂 ∨ 𝑥 ∈ ran 𝐻)) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) | 
| 71 | 56, 70 | sylan2b 594 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑂 ∪ ran 𝐻)) → (𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) | 
| 72 | 71 | ralrimiva 3146 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (𝑂 ∪ ran 𝐻)(𝑆‘𝑥) ∈ (𝐾𝐶𝐵)) | 
| 73 |  | mclsax.5 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ ran 𝐿) | 
| 74 | 12, 5 | msubf 35537 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ ran 𝐿 → 𝑆:𝐸⟶𝐸) | 
| 75 | 73, 74 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆:𝐸⟶𝐸) | 
| 76 | 75 | ffund 6740 | . . . . . . . . . 10
⊢ (𝜑 → Fun 𝑆) | 
| 77 | 4, 5, 28 | elmpst 35541 | . . . . . . . . . . . . . . 15
⊢
(〈𝑀, 𝑂, 𝑃〉 ∈ (mPreSt‘𝑇) ↔ ((𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀) ∧ (𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin) ∧ 𝑃 ∈ 𝐸)) | 
| 78 | 35, 77 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀) ∧ (𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin) ∧ 𝑃 ∈ 𝐸)) | 
| 79 | 78 | simp2d 1144 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin)) | 
| 80 | 79 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑂 ⊆ 𝐸) | 
| 81 | 75 | fdmd 6746 | . . . . . . . . . . . 12
⊢ (𝜑 → dom 𝑆 = 𝐸) | 
| 82 | 80, 81 | sseqtrrd 4021 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑂 ⊆ dom 𝑆) | 
| 83 | 62 | frnd 6744 | . . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐻 ⊆ 𝐸) | 
| 84 | 83, 81 | sseqtrrd 4021 | . . . . . . . . . . 11
⊢ (𝜑 → ran 𝐻 ⊆ dom 𝑆) | 
| 85 | 82, 84 | unssd 4192 | . . . . . . . . . 10
⊢ (𝜑 → (𝑂 ∪ ran 𝐻) ⊆ dom 𝑆) | 
| 86 |  | funimass4 6973 | . . . . . . . . . 10
⊢ ((Fun
𝑆 ∧ (𝑂 ∪ ran 𝐻) ⊆ dom 𝑆) → ((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ↔ ∀𝑥 ∈ (𝑂 ∪ ran 𝐻)(𝑆‘𝑥) ∈ (𝐾𝐶𝐵))) | 
| 87 | 76, 85, 86 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ↔ ∀𝑥 ∈ (𝑂 ∪ ran 𝐻)(𝑆‘𝑥) ∈ (𝐾𝐶𝐵))) | 
| 88 | 72, 87 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → (𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵)) | 
| 89 |  | mclsax.8 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏) | 
| 90 | 89 | 3exp2 1355 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥𝑀𝑦 → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))) → 𝑎𝐾𝑏)))) | 
| 91 | 90 | imp4b 421 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥𝑀𝑦) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))) → 𝑎𝐾𝑏)) | 
| 92 | 91 | ralrimivv 3200 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥𝑀𝑦) → ∀𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥)))∀𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))𝑎𝐾𝑏) | 
| 93 |  | dfss3 3972 | . . . . . . . . . . . 12
⊢ (((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾 ↔ ∀𝑧 ∈ ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦))))𝑧 ∈ 𝐾) | 
| 94 |  | eleq1 2829 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑎, 𝑏〉 → (𝑧 ∈ 𝐾 ↔ 〈𝑎, 𝑏〉 ∈ 𝐾)) | 
| 95 |  | df-br 5144 | . . . . . . . . . . . . . 14
⊢ (𝑎𝐾𝑏 ↔ 〈𝑎, 𝑏〉 ∈ 𝐾) | 
| 96 | 94, 95 | bitr4di 289 | . . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑎, 𝑏〉 → (𝑧 ∈ 𝐾 ↔ 𝑎𝐾𝑏)) | 
| 97 | 96 | ralxp 5852 | . . . . . . . . . . . 12
⊢
(∀𝑧 ∈
((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦))))𝑧 ∈ 𝐾 ↔ ∀𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥)))∀𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))𝑎𝐾𝑏) | 
| 98 | 93, 97 | bitri 275 | . . . . . . . . . . 11
⊢ (((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾 ↔ ∀𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥)))∀𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))𝑎𝐾𝑏) | 
| 99 | 92, 98 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥𝑀𝑦) → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾) | 
| 100 | 99 | ex 412 | . . . . . . . . 9
⊢ (𝜑 → (𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)) | 
| 101 | 100 | alrimivv 1928 | . . . . . . . 8
⊢ (𝜑 → ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)) | 
| 102 | 88, 101 | jca 511 | . . . . . . 7
⊢ (𝜑 → ((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾))) | 
| 103 |  | imaeq1 6073 | . . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → (𝑠 “ (𝑂 ∪ ran 𝐻)) = (𝑆 “ (𝑂 ∪ ran 𝐻))) | 
| 104 | 103 | sseq1d 4015 | . . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → ((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ↔ (𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵))) | 
| 105 |  | fveq1 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑆 → (𝑠‘(𝐻‘𝑥)) = (𝑆‘(𝐻‘𝑥))) | 
| 106 | 105 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑆 → (𝑊‘(𝑠‘(𝐻‘𝑥))) = (𝑊‘(𝑆‘(𝐻‘𝑥)))) | 
| 107 |  | fveq1 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑆 → (𝑠‘(𝐻‘𝑦)) = (𝑆‘(𝐻‘𝑦))) | 
| 108 | 107 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑆 → (𝑊‘(𝑠‘(𝐻‘𝑦))) = (𝑊‘(𝑆‘(𝐻‘𝑦)))) | 
| 109 | 106, 108 | xpeq12d 5716 | . . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑆 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) = ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦))))) | 
| 110 | 109 | sseq1d 4015 | . . . . . . . . . . . . 13
⊢ (𝑠 = 𝑆 → (((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾 ↔ ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)) | 
| 111 | 110 | imbi2d 340 | . . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → ((𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) ↔ (𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾))) | 
| 112 | 111 | 2albidv 1923 | . . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾) ↔ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾))) | 
| 113 | 104, 112 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) ↔ ((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)))) | 
| 114 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (𝑠‘𝑃) = (𝑆‘𝑃)) | 
| 115 | 114 | eleq1d 2826 | . . . . . . . . . 10
⊢ (𝑠 = 𝑆 → ((𝑠‘𝑃) ∈ 𝑐 ↔ (𝑆‘𝑃) ∈ 𝑐)) | 
| 116 | 113, 115 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑠 = 𝑆 → ((((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐) ↔ (((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑆‘𝑃) ∈ 𝑐))) | 
| 117 | 116 | rspcv 3618 | . . . . . . . 8
⊢ (𝑆 ∈ ran 𝐿 → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐) → (((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑆‘𝑃) ∈ 𝑐))) | 
| 118 | 73, 117 | syl 17 | . . . . . . 7
⊢ (𝜑 → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐) → (((𝑆 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑆‘(𝐻‘𝑥))) × (𝑊‘(𝑆‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑆‘𝑃) ∈ 𝑐))) | 
| 119 | 102, 118 | mpid 44 | . . . . . 6
⊢ (𝜑 → (∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐) → (𝑆‘𝑃) ∈ 𝑐)) | 
| 120 | 33, 119 | embantd 59 | . . . . 5
⊢ (𝜑 → ((〈𝑀, 𝑂, 𝑃〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑂 ∪ ran 𝐻)) ⊆ (𝐾𝐶𝐵) ∧ ∀𝑥∀𝑦(𝑥𝑀𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑃) ∈ 𝑐)) → (𝑆‘𝑃) ∈ 𝑐)) | 
| 121 | 27, 55, 120 | 3syld 60 | . . . 4
⊢ (𝜑 → (((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → (𝑆‘𝑃) ∈ 𝑐)) | 
| 122 | 121 | alrimiv 1927 | . . 3
⊢ (𝜑 → ∀𝑐(((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → (𝑆‘𝑃) ∈ 𝑐)) | 
| 123 |  | fvex 6919 | . . . 4
⊢ (𝑆‘𝑃) ∈ V | 
| 124 | 123 | elintab 4958 | . . 3
⊢ ((𝑆‘𝑃) ∈ ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))} ↔ ∀𝑐(((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐))) → (𝑆‘𝑃) ∈ 𝑐)) | 
| 125 | 122, 124 | sylibr 234 | . 2
⊢ (𝜑 → (𝑆‘𝑃) ∈ ∩ {𝑐 ∣ ((𝐵 ∪ ran 𝐻) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(〈𝑚, 𝑜, 𝑝〉 ∈ 𝐴 → ∀𝑠 ∈ ran 𝐿(((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → ((𝑊‘(𝑠‘(𝐻‘𝑥))) × (𝑊‘(𝑠‘(𝐻‘𝑦)))) ⊆ 𝐾)) → (𝑠‘𝑝) ∈ 𝑐)))}) | 
| 126 | 125, 14 | eleqtrrd 2844 | 1
⊢ (𝜑 → (𝑆‘𝑃) ∈ (𝐾𝐶𝐵)) |