Theorem mclsppslem 35796

Description: The closure is closed under application of provable pre-statements. (Compare mclsax 35782.) 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 35745	. . . 4 ⊢ (𝑠 ∈ ran 𝐿 → 𝑠:𝐸⟶𝐸)
5	1, 4	syl 17	. . 3 ⊢ (𝜑 → 𝑠:𝐸⟶𝐸)
6		mclspps.1	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ mFS)
7		eqid 2737	. . . . . . . . 9 ⊢ (mAx‘𝑇) = (mAx‘𝑇)
8		eqid 2737	. . . . . . . . 9 ⊢ (mStat‘𝑇) = (mStat‘𝑇)
9	7, 8	maxsta 35767	. . . . . . . 8 ⊢ (𝑇 ∈ mFS → (mAx‘𝑇) ⊆ (mStat‘𝑇))
10	6, 9	syl 17	. . . . . . 7 ⊢ (𝜑 → (mAx‘𝑇) ⊆ (mStat‘𝑇))
11		eqid 2737	. . . . . . . 8 ⊢ (mPreSt‘𝑇) = (mPreSt‘𝑇)
12	11, 8	mstapst 35760	. . . . . . 7 ⊢ (mStat‘𝑇) ⊆ (mPreSt‘𝑇)
13	10, 12	sstrdi 3948	. . . . . 6 ⊢ (𝜑 → (mAx‘𝑇) ⊆ (mPreSt‘𝑇))
14		mclsppslem.9	. . . . . 6 ⊢ (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑇))
15	13, 14	sseldd 3936	. . . . 5 ⊢ (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇))
16		mclspps.d	. . . . . 6 ⊢ 𝐷 = (mDV‘𝑇)
17	16, 3, 11	elmpst 35749	. . . . 5 ⊢ (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚) ∧ (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin) ∧ 𝑝 ∈ 𝐸))
18	15, 17	sylib 218	. . . 4 ⊢ (𝜑 → ((𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚) ∧ (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin) ∧ 𝑝 ∈ 𝐸))
19	18	simp3d 1145	. . 3 ⊢ (𝜑 → 𝑝 ∈ 𝐸)
20	5, 19	ffvelcdmd 7039	. 2 ⊢ (𝜑 → (𝑠‘𝑝) ∈ 𝐸)
21		fvco3 6941	. . . 4 ⊢ ((𝑠:𝐸⟶𝐸 ∧ 𝑝 ∈ 𝐸) → ((𝑆 ∘ 𝑠)‘𝑝) = (𝑆‘(𝑠‘𝑝)))
22	5, 19, 21	syl2anc 585	. . 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 35744	. . . . 5 ⊢ ((𝑆 ∈ ran 𝐿 ∧ 𝑠 ∈ ran 𝐿) → (𝑆 ∘ 𝑠) ∈ ran 𝐿)
31	29, 1, 30	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝑆 ∘ 𝑠) ∈ ran 𝐿)
32	2, 3	msubf 35745	. . . . . . . . 9 ⊢ (𝑆 ∈ ran 𝐿 → 𝑆:𝐸⟶𝐸)
33	29, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆:𝐸⟶𝐸)
34		fco 6694	. . . . . . . 8 ⊢ ((𝑆:𝐸⟶𝐸 ∧ 𝑠:𝐸⟶𝐸) → (𝑆 ∘ 𝑠):𝐸⟶𝐸)
35	33, 5, 34	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑆 ∘ 𝑠):𝐸⟶𝐸)
36	35	ffnd 6671	. . . . . 6 ⊢ (𝜑 → (𝑆 ∘ 𝑠) Fn 𝐸)
37	36	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑜) → (𝑆 ∘ 𝑠) Fn 𝐸)
38		mclsppslem.11	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵)))
39	5	ffund 6674	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝑠)
40	17	simp2bi 1147	. . . . . . . . . . . . . 14 ⊢ (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) → (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin))
41	15, 40	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin))
42	41	simpld 494	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑜 ⊆ 𝐸)
43	26, 3, 27	mvhf 35771	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ mFS → 𝐻:𝑉⟶𝐸)
44		frn 6677	. . . . . . . . . . . . 13 ⊢ (𝐻:𝑉⟶𝐸 → ran 𝐻 ⊆ 𝐸)
45	6, 43, 44	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝐻 ⊆ 𝐸)
46	42, 45	unssd 4146	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ 𝐸)
47	5	fdmd 6680	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑠 = 𝐸)
48	46, 47	sseqtrrd 3973	. . . . . . . . . 10 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠)
49		funimass3 7008	. . . . . . . . . 10 ⊢ ((Fun 𝑠 ∧ (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))))
50	39, 48, 49	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))))
51	38, 50	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵))))
52		cnvco 5842	. . . . . . . . . 10 ⊢ ◡(𝑆 ∘ 𝑠) = (◡𝑠 ∘ ◡𝑆)
53	52	imaeq1i 6024	. . . . . . . . 9 ⊢ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) = ((◡𝑠 ∘ ◡𝑆) “ (𝐾𝐶𝐵))
54		imaco 6217	. . . . . . . . 9 ⊢ ((◡𝑠 ∘ ◡𝑆) “ (𝐾𝐶𝐵)) = (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))
55	53, 54	eqtri 2760	. . . . . . . 8 ⊢ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) = (◡𝑠 “ (◡𝑆 “ (𝐾𝐶𝐵)))
56	51, 55	sseqtrrdi 3977	. . . . . . 7 ⊢ (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
57	56	unssad 4147	. . . . . 6 ⊢ (𝜑 → 𝑜 ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
58	57	sselda 3935	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑜) → 𝑐 ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
59		elpreima 7012	. . . . . 6 ⊢ ((𝑆 ∘ 𝑠) Fn 𝐸 → (𝑐 ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) ↔ (𝑐 ∈ 𝐸 ∧ ((𝑆 ∘ 𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))))
60	59	simplbda 499	. . . . 5 ⊢ (((𝑆 ∘ 𝑠) Fn 𝐸 ∧ 𝑐 ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵))) → ((𝑆 ∘ 𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
61	37, 58, 60	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ 𝑜) → ((𝑆 ∘ 𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
62	36	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑆 ∘ 𝑠) Fn 𝐸)
63	56	unssbd 4148	. . . . . . 7 ⊢ (𝜑 → ran 𝐻 ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
64	63	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ran 𝐻 ⊆ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
65		ffn 6670	. . . . . . . 8 ⊢ (𝐻:𝑉⟶𝐸 → 𝐻 Fn 𝑉)
66	6, 43, 65	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn 𝑉)
67		fnfvelrn 7034	. . . . . . 7 ⊢ ((𝐻 Fn 𝑉 ∧ 𝑡 ∈ 𝑉) → (𝐻‘𝑡) ∈ ran 𝐻)
68	66, 67	sylan 581	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐻‘𝑡) ∈ ran 𝐻)
69	64, 68	sseldd 3936	. . . . 5 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐻‘𝑡) ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)))
70		elpreima 7012	. . . . . 6 ⊢ ((𝑆 ∘ 𝑠) Fn 𝐸 → ((𝐻‘𝑡) ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵)) ↔ ((𝐻‘𝑡) ∈ 𝐸 ∧ ((𝑆 ∘ 𝑠)‘(𝐻‘𝑡)) ∈ (𝐾𝐶𝐵))))
71	70	simplbda 499	. . . . 5 ⊢ (((𝑆 ∘ 𝑠) Fn 𝐸 ∧ (𝐻‘𝑡) ∈ (◡(𝑆 ∘ 𝑠) “ (𝐾𝐶𝐵))) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑡)) ∈ (𝐾𝐶𝐵))
72	62, 69, 71	syl2anc 585	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑡)) ∈ (𝐾𝐶𝐵))
73	5	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑠:𝐸⟶𝐸)
74	6, 43	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻:𝑉⟶𝐸)
75	74	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝐻:𝑉⟶𝐸)
76	18	simp1d 1143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑚 ⊆ 𝐷 ∧ ◡𝑚 = 𝑚))
77	76	simpld 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑚 ⊆ 𝐷)
78	26, 16	mdvval 35717	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐷 = ((𝑉 × 𝑉) ∖ I )
79		difss 4090	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 × 𝑉) ∖ I ) ⊆ (𝑉 × 𝑉)
80	78, 79	eqsstri 3982	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐷 ⊆ (𝑉 × 𝑉)
81	77, 80	sstrdi 3948	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑚 ⊆ (𝑉 × 𝑉))
82	81	ssbrd 5143	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑐𝑚𝑑 → 𝑐(𝑉 × 𝑉)𝑑))
83	82	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑐(𝑉 × 𝑉)𝑑)
84		brxp 5681	. . . . . . . . . . . . . . . 16 ⊢ (𝑐(𝑉 × 𝑉)𝑑 ↔ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))
85	83, 84	sylib 218	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))
86	85	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑐 ∈ 𝑉)
87	75, 86	ffvelcdmd 7039	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝐻‘𝑐) ∈ 𝐸)
88		fvco3 6941	. . . . . . . . . . . . 13 ⊢ ((𝑠:𝐸⟶𝐸 ∧ (𝐻‘𝑐) ∈ 𝐸) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑐)) = (𝑆‘(𝑠‘(𝐻‘𝑐))))
89	73, 87, 88	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑐)) = (𝑆‘(𝑠‘(𝐻‘𝑐))))
90	89	fveq2d 6846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) = (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑐)))))
91	6	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑇 ∈ mFS)
92	29	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑆 ∈ ran 𝐿)
93	73, 87	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑠‘(𝐻‘𝑐)) ∈ 𝐸)
94	2, 3, 28, 27	msubvrs 35773	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻‘𝑐)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑐)))) = ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))))
95	91, 92, 93, 94	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑐)))) = ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))))
96	90, 95	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) = ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))))
97	96	eleq2d 2823	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ↔ 𝑎 ∈ ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢)))))
98		eliun 4952	. . . . . . . . 9 ⊢ (𝑎 ∈ ∪ 𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))(𝑊‘(𝑆‘(𝐻‘𝑢))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))))
99	97, 98	bitrdi 287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢)))))
100	85	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → 𝑑 ∈ 𝑉)
101	75, 100	ffvelcdmd 7039	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝐻‘𝑑) ∈ 𝐸)
102		fvco3 6941	. . . . . . . . . . . . 13 ⊢ ((𝑠:𝐸⟶𝐸 ∧ (𝐻‘𝑑) ∈ 𝐸) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)) = (𝑆‘(𝑠‘(𝐻‘𝑑))))
103	73, 101, 102	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)) = (𝑆‘(𝑠‘(𝐻‘𝑑))))
104	103	fveq2d 6846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) = (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑑)))))
105	73, 101	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑠‘(𝐻‘𝑑)) ∈ 𝐸)
106	2, 3, 28, 27	msubvrs 35773	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻‘𝑑)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑑)))) = ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))))
107	91, 92, 105, 106	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻‘𝑑)))) = ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))))
108	104, 107	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) = ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))))
109	108	eleq2d 2823	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) ↔ 𝑏 ∈ ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣)))))
110		eliun 4952	. . . . . . . . 9 ⊢ (𝑏 ∈ ∪ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑊‘(𝑆‘(𝐻‘𝑣))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))
111	109, 110	bitrdi 287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))
112	99, 111	anbi12d 633	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))))
113		reeanv 3210	. . . . . . . 8 ⊢ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))
114		simpll 767	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑))))) → 𝜑)
115		brxp 5681	. . . . . . . . . . . 12 ⊢ (𝑢((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑))))𝑣 ↔ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))))
116		mclsppslem.12	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀))
117		breq12 5105	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑧𝑚𝑤 ↔ 𝑐𝑚𝑑))
118		simpl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → 𝑧 = 𝑐)
119	118	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝐻‘𝑧) = (𝐻‘𝑐))
120	119	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑠‘(𝐻‘𝑧)) = (𝑠‘(𝐻‘𝑐)))
121	120	fveq2d 6846	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻‘𝑧))) = (𝑊‘(𝑠‘(𝐻‘𝑐))))
122		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → 𝑤 = 𝑑)
123	122	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝐻‘𝑤) = (𝐻‘𝑑))
124	123	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑠‘(𝐻‘𝑤)) = (𝑠‘(𝐻‘𝑑)))
125	124	fveq2d 6846	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻‘𝑤))) = (𝑊‘(𝑠‘(𝐻‘𝑑))))
126	121, 125	xpeq12d 5663	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) = ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))))
127	126	sseq1d 3967	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → (((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀 ↔ ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀))
128	117, 127	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 = 𝑐 ∧ 𝑤 = 𝑑) → ((𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀) ↔ (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀)))
129	128	spc2gv 3556	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ V ∧ 𝑑 ∈ V) → (∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀)))
130	129	el2v 3449	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧∀𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻‘𝑧))) × (𝑊‘(𝑠‘(𝐻‘𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀))
131	116, 130	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀))
132	131	imp 406	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑)))) ⊆ 𝑀)
133	132	ssbrd 5143	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (𝑢((𝑊‘(𝑠‘(𝐻‘𝑐))) × (𝑊‘(𝑠‘(𝐻‘𝑑))))𝑣 → 𝑢𝑀𝑣))
134	115, 133	biimtrrid 243	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))) → 𝑢𝑀𝑣))
135	134	imp 406	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑))))) → 𝑢𝑀𝑣)
136		vex 3446	. . . . . . . . . . . . 13 ⊢ 𝑢 ∈ V
137		vex 3446	. . . . . . . . . . . . 13 ⊢ 𝑣 ∈ V
138		breq12 5105	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑥𝑀𝑦 ↔ 𝑢𝑀𝑣))
139		simpl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑢)
140	139	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝐻‘𝑥) = (𝐻‘𝑢))
141	140	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑆‘(𝐻‘𝑥)) = (𝑆‘(𝐻‘𝑢)))
142	141	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻‘𝑥))) = (𝑊‘(𝑆‘(𝐻‘𝑢))))
143	142	eleq2d 2823	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ↔ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢)))))
144		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣)
145	144	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝐻‘𝑦) = (𝐻‘𝑣))
146	145	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑆‘(𝐻‘𝑦)) = (𝑆‘(𝐻‘𝑣)))
147	146	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻‘𝑦))) = (𝑊‘(𝑆‘(𝐻‘𝑣))))
148	147	eleq2d 2823	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))) ↔ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))
149	138, 143, 148	3anbi123d 1439	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦)))) ↔ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))))
150	149	anbi2d 631	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) ↔ (𝜑 ∧ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))))))
151	150	imbi1d 341	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → (((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏) ↔ ((𝜑 ∧ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))) → 𝑎𝐾𝑏)))
152		mclspps.8	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥𝑀𝑦 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑦))))) → 𝑎𝐾𝑏)
153	136, 137, 151, 152	vtocl2 3524	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢𝑀𝑣 ∧ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))))) → 𝑎𝐾𝑏)
154	153	3exp2 1356	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑢𝑀𝑣 → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣))) → 𝑎𝐾𝑏))))
155	154	imp4b 421	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢𝑀𝑣) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
156	114, 135, 155	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑))))) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
157	156	rexlimdvva 3195	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
158	113, 157	biimtrrid 243	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻‘𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻‘𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻‘𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻‘𝑣)))) → 𝑎𝐾𝑏))
159	112, 158	sylbid 240	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑)))) → 𝑎𝐾𝑏))
160	159	exp4b 430	. . . . 5 ⊢ (𝜑 → (𝑐𝑚𝑑 → (𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) → (𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))) → 𝑎𝐾𝑏))))
161	160	3imp2 1351	. . . 4 ⊢ ((𝜑 ∧ (𝑐𝑚𝑑 ∧ 𝑎 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆 ∘ 𝑠)‘(𝐻‘𝑑))))) → 𝑎𝐾𝑏)
162	16, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 61, 72, 161	mclsax 35782	. . 3 ⊢ (𝜑 → ((𝑆 ∘ 𝑠)‘𝑝) ∈ (𝐾𝐶𝐵))
163	22, 162	eqeltrrd 2838	. 2 ⊢ (𝜑 → (𝑆‘(𝑠‘𝑝)) ∈ (𝐾𝐶𝐵))
164	33	ffnd 6671	. . 3 ⊢ (𝜑 → 𝑆 Fn 𝐸)
165		elpreima 7012	. . 3 ⊢ (𝑆 Fn 𝐸 → ((𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠‘𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠‘𝑝)) ∈ (𝐾𝐶𝐵))))
166	164, 165	syl 17	. 2 ⊢ (𝜑 → ((𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠‘𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠‘𝑝)) ∈ (𝐾𝐶𝐵))))
167	20, 163, 166	mpbir2and 714	1 ⊢ (𝜑 → (𝑠‘𝑝) ∈ (◡𝑆 “ (𝐾𝐶𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087  ∀wal 1540   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  Vcvv 3442   ∖ cdif 3900   ∪ cun 3901   ⊆ wss 3903  ⟨cotp 4590  ∪ ciun 4948   class class class wbr 5100   I cid 5526   × cxp 5630  ^◡ccnv 5631  dom cdm 5632  ran crn 5633   “ cima 5635   ∘ ccom 5636  Fun wfun 6494   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  Fincfn 8895  mVRcmvar 35674  mAxcmax 35678  mExcmex 35680  mDVcmdv 35681  mVarscmvrs 35682  mSubstcmsub 35684  mVHcmvh 35685  mPreStcmpst 35686  mStatcmsta 35688  mFScmfs 35689  mClscmcls 35690  mPPStcmpps 35691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-ot 4591  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-er 8645  df-map 8777  df-pm 8778  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-2 12220  df-n0 12414  df-xnn0 12487  df-z 12501  df-uz 12764  df-fz 13436  df-fzo 13583  df-seq 13937  df-hash 14266  df-word 14449  df-lsw 14498  df-concat 14506  df-s1 14532  df-substr 14577  df-pfx 14607  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-0g 17373  df-gsum 17374  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-mhm 18720  df-submnd 18721  df-frmd 18786  df-vrmd 18787  df-mrex 35699  df-mex 35700  df-mdv 35701  df-mvrs 35702  df-mrsub 35703  df-msub 35704  df-mvh 35705  df-mpst 35706  df-msr 35707  df-msta 35708  df-mfs 35709  df-mcls 35710

This theorem is referenced by:  mclspps  35797