Metamath Proof Explorer

Theorem mclsppslem

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 ⊢ ( ( 𝜑 ∧ ( 𝑥 𝑀 𝑦 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ) → 𝑎 𝐾 𝑏 )
mclsppslem.9 ⊢ ( 𝜑 → ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) )
mclsppslem.10 ⊢ ( 𝜑 → 𝑠 ∈ ran 𝐿 )
mclsppslem.11 ⊢ ( 𝜑 → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
mclsppslem.12 ⊢ ( 𝜑 → ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) )
Assertion mclsppslem ( 𝜑 → ( 𝑠 ‘ 𝑝 ) ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )

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 mclsppslem.9 ⊢ ( 𝜑 → ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) )
18 mclsppslem.10 ⊢ ( 𝜑 → 𝑠 ∈ ran 𝐿 )
19 mclsppslem.11 ⊢ ( 𝜑 → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
20 mclsppslem.12 ⊢ ( 𝜑 → ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) )
21 8 2 msubf ⊢ ( 𝑠 ∈ ran 𝐿 → 𝑠 : 𝐸 ⟶ 𝐸 )
22 18 21 syl ⊢ ( 𝜑 → 𝑠 : 𝐸 ⟶ 𝐸 )
23 eqid ⊢ ( mAx ‘ 𝑇 ) = ( mAx ‘ 𝑇 )
24 eqid ⊢ ( mStat ‘ 𝑇 ) = ( mStat ‘ 𝑇 )
25 23 24 maxsta ⊢ ( 𝑇 ∈ mFS → ( mAx ‘ 𝑇 ) ⊆ ( mStat ‘ 𝑇 ) )
26 4 25 syl ⊢ ( 𝜑 → ( mAx ‘ 𝑇 ) ⊆ ( mStat ‘ 𝑇 ) )
27 eqid ⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 )
28 27 24 mstapst ⊢ ( mStat ‘ 𝑇 ) ⊆ ( mPreSt ‘ 𝑇 )
29 26 28 sstrdi ⊢ ( 𝜑 → ( mAx ‘ 𝑇 ) ⊆ ( mPreSt ‘ 𝑇 ) )
30 29 17 sseldd ⊢ ( 𝜑 → ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
31 1 2 27 elmpst ⊢ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( 𝑚 ⊆ 𝐷 ∧ ◡ 𝑚 = 𝑚 ) ∧ ( 𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin ) ∧ 𝑝 ∈ 𝐸 ) )
32 30 31 sylib ⊢ ( 𝜑 → ( ( 𝑚 ⊆ 𝐷 ∧ ◡ 𝑚 = 𝑚 ) ∧ ( 𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin ) ∧ 𝑝 ∈ 𝐸 ) )
33 32 simp3d ⊢ ( 𝜑 → 𝑝 ∈ 𝐸 )
34 22 33 ffvelrnd ⊢ ( 𝜑 → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 )
35 fvco3 ⊢ ( ( 𝑠 : 𝐸 ⟶ 𝐸 ∧ 𝑝 ∈ 𝐸 ) → ( ( 𝑆 ∘ 𝑠 ) ‘ 𝑝 ) = ( 𝑆 ‘ ( 𝑠 ‘ 𝑝 ) ) )
36 22 33 35 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 ∘ 𝑠 ) ‘ 𝑝 ) = ( 𝑆 ‘ ( 𝑠 ‘ 𝑝 ) ) )
37 8 msubco ⊢ ( ( 𝑆 ∈ ran 𝐿 ∧ 𝑠 ∈ ran 𝐿 ) → ( 𝑆 ∘ 𝑠 ) ∈ ran 𝐿 )
38 13 18 37 syl2anc ⊢ ( 𝜑 → ( 𝑆 ∘ 𝑠 ) ∈ ran 𝐿 )
39 8 2 msubf ⊢ ( 𝑆 ∈ ran 𝐿 → 𝑆 : 𝐸 ⟶ 𝐸 )
40 13 39 syl ⊢ ( 𝜑 → 𝑆 : 𝐸 ⟶ 𝐸 )
41 fco ⊢ ( ( 𝑆 : 𝐸 ⟶ 𝐸 ∧ 𝑠 : 𝐸 ⟶ 𝐸 ) → ( 𝑆 ∘ 𝑠 ) : 𝐸 ⟶ 𝐸 )
42 40 22 41 syl2anc ⊢ ( 𝜑 → ( 𝑆 ∘ 𝑠 ) : 𝐸 ⟶ 𝐸 )
43 42 ffnd ⊢ ( 𝜑 → ( 𝑆 ∘ 𝑠 ) Fn 𝐸 )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑜 ) → ( 𝑆 ∘ 𝑠 ) Fn 𝐸 )
45 22 ffund ⊢ ( 𝜑 → Fun 𝑠 )
46 31 simp2bi ⊢ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin ) )
47 30 46 syl ⊢ ( 𝜑 → ( 𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin ) )
48 47 simpld ⊢ ( 𝜑 → 𝑜 ⊆ 𝐸 )
49 9 2 10 mvhf ⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 ⟶ 𝐸 )
50 frn ⊢ ( 𝐻 : 𝑉 ⟶ 𝐸 → ran 𝐻 ⊆ 𝐸 )
51 4 49 50 3syl ⊢ ( 𝜑 → ran 𝐻 ⊆ 𝐸 )
52 48 51 unssd ⊢ ( 𝜑 → ( 𝑜 ∪ ran 𝐻 ) ⊆ 𝐸 )
53 22 fdmd ⊢ ( 𝜑 → dom 𝑠 = 𝐸 )
54 52 53 sseqtrrd ⊢ ( 𝜑 → ( 𝑜 ∪ ran 𝐻 ) ⊆ dom 𝑠 )
55 funimass3 ⊢ ( ( Fun 𝑠 ∧ ( 𝑜 ∪ ran 𝐻 ) ⊆ dom 𝑠 ) → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( 𝑜 ∪ ran 𝐻 ) ⊆ ( ◡ 𝑠 “ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ) )
56 45 54 55 syl2anc ⊢ ( 𝜑 → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( 𝑜 ∪ ran 𝐻 ) ⊆ ( ◡ 𝑠 “ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) ) )
57 19 56 mpbid ⊢ ( 𝜑 → ( 𝑜 ∪ ran 𝐻 ) ⊆ ( ◡ 𝑠 “ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ) )
58 cnvco ⊢ ◡ ( 𝑆 ∘ 𝑠 ) = ( ◡ 𝑠 ∘ ◡ 𝑆 )
59 58 imaeq1i ⊢ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) = ( ( ◡ 𝑠 ∘ ◡ 𝑆 ) “ ( 𝐾 𝐶 𝐵 ) )
60 imaco ⊢ ( ( ◡ 𝑠 ∘ ◡ 𝑆 ) “ ( 𝐾 𝐶 𝐵 ) ) = ( ◡ 𝑠 “ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
61 59 60 eqtri ⊢ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) = ( ◡ 𝑠 “ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )
62 57 61 sseqtrrdi ⊢ ( 𝜑 → ( 𝑜 ∪ ran 𝐻 ) ⊆ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) )
63 62 unssad ⊢ ( 𝜑 → 𝑜 ⊆ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) )
64 63 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑜 ) → 𝑐 ∈ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) )
65 elpreima ⊢ ( ( 𝑆 ∘ 𝑠 ) Fn 𝐸 → ( 𝑐 ∈ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( 𝑐 ∈ 𝐸 ∧ ( ( 𝑆 ∘ 𝑠 ) ‘ 𝑐 ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) )
66 65 simplbda ⊢ ( ( ( 𝑆 ∘ 𝑠 ) Fn 𝐸 ∧ 𝑐 ∈ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) ) → ( ( 𝑆 ∘ 𝑠 ) ‘ 𝑐 ) ∈ ( 𝐾 𝐶 𝐵 ) )
67 44 64 66 syl2anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑜 ) → ( ( 𝑆 ∘ 𝑠 ) ‘ 𝑐 ) ∈ ( 𝐾 𝐶 𝐵 ) )
68 43 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑆 ∘ 𝑠 ) Fn 𝐸 )
69 62 unssbd ⊢ ( 𝜑 → ran 𝐻 ⊆ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ran 𝐻 ⊆ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) )
71 ffn ⊢ ( 𝐻 : 𝑉 ⟶ 𝐸 → 𝐻 Fn 𝑉 )
72 4 49 71 3syl ⊢ ( 𝜑 → 𝐻 Fn 𝑉 )
73 fnfvelrn ⊢ ( ( 𝐻 Fn 𝑉 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑡 ) ∈ ran 𝐻 )
74 72 73 sylan ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑡 ) ∈ ran 𝐻 )
75 70 74 sseldd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑡 ) ∈ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) )
76 elpreima ⊢ ( ( 𝑆 ∘ 𝑠 ) Fn 𝐸 → ( ( 𝐻 ‘ 𝑡 ) ∈ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( ( 𝐻 ‘ 𝑡 ) ∈ 𝐸 ∧ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑡 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) )
77 76 simplbda ⊢ ( ( ( 𝑆 ∘ 𝑠 ) Fn 𝐸 ∧ ( 𝐻 ‘ 𝑡 ) ∈ ( ◡ ( 𝑆 ∘ 𝑠 ) “ ( 𝐾 𝐶 𝐵 ) ) ) → ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑡 ) ) ∈ ( 𝐾 𝐶 𝐵 ) )
78 68 75 77 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑡 ) ) ∈ ( 𝐾 𝐶 𝐵 ) )
79 22 adantr ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → 𝑠 : 𝐸 ⟶ 𝐸 )
80 4 49 syl ⊢ ( 𝜑 → 𝐻 : 𝑉 ⟶ 𝐸 )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → 𝐻 : 𝑉 ⟶ 𝐸 )
82 32 simp1d ⊢ ( 𝜑 → ( 𝑚 ⊆ 𝐷 ∧ ◡ 𝑚 = 𝑚 ) )
83 82 simpld ⊢ ( 𝜑 → 𝑚 ⊆ 𝐷 )
84 9 1 mdvval ⊢ 𝐷 = ( ( 𝑉 × 𝑉 ) ∖ I )
85 difss ⊢ ( ( 𝑉 × 𝑉 ) ∖ I ) ⊆ ( 𝑉 × 𝑉 )
86 84 85 eqsstri ⊢ 𝐷 ⊆ ( 𝑉 × 𝑉 )
87 83 86 sstrdi ⊢ ( 𝜑 → 𝑚 ⊆ ( 𝑉 × 𝑉 ) )
88 87 ssbrd ⊢ ( 𝜑 → ( 𝑐 𝑚 𝑑 → 𝑐 ( 𝑉 × 𝑉 ) 𝑑 ) )
89 88 imp ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → 𝑐 ( 𝑉 × 𝑉 ) 𝑑 )
90 brxp ⊢ ( 𝑐 ( 𝑉 × 𝑉 ) 𝑑 ↔ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) )
91 89 90 sylib ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) )
92 91 simpld ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → 𝑐 ∈ 𝑉 )
93 81 92 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝐻 ‘ 𝑐 ) ∈ 𝐸 )
94 fvco3 ⊢ ( ( 𝑠 : 𝐸 ⟶ 𝐸 ∧ ( 𝐻 ‘ 𝑐 ) ∈ 𝐸 ) → ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) = ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) )
95 79 93 94 syl2anc ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) = ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) )
96 95 fveq2d ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) ) = ( 𝑊 ‘ ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ) )
97 4 adantr ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → 𝑇 ∈ mFS )
98 13 adantr ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → 𝑆 ∈ ran 𝐿 )
99 79 93 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ∈ 𝐸 )
100 8 2 11 10 msubvrs ⊢ ( ( 𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ∈ 𝐸 ) → ( 𝑊 ‘ ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ) = ∪ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) )
101 97 98 99 100 syl3anc ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑊 ‘ ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ) = ∪ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) )
102 96 101 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) ) = ∪ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) )
103 102 eleq2d ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑎 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) ) ↔ 𝑎 ∈ ∪ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ) )
104 eliun ⊢ ( 𝑎 ∈ ∪ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) )
105 103 104 bitrdi ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑎 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ) )
106 91 simprd ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → 𝑑 ∈ 𝑉 )
107 81 106 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝐻 ‘ 𝑑 ) ∈ 𝐸 )
108 fvco3 ⊢ ( ( 𝑠 : 𝐸 ⟶ 𝐸 ∧ ( 𝐻 ‘ 𝑑 ) ∈ 𝐸 ) → ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) = ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) )
109 79 107 108 syl2anc ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) = ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) )
110 109 fveq2d ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) ) = ( 𝑊 ‘ ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) )
111 79 107 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ∈ 𝐸 )
112 8 2 11 10 msubvrs ⊢ ( ( 𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ∈ 𝐸 ) → ( 𝑊 ‘ ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) = ∪ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) )
113 97 98 111 112 syl3anc ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑊 ‘ ( 𝑆 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) = ∪ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) )
114 110 113 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) ) = ∪ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) )
115 114 eleq2d ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑏 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) ) ↔ 𝑏 ∈ ∪ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) )
116 eliun ⊢ ( 𝑏 ∈ ∪ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ↔ ∃ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) )
117 115 116 bitrdi ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑏 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) ) ↔ ∃ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) )
118 105 117 anbi12d ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( ( 𝑎 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ ∃ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) ) )
119 reeanv ⊢ ( ∃ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∃ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ( 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) ↔ ( ∃ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ ∃ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) )
120 simpll ⊢ ( ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) ∧ ( 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∧ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ) → 𝜑 )
121 brxp ⊢ ( 𝑢 ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) 𝑣 ↔ ( 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∧ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) )
122 breq12 ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( 𝑧 𝑚 𝑤 ↔ 𝑐 𝑚 𝑑 ) )
123 simpl ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → 𝑧 = 𝑐 )
124 123 fveq2d ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ 𝑐 ) )
125 124 fveq2d ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) = ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) )
126 125 fveq2d ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) = ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) )
127 simpr ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → 𝑤 = 𝑑 )
128 127 fveq2d ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( 𝐻 ‘ 𝑤 ) = ( 𝐻 ‘ 𝑑 ) )
129 128 fveq2d ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) = ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) )
130 129 fveq2d ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) = ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) )
131 126 130 xpeq12d ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) = ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) )
132 131 sseq1d ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ↔ ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ⊆ 𝑀 ) )
133 122 132 imbi12d ⊢ ( ( 𝑧 = 𝑐 ∧ 𝑤 = 𝑑 ) → ( ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) ↔ ( 𝑐 𝑚 𝑑 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ⊆ 𝑀 ) ) )
134 133 spc2gv ⊢ ( ( 𝑐 ∈ V ∧ 𝑑 ∈ V ) → ( ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) → ( 𝑐 𝑚 𝑑 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ⊆ 𝑀 ) ) )
135 134 el2v ⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝑧 𝑚 𝑤 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑧 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑤 ) ) ) ) ⊆ 𝑀 ) → ( 𝑐 𝑚 𝑑 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ⊆ 𝑀 ) )
136 20 135 syl ⊢ ( 𝜑 → ( 𝑐 𝑚 𝑑 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ⊆ 𝑀 ) )
137 136 imp ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ⊆ 𝑀 )
138 137 ssbrd ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( 𝑢 ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) 𝑣 → 𝑢 𝑀 𝑣 ) )
139 121 138 syl5bir ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( ( 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∧ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) → 𝑢 𝑀 𝑣 ) )
140 139 imp ⊢ ( ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) ∧ ( 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∧ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ) → 𝑢 𝑀 𝑣 )
141 vex ⊢ 𝑢 ∈ V
142 vex ⊢ 𝑣 ∈ V
143 breq12 ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑥 𝑀 𝑦 ↔ 𝑢 𝑀 𝑣 ) )
144 simpl ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑥 = 𝑢 )
145 144 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑢 ) )
146 145 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) = ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) )
147 146 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) = ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) )
148 147 eleq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ↔ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ) )
149 simpr ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
150 149 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑣 ) )
151 150 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) )
152 151 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) = ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) )
153 152 eleq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ↔ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) )
154 143 148 153 3anbi123d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( 𝑥 𝑀 𝑦 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ↔ ( 𝑢 𝑀 𝑣 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) ) )
155 154 anbi2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( 𝜑 ∧ ( 𝑥 𝑀 𝑦 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝜑 ∧ ( 𝑢 𝑀 𝑣 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) ) ) )
156 155 imbi1d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( ( 𝜑 ∧ ( 𝑥 𝑀 𝑦 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑥 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ) → 𝑎 𝐾 𝑏 ) ↔ ( ( 𝜑 ∧ ( 𝑢 𝑀 𝑣 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) ) → 𝑎 𝐾 𝑏 ) ) )
157 141 142 156 16 vtocl2 ⊢ ( ( 𝜑 ∧ ( 𝑢 𝑀 𝑣 ∧ 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) ) → 𝑎 𝐾 𝑏 )
158 157 3exp2 ⊢ ( 𝜑 → ( 𝑢 𝑀 𝑣 → ( 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) → ( 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) → 𝑎 𝐾 𝑏 ) ) ) )
159 158 imp4b ⊢ ( ( 𝜑 ∧ 𝑢 𝑀 𝑣 ) → ( ( 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) → 𝑎 𝐾 𝑏 ) )
160 120 140 159 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) ∧ ( 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∧ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ) → ( ( 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) → 𝑎 𝐾 𝑏 ) )
161 160 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( ∃ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∃ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) ( 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) → 𝑎 𝐾 𝑏 ) )
162 119 161 syl5bir ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( ( ∃ 𝑢 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑐 ) ) ) 𝑎 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑢 ) ) ) ∧ ∃ 𝑣 ∈ ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑑 ) ) ) 𝑏 ∈ ( 𝑊 ‘ ( 𝑆 ‘ ( 𝐻 ‘ 𝑣 ) ) ) ) → 𝑎 𝐾 𝑏 ) )
163 118 162 sylbid ⊢ ( ( 𝜑 ∧ 𝑐 𝑚 𝑑 ) → ( ( 𝑎 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) → 𝑎 𝐾 𝑏 ) )
164 163 exp4b ⊢ ( 𝜑 → ( 𝑐 𝑚 𝑑 → ( 𝑎 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) ) → ( 𝑏 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) ) → 𝑎 𝐾 𝑏 ) ) ) )
165 164 3imp2 ⊢ ( ( 𝜑 ∧ ( 𝑐 𝑚 𝑑 ∧ 𝑎 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑐 ) ) ) ∧ 𝑏 ∈ ( 𝑊 ‘ ( ( 𝑆 ∘ 𝑠 ) ‘ ( 𝐻 ‘ 𝑑 ) ) ) ) ) → 𝑎 𝐾 𝑏 )
166 1 2 3 4 5 6 23 8 9 10 11 17 38 67 78 165 mclsax ⊢ ( 𝜑 → ( ( 𝑆 ∘ 𝑠 ) ‘ 𝑝 ) ∈ ( 𝐾 𝐶 𝐵 ) )
167 36 166 eqeltrrd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑠 ‘ 𝑝 ) ) ∈ ( 𝐾 𝐶 𝐵 ) )
168 40 ffnd ⊢ ( 𝜑 → 𝑆 Fn 𝐸 )
169 elpreima ⊢ ( 𝑆 Fn 𝐸 → ( ( 𝑠 ‘ 𝑝 ) ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ∧ ( 𝑆 ‘ ( 𝑠 ‘ 𝑝 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) )
170 168 169 syl ⊢ ( 𝜑 → ( ( 𝑠 ‘ 𝑝 ) ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) ↔ ( ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 ∧ ( 𝑆 ‘ ( 𝑠 ‘ 𝑝 ) ) ∈ ( 𝐾 𝐶 𝐵 ) ) ) )
171 34 167 170 mpbir2and ⊢ ( 𝜑 → ( 𝑠 ‘ 𝑝 ) ∈ ( ◡ 𝑆 “ ( 𝐾 𝐶 𝐵 ) ) )