Theorem mclsppslem 35183

Description: The closure is closed under application of provable pre-statements. (Compare mclsax 35169.) 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 35132	. . . 4 ⊢ (𝑠 ∈ ran 𝐿 → 𝑠:𝐸⟶𝐸)
5	1, 4	syl 17	. . 3 ⊢ (𝜑 → 𝑠:𝐸⟶𝐸)
6		mclspps.1	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ mFS)
7		eqid 2727	. . . . . . . . 9 ⊢ (mAx‘𝑇) = (mAx‘𝑇)
8		eqid 2727	. . . . . . . . 9 ⊢ (mStat‘𝑇) = (mStat‘𝑇)
9	7, 8	maxsta 35154	. . . . . . . 8 ⊢ (𝑇 ∈ mFS → (mAx‘𝑇) ⊆ (mStat‘𝑇))
10	6, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → (mAx‘𝑇) ⊆ (mStat‘𝑇))
11		eqid 2727	. . . . . . . 8 ⊢ (mPreSt‘𝑇) = (mPreSt‘𝑇)
12	11, 8	mstapst 35147	. . . . . . 7 ⊢ (mStat‘𝑇) ⊆ (mPreSt‘𝑇)
13	10, 12	sstrdi 3990	. . . . . 6 ⊢ (𝜑 → (mAx‘𝑇) ⊆ (mPreSt‘𝑇))
14		mclsppslem.9	. . . . . 6 ⊢ (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑇))
15	13, 14	sseldd 3979	. . . . 5 ⊢ (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇))
16		mclspps.d	. . . . . 6 ⊢ 𝐷 = (mDV‘𝑇)
17	16, 3, 11	elmpst 35136	. . . . 5 ⊢ (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚) ∧ (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin) ∧ 𝑝 ∈ 𝐸))
18	15, 17	sylib 217	. . . 4 ⊢ (𝜑 → ((𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚) ∧ (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin) ∧ 𝑝 ∈ 𝐸))
19	18	simp3d 1142	. . 3 ⊢ (𝜑 → 𝑝 ∈ 𝐸)
20	5, 19	ffvelcdmd 7089	. 2 ⊢ (𝜑 → (𝑠‘𝑝) ∈ 𝐸)
21		fvco3 6991	. . . 4 ⊢ ((𝑠:𝐸⟶𝐸 ∧ 𝑝 ∈ 𝐸) → ((𝑆 ∘ 𝑠)‘𝑝) = (𝑆‘(𝑠‘𝑝)))
22	5, 19, 21	syl2anc 583	. . 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 35131	. . . . 5 ⊢ ((𝑆 ∈ ran 𝐿 ∧ 𝑠 ∈ ran 𝐿) → (𝑆 ∘ 𝑠) ∈ ran 𝐿)
31	29, 1, 30	syl2anc 583	. . . 4 ⊢ (𝜑 → (𝑆 ∘ 𝑠) ∈ ran 𝐿)
32	2, 3	msubf 35132	. . . . . . . . 9 ⊢ (𝑆 ∈ ran 𝐿 → 𝑆:𝐸⟶𝐸)
33	29, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:𝐸⟶𝐸)
34		fco 6741	. . . . . . . 8 ⊢ ((𝑆:𝐸⟶𝐸 ∧ 𝑠:𝐸⟶𝐸) → (𝑆 ∘ 𝑠):𝐸⟶𝐸)
35	33, 5, 34	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (𝑆 ∘ 𝑠):𝐸⟶𝐸)
36	35	ffnd 6717	. . . . . 6 ⊢ (𝜑 → (𝑆 ∘ 𝑠) Fn 𝐸)
37	36	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑜) → (𝑆 ∘ 𝑠) Fn 𝐸)
38		mclsppslem.11	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵)))
39	5	ffund 6720	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝑠)
40	17	simp2bi 1144	. . . . . . . . . . . . . 14 ⊢ (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) → (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin))
41	15, 40	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin))
42	41	simpld 494	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑜 ⊆ 𝐸)
43	26, 3, 27	mvhf 35158	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸)
44		frn 6723	. . . . . . . . . . . . 13 ⊢ (𝐻:𝑉⟶𝐸 → ran 𝐻 ⊆ 𝐸)
45	6, 43, 44	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐻 ⊆ 𝐸)
46	42, 45	unssd 4182	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ 𝐸)
47	5	fdmd 6727	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑠 = 𝐸)
48	46, 47	sseqtrrd 4019	. . . . . . . . . 10 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠)
49		funimass3 7057	. . . . . . . . . 10 ⊢ ((Fun 𝑠 ∧ (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))))
50	39, 48, 49	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))))
51	38, 50	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵))))
52		cnvco 5882	. . . . . . . . . 10 ⊢ ◡(𝑆 ∘ 𝑠) = (◡𝑠 ∘ ◡𝑆)
53	52	imaeq1i 6054	. . . . . . . . 9 ⊢ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) = ((◡𝑠 ∘ ◡𝑆) “ (𝐾𝐶𝐵))
54		imaco 6249	. . . . . . . . 9 ⊢ ((◡𝑠 ∘ ◡𝑆) “ (𝐾𝐶𝐵)) = (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))
55	53, 54	eqtri 2755	. . . . . . . 8 ⊢ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) = (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))
56	51, 55	sseqtrrdi 4029	. . . . . . 7 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
57	56	unssad 4183	. . . . . 6 ⊢ (𝜑 → 𝑜 ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
58	57	sselda 3978	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑜) → 𝑐 ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
59		elpreima 7061	. . . . . 6 ⊢ ((𝑆 ∘ 𝑠) Fn 𝐸 → (𝑐 ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) ↔ (𝑐 ∈ 𝐸 ∧ ((𝑆 ∘ 𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))))
60	59	simplbda 499	. . . . 5 ⊢ (((𝑆 ∘ 𝑠) Fn 𝐸 ∧ 𝑐 ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵))) → ((𝑆 ∘ 𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
61	37, 58, 60	syl2anc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑜) → ((𝑆 ∘ 𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
62	36	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑆 ∘ 𝑠) Fn 𝐸)
63	56	unssbd 4184	. . . . . . 7 ⊢ (𝜑 → ran 𝐻 ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
64	63	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ran 𝐻 ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
65		ffn 6716	. . . . . . . 8 ⊢ (𝐻:𝑉⟶𝐸 → 𝐻 Fn 𝑉)
66	6, 43, 65	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn 𝑉)
67		fnfvelrn 7084	. . . . . . 7 ⊢ ((𝐻 Fn 𝑉 ∧ 𝑡 ∈ 𝑉) → (𝐻‘𝑡) ∈ ran 𝐻)
68	66, 67	sylan 579	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐻‘𝑡) ∈ ran 𝐻)
69	64, 68	sseldd 3979	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐻‘𝑡) ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
70		elpreima 7061	. . . . . 6 ⊢ ((𝑆 ∘ 𝑠) Fn 𝐸 → ((𝐻‘𝑡) ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) ↔ ((𝐻‘𝑡) ∈ 𝐸 ∧ ((𝑆 ∘ 𝑠)‘(𝐻‘𝑡)) ∈ (𝐾𝐶𝐵))))
71	70	simplbda 499	. . . . 5 ⊢ (((𝑆 ∘ 𝑠) Fn 𝐸 ∧ (𝐻‘𝑡) ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵))) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑡)) ∈ (𝐾𝐶𝐵))
72	62, 69, 71	syl2anc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑡)) ∈ (𝐾𝐶𝐵))
73	5	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑠:𝐸⟶𝐸)
74	6, 43	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:𝑉⟶𝐸)
75	74	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝐻:𝑉⟶𝐸)
76	18	simp1d 1140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚))
77	76	simpld 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑚 ⊆ 𝐷)
78	26, 16	mdvval 35104	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐷 = ((𝑉 × 𝑉) ∖ I )
79		difss 4127	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 × 𝑉) ∖ I ) ⊆ (𝑉 × 𝑉)
80	78, 79	eqsstri 4012	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐷 ⊆ (𝑉 × 𝑉)
81	77, 80	sstrdi 3990	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑚 ⊆ (𝑉 × 𝑉))
82	81	ssbrd 5185	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑐𝑚𝑑 → 𝑐(𝑉 × 𝑉)𝑑))
83	82	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑐(𝑉 × 𝑉)𝑑)
84		brxp 5721	. . . . . . . . . . . . . . . 16 ⊢ (𝑐(𝑉 × 𝑉)𝑑 ↔ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))
85	83, 84	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))
86	85	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑐 ∈ 𝑉)
87	75, 86	ffvelcdmd 7089	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝐻‘𝑐) ∈ 𝐸)
88		fvco3 6991	. . . . . . . . . . . . 13 ⊢ ((𝑠:𝐸⟶𝐸 ∧ (𝐻‘𝑐) ∈ 𝐸) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑐)) = (𝑆‘(𝑠‘(𝐻‘𝑐))))
89	73, 87, 88	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑐)) = (𝑆‘(𝑠‘(𝐻‘𝑐))))
90	89	fveq2d 6895	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) = (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑐)))))
91	6	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑇 ∈ mFS)
92	29	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑆 ∈ ran 𝐿)
93	73, 87	ffvelcdmd 7089	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑠‘(𝐻‘𝑐)) ∈ 𝐸)
94	2, 3, 28, 27	msubvrs 35160	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻‘𝑐)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑐)))) = ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))))
95	91, 92, 93, 94	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑐)))) = ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))))
96	90, 95	eqtrd 2767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) = ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))))
97	96	eleq2d 2814	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ↔ 𝑎 ∈ ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢)))))
98		eliun 4995	. . . . . . . . 9 ⊢ (𝑎 ∈ ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))))
99	97, 98	bitrdi 287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢)))))
100	85	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑑 ∈ 𝑉)
101	75, 100	ffvelcdmd 7089	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝐻‘𝑑) ∈ 𝐸)
102		fvco3 6991	. . . . . . . . . . . . 13 ⊢ ((𝑠:𝐸⟶𝐸 ∧ (𝐻‘𝑑) ∈ 𝐸) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)) = (𝑆‘(𝑠‘(𝐻‘𝑑))))
103	73, 101, 102	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)) = (𝑆‘(𝑠‘(𝐻‘𝑑))))
104	103	fveq2d 6895	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) = (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑑)))))
105	73, 101	ffvelcdmd 7089	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑠‘(𝐻‘𝑑)) ∈ 𝐸)
106	2, 3, 28, 27	msubvrs 35160	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻‘𝑑)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑑)))) = ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))))
107	91, 92, 105, 106	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑑)))) = ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))))
108	104, 107	eqtrd 2767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) = ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))))
109	108	eleq2d 2814	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) ↔ 𝑏 ∈ ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣)))))
110		eliun 4995	. . . . . . . . 9 ⊢ (𝑏 ∈ ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))
111	109, 110	bitrdi 287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))
112	99, 111	anbi12d 630	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))))
113		reeanv 3221	. . . . . . . 8 ⊢ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))
114		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑))))) → 𝜑)
115		brxp 5721	. . . . . . . . . . . 12 ⊢ (𝑢((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑))))𝑣 ↔ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))))
116		mclsppslem.12	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀))
117		breq12 5147	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑧𝑚𝑤 ↔ 𝑐𝑚𝑑))
118		simpl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → 𝑧 = 𝑐)
119	118	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝐻‘𝑧) = (𝐻‘𝑐))
120	119	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑠‘(𝐻‘𝑧)) = (𝑠‘(𝐻‘𝑐)))
121	120	fveq2d 6895	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻‘𝑧))) = (𝑊‘(𝑠‘(𝐻‘𝑐))))
122		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → 𝑤 = 𝑑)
123	122	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝐻‘𝑤) = (𝐻‘𝑑))
124	123	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑠‘(𝐻‘𝑤)) = (𝑠‘(𝐻‘𝑑)))
125	124	fveq2d 6895	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻‘𝑤))) = (𝑊‘(𝑠‘(𝐻‘𝑑))))
126	121, 125	xpeq12d 5703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) = ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))))
127	126	sseq1d 4009	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀 ↔ ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀))
128	117, 127	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → ((𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀) ↔ (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀)))
129	128	spc2gv 3585	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ V ∧ 𝑑 ∈ V) → (∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀)))
130	129	el2v 3477	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀))
131	116, 130	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀))
132	131	imp 406	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀)
133	132	ssbrd 5185	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑢((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑))))𝑣 → 𝑢𝑀𝑣))
134	115, 133	biimtrrid 242	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))) → 𝑢𝑀𝑣))
135	134	imp 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑))))) → 𝑢𝑀𝑣)
136		vex 3473	. . . . . . . . . . . . 13 ⊢ 𝑢 ∈ V
137		vex 3473	. . . . . . . . . . . . 13 ⊢ 𝑣 ∈ V
138		breq12 5147	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥𝑀𝑦 ↔ 𝑢𝑀𝑣))
139		simpl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
140	139	fveq2d 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝐻‘𝑥) = (𝐻‘𝑢))
141	140	fveq2d 6895	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑆‘(𝐻‘𝑥)) = (𝑆‘(𝐻‘𝑢)))
142	141	fveq2d 6895	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻‘𝑥))) = (𝑊‘(𝑆‘(𝐻‘𝑢))))
143	142	eleq2d 2814	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ↔ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢)))))
144		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
145	144	fveq2d 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝐻‘𝑦) = (𝐻‘𝑣))
146	145	fveq2d 6895	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑆‘(𝐻‘𝑦)) = (𝑆‘(𝐻‘𝑣)))
147	146	fveq2d 6895	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻‘𝑦))) = (𝑊‘(𝑆‘(𝐻‘𝑣))))
148	147	eleq2d 2814	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))) ↔ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))
149	138, 143, 148	3anbi123d 1433	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))) ↔ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))))
150	149	anbi2d 628	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) ↔ (𝜑 ∧ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))))
151	150	imbi1d 341	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏) ↔ ((𝜑 ∧ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))) → 𝑎𝐾𝑏)))
152		mclspps.8	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏)
153	136, 137, 151, 152	vtocl2 3550	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))) → 𝑎𝐾𝑏)
154	153	3exp2 1352	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑢𝑀𝑣 → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))) → 𝑎𝐾𝑏))))
155	154	imp4b 421	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢𝑀𝑣) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
156	114, 135, 155	syl2anc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑))))) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
157	156	rexlimdvva 3206	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
158	113, 157	biimtrrid 242	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
159	112, 158	sylbid 239	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)))) → 𝑎𝐾𝑏))
160	159	exp4b 430	. . . . 5 ⊢ (𝜑 → (𝑐𝑚𝑑 → (𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) → (𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) → 𝑎𝐾𝑏))))
161	160	3imp2 1347	. . . 4 ⊢ ((𝜑 ∧ (𝑐𝑚𝑑 ∧ 𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))))) → 𝑎𝐾𝑏)
162	16, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 61, 72, 161	mclsax 35169	. . 3 ⊢ (𝜑 → ((𝑆 ∘ 𝑠)‘𝑝) ∈ (𝐾𝐶𝐵))
163	22, 162	eqeltrrd 2829	. 2 ⊢ (𝜑 → (𝑆‘(𝑠‘𝑝)) ∈ (𝐾𝐶𝐵))
164	33	ffnd 6717	. . 3 ⊢ (𝜑 → 𝑆 Fn 𝐸)
165		elpreima 7061	. . 3 ⊢ (𝑆 Fn 𝐸 → ((𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠‘𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠‘𝑝)) ∈ (𝐾𝐶𝐵))))
166	164, 165	syl 17	. 2 ⊢ (𝜑 → ((𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠‘𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠‘𝑝)) ∈ (𝐾𝐶𝐵))))
167	20, 163, 166	mpbir2and 712	1 ⊢ (𝜑 → (𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1532   = wceq 1534   ∈ wcel 2099  ∃wrex 3065  Vcvv 3469   ∖ cdif 3941   ∪ cun 3942   ⊆ wss 3944  ⟨cotp 4632  ∪ ciun 4991   class class class wbr 5142   I cid 5569   × cxp 5670  ^◡ccnv 5671  dom cdm 5672  ran crn 5673   “ cima 5675   ∘ ccom 5676  Fun wfun 6536   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542  (class class class)co 7414  Fincfn 8957  mVRcmvar 35061  mAxcmax 35065  mExcmex 35067  mDVcmdv 35068  mVarscmvrs 35069  mSubstcmsub 35071  mVHcmvh 35072  mPreStcmpst 35073  mStatcmsta 35075  mFScmfs 35076  mClscmcls 35077  mPPStcmpps 35078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11188  ax-resscn 11189  ax-1cn 11190  ax-icn 11191  ax-addcl 11192  ax-addrcl 11193  ax-mulcl 11194  ax-mulrcl 11195  ax-mulcom 11196  ax-addass 11197  ax-mulass 11198  ax-distr 11199  ax-i2m1 11200  ax-1ne0 11201  ax-1rid 11202  ax-rnegex 11203  ax-rrecex 11204  ax-cnre 11205  ax-pre-lttri 11206  ax-pre-lttrn 11207  ax-pre-ltadd 11208  ax-pre-mulgt0 11209

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-ot 4633  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8840  df-pm 8841  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-card 9956  df-pnf 11274  df-mnf 11275  df-xr 11276  df-ltxr 11277  df-le 11278  df-sub 11470  df-neg 11471  df-nn 12237  df-2 12299  df-n0 12497  df-xnn0 12569  df-z 12583  df-uz 12847  df-fz 13511  df-fzo 13654  df-seq 13993  df-hash 14316  df-word 14491  df-lsw 14539  df-concat 14547  df-s1 14572  df-substr 14617  df-pfx 14647  df-struct 17109  df-sets 17126  df-slot 17144  df-ndx 17156  df-base 17174  df-ress 17203  df-plusg 17239  df-0g 17416  df-gsum 17417  df-mgm 18593  df-sgrp 18672  df-mnd 18688  df-mhm 18733  df-submnd 18734  df-frmd 18794  df-vrmd 18795  df-mrex 35086  df-mex 35087  df-mdv 35088  df-mvrs 35089  df-mrsub 35090  df-msub 35091  df-mvh 35092  df-mpst 35093  df-msr 35094  df-msta 35095  df-mfs 35096  df-mcls 35097

This theorem is referenced by:  mclspps  35184