Metamath Proof Explorer

Theorem mclspps

Description: The closure is closed under application of provable pre-statements. (Compare mclsax .) This theorem is what justifies the treatment of theorems as "equivalent" to axioms once they have been proven: the composition of one theorem in the proof of another yields a theorem. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclspps.d ⊢ 𝐷 = ( mDV ‘ 𝑇 )
mclspps.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
mclspps.c ⊢ 𝐶 = ( mCls ‘ 𝑇 )
mclspps.1 ⊢ ( 𝜑 → 𝑇 ∈ mFS )
mclspps.2 ⊢ ( 𝜑 → 𝐾 ⊆ 𝐷 )
mclspps.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
mclspps.j ⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
mclspps.l ⊢ 𝐿 = ( mSubst ‘ 𝑇 )
mclspps.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
mclspps.h ⊢ 𝐻 = ( mVH ‘ 𝑇 )
mclspps.w ⊢ 𝑊 = ( mVars ‘ 𝑇 )
mclspps.4 ⊢ ( 𝜑 → ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ 𝐽 )
mclspps.5 ⊢ ( 𝜑 → 𝑆 ∈ ran 𝐿 )
mclspps.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) )
mclspps.7 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) )
mclspps.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 𝑀 𝑦 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ) → 𝑎 𝐾 𝑏 )
Assertion mclspps ( 𝜑 → ( 𝑆 ‘ 𝑃 ) ∈ ( 𝐾 𝐶 𝐵 ) )

Proof

Step Hyp Ref Expression
1 mclspps.d ⊢ 𝐷 = ( mDV ‘ 𝑇 )
2 mclspps.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
3 mclspps.c ⊢ 𝐶 = ( mCls ‘ 𝑇 )
4 mclspps.1 ⊢ ( 𝜑 → 𝑇 ∈ mFS )
5 mclspps.2 ⊢ ( 𝜑 → 𝐾 ⊆ 𝐷 )
6 mclspps.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
7 mclspps.j ⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
8 mclspps.l ⊢ 𝐿 = ( mSubst ‘ 𝑇 )
9 mclspps.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
10 mclspps.h ⊢ 𝐻 = ( mVH ‘ 𝑇 )
11 mclspps.w ⊢ 𝑊 = ( mVars ‘ 𝑇 )
12 mclspps.4 ⊢ ( 𝜑 → ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ 𝐽 )
13 mclspps.5 ⊢ ( 𝜑 → 𝑆 ∈ ran 𝐿 )
14 mclspps.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) )
15 mclspps.7 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) )
16 mclspps.8 ⊢ ( ( 𝜑 ∧ ( 𝑥 𝑀 𝑦 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ) → 𝑎 𝐾 𝑏 )
17 8 2 msubf ⊢ ( 𝑆 ∈ ran 𝐿 → 𝑆 : 𝐸 ⟶ 𝐸 )
18 13 17 syl ⊢ ( 𝜑 → 𝑆 : 𝐸 ⟶ 𝐸 )
19 18 ffnd ⊢ ( 𝜑 → 𝑆 Fn 𝐸 )
20 eqid ⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 )
21 20 7 mppspst ⊢ 𝐽 ⊆ ( mPreSt ‘ 𝑇 )
22 21 12 sseldi ⊢ ( 𝜑 → ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
23 1 2 20 elmpst ⊢ ( ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( 𝑀 ⊆ 𝐷 ∧ ◡ 𝑀 = 𝑀 ) ∧ ( 𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin ) ∧ 𝑃 ∈ 𝐸 ) )
24 22 23 sylib ⊢ ( 𝜑 → ( ( 𝑀 ⊆ 𝐷 ∧ ◡ 𝑀 = 𝑀 ) ∧ ( 𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin ) ∧ 𝑃 ∈ 𝐸 ) )
25 24 simp1d ⊢ ( 𝜑 → ( 𝑀 ⊆ 𝐷 ∧ ◡ 𝑀 = 𝑀 ) )
26 25 simpld ⊢ ( 𝜑 → 𝑀 ⊆ 𝐷 )
27 24 simp2d ⊢ ( 𝜑 → ( 𝑂 ⊆ 𝐸 ∧ 𝑂 ∈ Fin ) )
28 27 simpld ⊢ ( 𝜑 → 𝑂 ⊆ 𝐸 )
29 eqid ⊢ ( mAx ‘ 𝑇 ) = ( mAx ‘ 𝑇 )
30 14 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑂 ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) )
31 18 ffund ⊢ ( 𝜑 → Fun 𝑆 )
32 18 fdmd ⊢ ( 𝜑 → dom 𝑆 = 𝐸 )
33 28 32 sseqtrrd ⊢ ( 𝜑 → 𝑂 ⊆ dom 𝑆 )
34 funimass5 ⊢ ( ( Fun 𝑆 ∧ 𝑂 ⊆ dom 𝑆 ) → ( 𝑂 ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ∀ 𝑥 ∈ 𝑂 ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) )
35 31 33 34 syl2anc ⊢ ( 𝜑 → ( 𝑂 ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ∀ 𝑥 ∈ 𝑂 ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) ) )
36 30 35 mpbird ⊢ ( 𝜑 → 𝑂 ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
37 9 2 10 mvhf ⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 ⟶ 𝐸 )
38 4 37 syl ⊢ ( 𝜑 → 𝐻 : 𝑉 ⟶ 𝐸 )
39 38 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑣 ) ∈ 𝐸 )
40 elpreima ⊢ ( 𝑆 Fn 𝐸 → ( ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( ( 𝐻 ‘ 𝑣 ) ∈ 𝐸 ∧ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) )
41 19 40 syl ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( ( 𝐻 ‘ 𝑣 ) ∈ 𝐸 ∧ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( ( 𝐻 ‘ 𝑣 ) ∈ 𝐸 ∧ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) )
43 39 15 42 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑣 ) ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
44 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → 𝑇 ∈ mFS )
45 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → 𝐾 ⊆ 𝐷 )
46 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → 𝐵 ⊆ 𝐸 )
47 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ 𝐽 )
48 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → 𝑆 ∈ ran 𝐿 )
49 14 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) ∧ 𝑥 ∈ 𝑂 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( 𝐾 𝐶 𝐵 ) )
50 15 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐾 𝐶 𝐵 ) )
51 16 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) ∧ ( 𝑥 𝑀 𝑦 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ) → 𝑎 𝐾 𝑏 )
52 simp21 ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) )
53 simp22 ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → 𝑠 ∈ ran 𝐿 )
54 simp23 ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
55 simp3 ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) )
56 1 2 3 44 45 46 7 8 9 10 11 47 48 49 50 51 52 53 54 55 mclsppslem ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ∧ ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
57 1 2 3 4 26 28 29 8 9 10 11 36 43 56 mclsind ⊢ ( 𝜑 → ( 𝑀 𝐶 𝑂 ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
58 20 7 3 elmpps ⊢ ( ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ 𝐽 ↔ ( ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ∧ 𝑃 ∈ ( 𝑀 𝐶 𝑂 ) ) )
59 58 simprbi ⊢ ( ⟨ 𝑀 , 𝑂 , 𝑃 ⟩ ∈ 𝐽 → 𝑃 ∈ ( 𝑀 𝐶 𝑂 ) )
60 12 59 syl ⊢ ( 𝜑 → 𝑃 ∈ ( 𝑀 𝐶 𝑂 ) )
61 57 60 sseldd ⊢ ( 𝜑 → 𝑃 ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
62 elpreima ⊢ ( 𝑆 Fn 𝐸 → ( 𝑃 ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( 𝑃 ∈ 𝐸 ∧ ( 𝑆 ‘ 𝑃 ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) )
63 62 simplbda ⊢ ( ( 𝑆 Fn 𝐸 ∧ 𝑃 ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) → ( 𝑆 ‘ 𝑃 ) ∈ ( 𝐾 𝐶 𝐵 ) )
64 19 61 63 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑃 ) ∈ ( 𝐾 𝐶 𝐵 ) )