Theorem mclsppslem 32837

Description: The closure is closed under application of provable pre-statements. (Compare mclsax 32823.) 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.)

Hypotheses

Ref	Expression
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

Ref	Expression
mclsppslem	⊢ (𝜑 → (𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)))

Distinct variable groups:   𝑚,𝑜,𝑝,𝑠,𝑣,𝐸   𝑎,𝑏,𝑚,𝑜,𝑝,𝑠,𝑣,𝑤,𝑥,𝑦,𝑧,𝐻   𝑣,𝑉,𝑧   𝐾,𝑎,𝑏,𝑚,𝑜,𝑝,𝑠,𝑣,𝑥,𝑦   𝑇,𝑎,𝑏,𝑚,𝑜,𝑝,𝑠,𝑣,𝑤,𝑥,𝑦,𝑧   𝐿,𝑎,𝑏,𝑚,𝑜,𝑝,𝑠,𝑣,𝑤,𝑥,𝑦,𝑧   𝑆,𝑎,𝑏,𝑚,𝑜,𝑝,𝑠,𝑣,𝑥,𝑦   𝐵,𝑎,𝑏,𝑚,𝑜,𝑝,𝑠,𝑣,𝑥,𝑦   𝑊,𝑎,𝑏,𝑚,𝑜,𝑝,𝑠,𝑣,𝑤,𝑥,𝑦,𝑧   𝐶,𝑎,𝑏,𝑚,𝑜,𝑝,𝑠,𝑣,𝑥,𝑦,𝑧   𝑀,𝑎,𝑏,𝑚,𝑜,𝑝,𝑠,𝑣,𝑤,𝑥,𝑦,𝑧   𝑚,𝑂,𝑜,𝑝,𝑠,𝑣,𝑤,𝑥,𝑧   𝜑,𝑎,𝑏,𝑣,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑧,𝑤,𝑚,𝑜,𝑠,𝑝)   𝐵(𝑧,𝑤)   𝐶(𝑤)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑚,𝑜,𝑠,𝑝,𝑎,𝑏)   𝑃(𝑥,𝑦,𝑧,𝑤,𝑣,𝑚,𝑜,𝑠,𝑝,𝑎,𝑏)   𝑆(𝑧,𝑤)   𝐸(𝑥,𝑦,𝑧,𝑤,𝑎,𝑏)   𝐽(𝑥,𝑦,𝑧,𝑤,𝑣,𝑚,𝑜,𝑠,𝑝,𝑎,𝑏)   𝐾(𝑧,𝑤)   𝑂(𝑦,𝑎,𝑏)   𝑉(𝑥,𝑦,𝑤,𝑚,𝑜,𝑠,𝑝,𝑎,𝑏)

Proof of Theorem mclsppslem

Dummy variables 𝑡 𝑢 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mclsppslem.10	. . . 4 ⊢ (𝜑 → 𝑠 ∈ ran 𝐿)
2		mclspps.l	. . . . 5 ⊢ 𝐿 = (mSubst‘𝑇)
3		mclspps.e	. . . . 5 ⊢ 𝐸 = (mEx‘𝑇)
4	2, 3	msubf 32786	. . . 4 ⊢ (𝑠 ∈ ran 𝐿 → 𝑠:𝐸⟶𝐸)
5	1, 4	syl 17	. . 3 ⊢ (𝜑 → 𝑠:𝐸⟶𝐸)
6		mclspps.1	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ mFS)
7		eqid 2821	. . . . . . . . 9 ⊢ (mAx‘𝑇) = (mAx‘𝑇)
8		eqid 2821	. . . . . . . . 9 ⊢ (mStat‘𝑇) = (mStat‘𝑇)
9	7, 8	maxsta 32808	. . . . . . . 8 ⊢ (𝑇 ∈ mFS → (mAx‘𝑇) ⊆ (mStat‘𝑇))
10	6, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → (mAx‘𝑇) ⊆ (mStat‘𝑇))
11		eqid 2821	. . . . . . . 8 ⊢ (mPreSt‘𝑇) = (mPreSt‘𝑇)
12	11, 8	mstapst 32801	. . . . . . 7 ⊢ (mStat‘𝑇) ⊆ (mPreSt‘𝑇)
13	10, 12	sstrdi 3967	. . . . . 6 ⊢ (𝜑 → (mAx‘𝑇) ⊆ (mPreSt‘𝑇))
14		mclsppslem.9	. . . . . 6 ⊢ (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑇))
15	13, 14	sseldd 3956	. . . . 5 ⊢ (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇))
16		mclspps.d	. . . . . 6 ⊢ 𝐷 = (mDV‘𝑇)
17	16, 3, 11	elmpst 32790	. . . . 5 ⊢ (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚) ∧ (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin) ∧ 𝑝 ∈ 𝐸))
18	15, 17	sylib 220	. . . 4 ⊢ (𝜑 → ((𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚) ∧ (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin) ∧ 𝑝 ∈ 𝐸))
19	18	simp3d 1140	. . 3 ⊢ (𝜑 → 𝑝 ∈ 𝐸)
20	5, 19	ffvelrnd 6838	. 2 ⊢ (𝜑 → (𝑠‘𝑝) ∈ 𝐸)
21		fvco3 6746	. . . 4 ⊢ ((𝑠:𝐸⟶𝐸 ∧ 𝑝 ∈ 𝐸) → ((𝑆 ∘ 𝑠)‘𝑝) = (𝑆‘(𝑠‘𝑝)))
22	5, 19, 21	syl2anc 586	. . 3 ⊢ (𝜑 → ((𝑆 ∘ 𝑠)‘𝑝) = (𝑆‘(𝑠‘𝑝)))
23		mclspps.c	. . . 4 ⊢ 𝐶 = (mCls‘𝑇)
24		mclspps.2	. . . 4 ⊢ (𝜑 → 𝐾 ⊆ 𝐷)
25		mclspps.3	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ 𝐸)
26		mclspps.v	. . . 4 ⊢ 𝑉 = (mVR‘𝑇)
27		mclspps.h	. . . 4 ⊢ 𝐻 = (mVH‘𝑇)
28		mclspps.w	. . . 4 ⊢ 𝑊 = (mVars‘𝑇)
29		mclspps.5	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ ran 𝐿)
30	2	msubco 32785	. . . . 5 ⊢ ((𝑆 ∈ ran 𝐿 ∧ 𝑠 ∈ ran 𝐿) → (𝑆 ∘ 𝑠) ∈ ran 𝐿)
31	29, 1, 30	syl2anc 586	. . . 4 ⊢ (𝜑 → (𝑆 ∘ 𝑠) ∈ ran 𝐿)
32	2, 3	msubf 32786	. . . . . . . . 9 ⊢ (𝑆 ∈ ran 𝐿 → 𝑆:𝐸⟶𝐸)
33	29, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:𝐸⟶𝐸)
34		fco 6517	. . . . . . . 8 ⊢ ((𝑆:𝐸⟶𝐸 ∧ 𝑠:𝐸⟶𝐸) → (𝑆 ∘ 𝑠):𝐸⟶𝐸)
35	33, 5, 34	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → (𝑆 ∘ 𝑠):𝐸⟶𝐸)
36	35	ffnd 6501	. . . . . 6 ⊢ (𝜑 → (𝑆 ∘ 𝑠) Fn 𝐸)
37	36	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑜) → (𝑆 ∘ 𝑠) Fn 𝐸)
38		mclsppslem.11	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵)))
39	5	ffund 6504	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝑠)
40	17	simp2bi 1142	. . . . . . . . . . . . . 14 ⊢ (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) → (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin))
41	15, 40	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin))
42	41	simpld 497	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑜 ⊆ 𝐸)
43	26, 3, 27	mvhf 32812	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸)
44		frn 6506	. . . . . . . . . . . . 13 ⊢ (𝐻:𝑉⟶𝐸 → ran 𝐻 ⊆ 𝐸)
45	6, 43, 44	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐻 ⊆ 𝐸)
46	42, 45	unssd 4150	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ 𝐸)
47	5	fdmd 6509	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑠 = 𝐸)
48	46, 47	sseqtrrd 3996	. . . . . . . . . 10 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠)
49		funimass3 6810	. . . . . . . . . 10 ⊢ ((Fun 𝑠 ∧ (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))))
50	39, 48, 49	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))))
51	38, 50	mpbid 234	. . . . . . . 8 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵))))
52		cnvco 5742	. . . . . . . . . 10 ⊢ ◡(𝑆 ∘ 𝑠) = (◡𝑠 ∘ ◡𝑆)
53	52	imaeq1i 5912	. . . . . . . . 9 ⊢ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) = ((◡𝑠 ∘ ◡𝑆) “ (𝐾𝐶𝐵))
54		imaco 6090	. . . . . . . . 9 ⊢ ((◡𝑠 ∘ ◡𝑆) “ (𝐾𝐶𝐵)) = (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))
55	53, 54	eqtri 2844	. . . . . . . 8 ⊢ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) = (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))
56	51, 55	sseqtrrdi 4006	. . . . . . 7 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
57	56	unssad 4151	. . . . . 6 ⊢ (𝜑 → 𝑜 ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
58	57	sselda 3955	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑜) → 𝑐 ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
59		elpreima 6814	. . . . . 6 ⊢ ((𝑆 ∘ 𝑠) Fn 𝐸 → (𝑐 ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) ↔ (𝑐 ∈ 𝐸 ∧ ((𝑆 ∘ 𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))))
60	59	simplbda 502	. . . . 5 ⊢ (((𝑆 ∘ 𝑠) Fn 𝐸 ∧ 𝑐 ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵))) → ((𝑆 ∘ 𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
61	37, 58, 60	syl2anc 586	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑜) → ((𝑆 ∘ 𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
62	36	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑆 ∘ 𝑠) Fn 𝐸)
63	56	unssbd 4152	. . . . . . 7 ⊢ (𝜑 → ran 𝐻 ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
64	63	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ran 𝐻 ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
65		ffn 6500	. . . . . . . 8 ⊢ (𝐻:𝑉⟶𝐸 → 𝐻 Fn 𝑉)
66	6, 43, 65	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn 𝑉)
67		fnfvelrn 6834	. . . . . . 7 ⊢ ((𝐻 Fn 𝑉 ∧ 𝑡 ∈ 𝑉) → (𝐻‘𝑡) ∈ ran 𝐻)
68	66, 67	sylan 582	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐻‘𝑡) ∈ ran 𝐻)
69	64, 68	sseldd 3956	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐻‘𝑡) ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
70		elpreima 6814	. . . . . 6 ⊢ ((𝑆 ∘ 𝑠) Fn 𝐸 → ((𝐻‘𝑡) ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) ↔ ((𝐻‘𝑡) ∈ 𝐸 ∧ ((𝑆 ∘ 𝑠)‘(𝐻‘𝑡)) ∈ (𝐾𝐶𝐵))))
71	70	simplbda 502	. . . . 5 ⊢ (((𝑆 ∘ 𝑠) Fn 𝐸 ∧ (𝐻‘𝑡) ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵))) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑡)) ∈ (𝐾𝐶𝐵))
72	62, 69, 71	syl2anc 586	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑡)) ∈ (𝐾𝐶𝐵))
73	5	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑠:𝐸⟶𝐸)
74	6, 43	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:𝑉⟶𝐸)
75	74	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝐻:𝑉⟶𝐸)
76	18	simp1d 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚))
77	76	simpld 497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑚 ⊆ 𝐷)
78	26, 16	mdvval 32758	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐷 = ((𝑉 × 𝑉) ∖ I )
79		difss 4096	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 × 𝑉) ∖ I ) ⊆ (𝑉 × 𝑉)
80	78, 79	eqsstri 3989	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐷 ⊆ (𝑉 × 𝑉)
81	77, 80	sstrdi 3967	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑚 ⊆ (𝑉 × 𝑉))
82	81	ssbrd 5095	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑐𝑚𝑑 → 𝑐(𝑉 × 𝑉)𝑑))
83	82	imp 409	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑐(𝑉 × 𝑉)𝑑)
84		brxp 5587	. . . . . . . . . . . . . . . 16 ⊢ (𝑐(𝑉 × 𝑉)𝑑 ↔ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))
85	83, 84	sylib 220	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))
86	85	simpld 497	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑐 ∈ 𝑉)
87	75, 86	ffvelrnd 6838	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝐻‘𝑐) ∈ 𝐸)
88		fvco3 6746	. . . . . . . . . . . . 13 ⊢ ((𝑠:𝐸⟶𝐸 ∧ (𝐻‘𝑐) ∈ 𝐸) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑐)) = (𝑆‘(𝑠‘(𝐻‘𝑐))))
89	73, 87, 88	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑐)) = (𝑆‘(𝑠‘(𝐻‘𝑐))))
90	89	fveq2d 6660	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) = (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑐)))))
91	6	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑇 ∈ mFS)
92	29	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑆 ∈ ran 𝐿)
93	73, 87	ffvelrnd 6838	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑠‘(𝐻‘𝑐)) ∈ 𝐸)
94	2, 3, 28, 27	msubvrs 32814	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻‘𝑐)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑐)))) = ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))))
95	91, 92, 93, 94	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑐)))) = ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))))
96	90, 95	eqtrd 2856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) = ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))))
97	96	eleq2d 2898	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ↔ 𝑎 ∈ ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢)))))
98		eliun 4909	. . . . . . . . 9 ⊢ (𝑎 ∈ ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))))
99	97, 98	syl6bb 289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢)))))
100	85	simprd 498	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑑 ∈ 𝑉)
101	75, 100	ffvelrnd 6838	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝐻‘𝑑) ∈ 𝐸)
102		fvco3 6746	. . . . . . . . . . . . 13 ⊢ ((𝑠:𝐸⟶𝐸 ∧ (𝐻‘𝑑) ∈ 𝐸) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)) = (𝑆‘(𝑠‘(𝐻‘𝑑))))
103	73, 101, 102	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)) = (𝑆‘(𝑠‘(𝐻‘𝑑))))
104	103	fveq2d 6660	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) = (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑑)))))
105	73, 101	ffvelrnd 6838	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑠‘(𝐻‘𝑑)) ∈ 𝐸)
106	2, 3, 28, 27	msubvrs 32814	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻‘𝑑)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑑)))) = ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))))
107	91, 92, 105, 106	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑑)))) = ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))))
108	104, 107	eqtrd 2856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) = ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))))
109	108	eleq2d 2898	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) ↔ 𝑏 ∈ ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣)))))
110		eliun 4909	. . . . . . . . 9 ⊢ (𝑏 ∈ ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))
111	109, 110	syl6bb 289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))
112	99, 111	anbi12d 632	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))))
113		reeanv 3367	. . . . . . . 8 ⊢ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))
114		simpll 765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑))))) → 𝜑)
115		brxp 5587	. . . . . . . . . . . 12 ⊢ (𝑢((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑))))𝑣 ↔ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))))
116		mclsppslem.12	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀))
117		breq12 5057	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑧𝑚𝑤 ↔ 𝑐𝑚𝑑))
118		simpl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → 𝑧 = 𝑐)
119	118	fveq2d 6660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝐻‘𝑧) = (𝐻‘𝑐))
120	119	fveq2d 6660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑠‘(𝐻‘𝑧)) = (𝑠‘(𝐻‘𝑐)))
121	120	fveq2d 6660	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻‘𝑧))) = (𝑊‘(𝑠‘(𝐻‘𝑐))))
122		simpr 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → 𝑤 = 𝑑)
123	122	fveq2d 6660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝐻‘𝑤) = (𝐻‘𝑑))
124	123	fveq2d 6660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑠‘(𝐻‘𝑤)) = (𝑠‘(𝐻‘𝑑)))
125	124	fveq2d 6660	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻‘𝑤))) = (𝑊‘(𝑠‘(𝐻‘𝑑))))
126	121, 125	xpeq12d 5572	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) = ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))))
127	126	sseq1d 3986	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀 ↔ ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀))
128	117, 127	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → ((𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀) ↔ (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀)))
129	128	spc2gv 3593	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ V ∧ 𝑑 ∈ V) → (∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀)))
130	129	el2v 3493	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀))
131	116, 130	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀))
132	131	imp 409	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀)
133	132	ssbrd 5095	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑢((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑))))𝑣 → 𝑢𝑀𝑣))
134	115, 133	syl5bir 245	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))) → 𝑢𝑀𝑣))
135	134	imp 409	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑))))) → 𝑢𝑀𝑣)
136		vex 3489	. . . . . . . . . . . . 13 ⊢ 𝑢 ∈ V
137		vex 3489	. . . . . . . . . . . . 13 ⊢ 𝑣 ∈ V
138		breq12 5057	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥𝑀𝑦 ↔ 𝑢𝑀𝑣))
139		simpl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
140	139	fveq2d 6660	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝐻‘𝑥) = (𝐻‘𝑢))
141	140	fveq2d 6660	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑆‘(𝐻‘𝑥)) = (𝑆‘(𝐻‘𝑢)))
142	141	fveq2d 6660	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻‘𝑥))) = (𝑊‘(𝑆‘(𝐻‘𝑢))))
143	142	eleq2d 2898	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ↔ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢)))))
144		simpr 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
145	144	fveq2d 6660	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝐻‘𝑦) = (𝐻‘𝑣))
146	145	fveq2d 6660	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑆‘(𝐻‘𝑦)) = (𝑆‘(𝐻‘𝑣)))
147	146	fveq2d 6660	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻‘𝑦))) = (𝑊‘(𝑆‘(𝐻‘𝑣))))
148	147	eleq2d 2898	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))) ↔ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))
149	138, 143, 148	3anbi123d 1432	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))) ↔ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))))
150	149	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) ↔ (𝜑 ∧ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))))
151	150	imbi1d 344	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏) ↔ ((𝜑 ∧ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))) → 𝑎𝐾𝑏)))
152		mclspps.8	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏)
153	136, 137, 151, 152	vtocl2 3553	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))) → 𝑎𝐾𝑏)
154	153	3exp2 1350	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑢𝑀𝑣 → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))) → 𝑎𝐾𝑏))))
155	154	imp4b 424	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢𝑀𝑣) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
156	114, 135, 155	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑))))) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
157	156	rexlimdvva 3294	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
158	113, 157	syl5bir 245	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
159	112, 158	sylbid 242	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)))) → 𝑎𝐾𝑏))
160	159	exp4b 433	. . . . 5 ⊢ (𝜑 → (𝑐𝑚𝑑 → (𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) → (𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) → 𝑎𝐾𝑏))))
161	160	3imp2 1345	. . . 4 ⊢ ((𝜑 ∧ (𝑐𝑚𝑑 ∧ 𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))))) → 𝑎𝐾𝑏)
162	16, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 61, 72, 161	mclsax 32823	. . 3 ⊢ (𝜑 → ((𝑆 ∘ 𝑠)‘𝑝) ∈ (𝐾𝐶𝐵))
163	22, 162	eqeltrrd 2914	. 2 ⊢ (𝜑 → (𝑆‘(𝑠‘𝑝)) ∈ (𝐾𝐶𝐵))
164	33	ffnd 6501	. . 3 ⊢ (𝜑 → 𝑆 Fn 𝐸)
165		elpreima 6814	. . 3 ⊢ (𝑆 Fn 𝐸 → ((𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠‘𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠‘𝑝)) ∈ (𝐾𝐶𝐵))))
166	164, 165	syl 17	. 2 ⊢ (𝜑 → ((𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠‘𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠‘𝑝)) ∈ (𝐾𝐶𝐵))))
167	20, 163, 166	mpbir2and 711	1 ⊢ (𝜑 → (𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083  ∀wal 1535   = wceq 1537   ∈ wcel 2114  ∃wrex 3139  Vcvv 3486   ∖ cdif 3921   ∪ cun 3922   ⊆ wss 3924  ⟨cotp 4561  ∪ ciun 4905   class class class wbr 5052   I cid 5445   × cxp 5539  ^◡ccnv 5540  dom cdm 5541  ran crn 5542   “ cima 5544   ∘ ccom 5545  Fun wfun 6335   Fn wfn 6336  ⟶wf 6337  ‘cfv 6341  (class class class)co 7142  Fincfn 8495  mVRcmvar 32715  mAxcmax 32719  mExcmex 32721  mDVcmdv 32722  mVarscmvrs 32723  mSubstcmsub 32725  mVHcmvh 32726  mPreStcmpst 32727  mStatcmsta 32729  mFScmfs 32730  mClscmcls 32731  mPPStcmpps 32732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-cnex 10579  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599  ax-pre-mulgt0 10600

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-pss 3942  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-tp 4558  df-op 4560  df-ot 4562  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5446  df-eprel 5451  df-po 5460  df-so 5461  df-fr 5500  df-we 5502  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-pred 6134  df-ord 6180  df-on 6181  df-lim 6182  df-suc 6183  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7567  df-1st 7675  df-2nd 7676  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-oadd 8092  df-er 8275  df-map 8394  df-pm 8395  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-card 9354  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-sub 10858  df-neg 10859  df-nn 11625  df-2 11687  df-n0 11885  df-xnn0 11955  df-z 11969  df-uz 12231  df-fz 12883  df-fzo 13024  df-seq 13360  df-hash 13681  df-word 13852  df-lsw 13900  df-concat 13908  df-s1 13935  df-substr 13988  df-pfx 14018  df-struct 16468  df-ndx 16469  df-slot 16470  df-base 16472  df-sets 16473  df-ress 16474  df-plusg 16561  df-0g 16698  df-gsum 16699  df-mgm 17835  df-sgrp 17884  df-mnd 17895  df-mhm 17939  df-submnd 17940  df-frmd 17997  df-vrmd 17998  df-mrex 32740  df-mex 32741  df-mdv 32742  df-mvrs 32743  df-mrsub 32744  df-msub 32745  df-mvh 32746  df-mpst 32747  df-msr 32748  df-msta 32749  df-mfs 32750  df-mcls 32751

This theorem is referenced by:  mclspps  32838