Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mclsppslem Structured version   Visualization version   GIF version

Theorem mclsppslem 33288
Description: The closure is closed under application of provable pre-statements. (Compare mclsax 33274.) 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.
StepHypRef Expression
1 mclsppslem.10 . . . 4 (𝜑𝑠 ∈ ran 𝐿)
2 mclspps.l . . . . 5 𝐿 = (mSubst‘𝑇)
3 mclspps.e . . . . 5 𝐸 = (mEx‘𝑇)
42, 3msubf 33237 . . . 4 (𝑠 ∈ ran 𝐿𝑠:𝐸𝐸)
51, 4syl 17 . . 3 (𝜑𝑠:𝐸𝐸)
6 mclspps.1 . . . . . . . 8 (𝜑𝑇 ∈ mFS)
7 eqid 2739 . . . . . . . . 9 (mAx‘𝑇) = (mAx‘𝑇)
8 eqid 2739 . . . . . . . . 9 (mStat‘𝑇) = (mStat‘𝑇)
97, 8maxsta 33259 . . . . . . . 8 (𝑇 ∈ mFS → (mAx‘𝑇) ⊆ (mStat‘𝑇))
106, 9syl 17 . . . . . . 7 (𝜑 → (mAx‘𝑇) ⊆ (mStat‘𝑇))
11 eqid 2739 . . . . . . . 8 (mPreSt‘𝑇) = (mPreSt‘𝑇)
1211, 8mstapst 33252 . . . . . . 7 (mStat‘𝑇) ⊆ (mPreSt‘𝑇)
1310, 12sstrdi 3929 . . . . . 6 (𝜑 → (mAx‘𝑇) ⊆ (mPreSt‘𝑇))
14 mclsppslem.9 . . . . . 6 (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑇))
1513, 14sseldd 3918 . . . . 5 (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇))
16 mclspps.d . . . . . 6 𝐷 = (mDV‘𝑇)
1716, 3, 11elmpst 33241 . . . . 5 (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑚𝐷𝑚 = 𝑚) ∧ (𝑜𝐸𝑜 ∈ Fin) ∧ 𝑝𝐸))
1815, 17sylib 221 . . . 4 (𝜑 → ((𝑚𝐷𝑚 = 𝑚) ∧ (𝑜𝐸𝑜 ∈ Fin) ∧ 𝑝𝐸))
1918simp3d 1146 . . 3 (𝜑𝑝𝐸)
205, 19ffvelrnd 6926 . 2 (𝜑 → (𝑠𝑝) ∈ 𝐸)
21 fvco3 6831 . . . 4 ((𝑠:𝐸𝐸𝑝𝐸) → ((𝑆𝑠)‘𝑝) = (𝑆‘(𝑠𝑝)))
225, 19, 21syl2anc 587 . . 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 𝐿)
302msubco 33236 . . . . 5 ((𝑆 ∈ ran 𝐿𝑠 ∈ ran 𝐿) → (𝑆𝑠) ∈ ran 𝐿)
3129, 1, 30syl2anc 587 . . . 4 (𝜑 → (𝑆𝑠) ∈ ran 𝐿)
322, 3msubf 33237 . . . . . . . . 9 (𝑆 ∈ ran 𝐿𝑆:𝐸𝐸)
3329, 32syl 17 . . . . . . . 8 (𝜑𝑆:𝐸𝐸)
34 fco 6590 . . . . . . . 8 ((𝑆:𝐸𝐸𝑠:𝐸𝐸) → (𝑆𝑠):𝐸𝐸)
3533, 5, 34syl2anc 587 . . . . . . 7 (𝜑 → (𝑆𝑠):𝐸𝐸)
3635ffnd 6567 . . . . . 6 (𝜑 → (𝑆𝑠) Fn 𝐸)
3736adantr 484 . . . . 5 ((𝜑𝑐𝑜) → (𝑆𝑠) Fn 𝐸)
38 mclsppslem.11 . . . . . . . . 9 (𝜑 → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)))
395ffund 6570 . . . . . . . . . 10 (𝜑 → Fun 𝑠)
4017simp2bi 1148 . . . . . . . . . . . . . 14 (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) → (𝑜𝐸𝑜 ∈ Fin))
4115, 40syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑜𝐸𝑜 ∈ Fin))
4241simpld 498 . . . . . . . . . . . 12 (𝜑𝑜𝐸)
4326, 3, 27mvhf 33263 . . . . . . . . . . . . 13 (𝑇 ∈ mFS → 𝐻:𝑉𝐸)
44 frn 6573 . . . . . . . . . . . . 13 (𝐻:𝑉𝐸 → ran 𝐻𝐸)
456, 43, 443syl 18 . . . . . . . . . . . 12 (𝜑 → ran 𝐻𝐸)
4642, 45unssd 4116 . . . . . . . . . . 11 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ 𝐸)
475fdmd 6577 . . . . . . . . . . 11 (𝜑 → dom 𝑠 = 𝐸)
4846, 47sseqtrrd 3958 . . . . . . . . . 10 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠)
49 funimass3 6895 . . . . . . . . . 10 ((Fun 𝑠 ∧ (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))))
5039, 48, 49syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))))
5138, 50mpbid 235 . . . . . . . 8 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵))))
52 cnvco 5771 . . . . . . . . . 10 (𝑆𝑠) = (𝑠𝑆)
5352imaeq1i 5943 . . . . . . . . 9 ((𝑆𝑠) “ (𝐾𝐶𝐵)) = ((𝑠𝑆) “ (𝐾𝐶𝐵))
54 imaco 6132 . . . . . . . . 9 ((𝑠𝑆) “ (𝐾𝐶𝐵)) = (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))
5553, 54eqtri 2767 . . . . . . . 8 ((𝑆𝑠) “ (𝐾𝐶𝐵)) = (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))
5651, 55sseqtrrdi 3968 . . . . . . 7 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
5756unssad 4117 . . . . . 6 (𝜑𝑜 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
5857sselda 3917 . . . . 5 ((𝜑𝑐𝑜) → 𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
59 elpreima 6899 . . . . . 6 ((𝑆𝑠) Fn 𝐸 → (𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)) ↔ (𝑐𝐸 ∧ ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))))
6059simplbda 503 . . . . 5 (((𝑆𝑠) Fn 𝐸𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵))) → ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
6137, 58, 60syl2anc 587 . . . 4 ((𝜑𝑐𝑜) → ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
6236adantr 484 . . . . 5 ((𝜑𝑡𝑉) → (𝑆𝑠) Fn 𝐸)
6356unssbd 4118 . . . . . . 7 (𝜑 → ran 𝐻 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
6463adantr 484 . . . . . 6 ((𝜑𝑡𝑉) → ran 𝐻 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
65 ffn 6566 . . . . . . . 8 (𝐻:𝑉𝐸𝐻 Fn 𝑉)
666, 43, 653syl 18 . . . . . . 7 (𝜑𝐻 Fn 𝑉)
67 fnfvelrn 6922 . . . . . . 7 ((𝐻 Fn 𝑉𝑡𝑉) → (𝐻𝑡) ∈ ran 𝐻)
6866, 67sylan 583 . . . . . 6 ((𝜑𝑡𝑉) → (𝐻𝑡) ∈ ran 𝐻)
6964, 68sseldd 3918 . . . . 5 ((𝜑𝑡𝑉) → (𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
70 elpreima 6899 . . . . . 6 ((𝑆𝑠) Fn 𝐸 → ((𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)) ↔ ((𝐻𝑡) ∈ 𝐸 ∧ ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))))
7170simplbda 503 . . . . 5 (((𝑆𝑠) Fn 𝐸 ∧ (𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵))) → ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))
7262, 69, 71syl2anc 587 . . . 4 ((𝜑𝑡𝑉) → ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))
735adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → 𝑠:𝐸𝐸)
746, 43syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝑉𝐸)
7574adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝐻:𝑉𝐸)
7618simp1d 1144 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑚𝐷𝑚 = 𝑚))
7776simpld 498 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑚𝐷)
7826, 16mdvval 33209 . . . . . . . . . . . . . . . . . . . 20 𝐷 = ((𝑉 × 𝑉) ∖ I )
79 difss 4062 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 × 𝑉) ∖ I ) ⊆ (𝑉 × 𝑉)
8078, 79eqsstri 3951 . . . . . . . . . . . . . . . . . . 19 𝐷 ⊆ (𝑉 × 𝑉)
8177, 80sstrdi 3929 . . . . . . . . . . . . . . . . . 18 (𝜑𝑚 ⊆ (𝑉 × 𝑉))
8281ssbrd 5112 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑐𝑚𝑑𝑐(𝑉 × 𝑉)𝑑))
8382imp 410 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝑚𝑑) → 𝑐(𝑉 × 𝑉)𝑑)
84 brxp 5615 . . . . . . . . . . . . . . . 16 (𝑐(𝑉 × 𝑉)𝑑 ↔ (𝑐𝑉𝑑𝑉))
8583, 84sylib 221 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑚𝑑) → (𝑐𝑉𝑑𝑉))
8685simpld 498 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝑐𝑉)
8775, 86ffvelrnd 6926 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → (𝐻𝑐) ∈ 𝐸)
88 fvco3 6831 . . . . . . . . . . . . 13 ((𝑠:𝐸𝐸 ∧ (𝐻𝑐) ∈ 𝐸) → ((𝑆𝑠)‘(𝐻𝑐)) = (𝑆‘(𝑠‘(𝐻𝑐))))
8973, 87, 88syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → ((𝑆𝑠)‘(𝐻𝑐)) = (𝑆‘(𝑠‘(𝐻𝑐))))
9089fveq2d 6742 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) = (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))))
916adantr 484 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → 𝑇 ∈ mFS)
9229adantr 484 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → 𝑆 ∈ ran 𝐿)
9373, 87ffvelrnd 6926 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑠‘(𝐻𝑐)) ∈ 𝐸)
942, 3, 28, 27msubvrs 33265 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻𝑐)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9591, 92, 93, 94syl3anc 1373 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9690, 95eqtrd 2779 . . . . . . . . . 10 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9796eleq2d 2825 . . . . . . . . 9 ((𝜑𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ↔ 𝑎 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢)))))
98 eliun 4924 . . . . . . . . 9 (𝑎 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))))
9997, 98bitrdi 290 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢)))))
10085simprd 499 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝑑𝑉)
10175, 100ffvelrnd 6926 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → (𝐻𝑑) ∈ 𝐸)
102 fvco3 6831 . . . . . . . . . . . . 13 ((𝑠:𝐸𝐸 ∧ (𝐻𝑑) ∈ 𝐸) → ((𝑆𝑠)‘(𝐻𝑑)) = (𝑆‘(𝑠‘(𝐻𝑑))))
10373, 101, 102syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → ((𝑆𝑠)‘(𝐻𝑑)) = (𝑆‘(𝑠‘(𝐻𝑑))))
104103fveq2d 6742 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) = (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))))
10573, 101ffvelrnd 6926 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑠‘(𝐻𝑑)) ∈ 𝐸)
1062, 3, 28, 27msubvrs 33265 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻𝑑)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
10791, 92, 105, 106syl3anc 1373 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
108104, 107eqtrd 2779 . . . . . . . . . 10 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
109108eleq2d 2825 . . . . . . . . 9 ((𝜑𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) ↔ 𝑏 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣)))))
110 eliun 4924 . . . . . . . . 9 (𝑏 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))
111109, 110bitrdi 290 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
11299, 111anbi12d 634 . . . . . . 7 ((𝜑𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))))
113 reeanv 3294 . . . . . . . 8 (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
114 simpll 767 . . . . . . . . . 10 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → 𝜑)
115 brxp 5615 . . . . . . . . . . . 12 (𝑢((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑))))𝑣 ↔ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))))
116 mclsppslem.12 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀))
117 breq12 5074 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑧𝑚𝑤𝑐𝑚𝑑))
118 simpl 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑐𝑤 = 𝑑) → 𝑧 = 𝑐)
119118fveq2d 6742 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝐻𝑧) = (𝐻𝑐))
120119fveq2d 6742 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑠‘(𝐻𝑧)) = (𝑠‘(𝐻𝑐)))
121120fveq2d 6742 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻𝑧))) = (𝑊‘(𝑠‘(𝐻𝑐))))
122 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑐𝑤 = 𝑑) → 𝑤 = 𝑑)
123122fveq2d 6742 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝐻𝑤) = (𝐻𝑑))
124123fveq2d 6742 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑠‘(𝐻𝑤)) = (𝑠‘(𝐻𝑑)))
125124fveq2d 6742 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻𝑤))) = (𝑊‘(𝑠‘(𝐻𝑑))))
126121, 125xpeq12d 5599 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = 𝑐𝑤 = 𝑑) → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) = ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))))
127126sseq1d 3948 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑐𝑤 = 𝑑) → (((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀 ↔ ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
128117, 127imbi12d 348 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑐𝑤 = 𝑑) → ((𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) ↔ (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)))
129128spc2gv 3530 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ V ∧ 𝑑 ∈ V) → (∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)))
130129el2v 3431 . . . . . . . . . . . . . . 15 (∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
131116, 130syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
132131imp 410 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)
133132ssbrd 5112 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑢((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑))))𝑣𝑢𝑀𝑣))
134115, 133syl5bir 246 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → ((𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))) → 𝑢𝑀𝑣))
135134imp 410 . . . . . . . . . 10 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → 𝑢𝑀𝑣)
136 vex 3427 . . . . . . . . . . . . 13 𝑢 ∈ V
137 vex 3427 . . . . . . . . . . . . 13 𝑣 ∈ V
138 breq12 5074 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥𝑀𝑦𝑢𝑀𝑣))
139 simpl 486 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
140139fveq2d 6742 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐻𝑥) = (𝐻𝑢))
141140fveq2d 6742 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑆‘(𝐻𝑥)) = (𝑆‘(𝐻𝑢)))
142141fveq2d 6742 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻𝑥))) = (𝑊‘(𝑆‘(𝐻𝑢))))
143142eleq2d 2825 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ↔ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢)))))
144 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
145144fveq2d 6742 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐻𝑦) = (𝐻𝑣))
146145fveq2d 6742 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑆‘(𝐻𝑦)) = (𝑆‘(𝐻𝑣)))
147146fveq2d 6742 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻𝑦))) = (𝑊‘(𝑆‘(𝐻𝑣))))
148147eleq2d 2825 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))) ↔ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
149138, 143, 1483anbi123d 1438 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦)))) ↔ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))))
150149anbi2d 632 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) ↔ (𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))))
151150imbi1d 345 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) → 𝑎𝐾𝑏) ↔ ((𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))) → 𝑎𝐾𝑏)))
152 mclspps.8 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) → 𝑎𝐾𝑏)
153136, 137, 151, 152vtocl2 3491 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))) → 𝑎𝐾𝑏)
1541533exp2 1356 . . . . . . . . . . 11 (𝜑 → (𝑢𝑀𝑣 → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))) → 𝑎𝐾𝑏))))
155154imp4b 425 . . . . . . . . . 10 ((𝜑𝑢𝑀𝑣) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
156114, 135, 155syl2anc 587 . . . . . . . . 9 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
157156rexlimdvva 3223 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
158113, 157syl5bir 246 . . . . . . 7 ((𝜑𝑐𝑚𝑑) → ((∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
159112, 158sylbid 243 . . . . . 6 ((𝜑𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑)))) → 𝑎𝐾𝑏))
160159exp4b 434 . . . . 5 (𝜑 → (𝑐𝑚𝑑 → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) → 𝑎𝐾𝑏))))
1611603imp2 1351 . . . 4 ((𝜑 ∧ (𝑐𝑚𝑑𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))))) → 𝑎𝐾𝑏)
16216, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 61, 72, 161mclsax 33274 . . 3 (𝜑 → ((𝑆𝑠)‘𝑝) ∈ (𝐾𝐶𝐵))
16322, 162eqeltrrd 2841 . 2 (𝜑 → (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))
16433ffnd 6567 . . 3 (𝜑𝑆 Fn 𝐸)
165 elpreima 6899 . . 3 (𝑆 Fn 𝐸 → ((𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))))
166164, 165syl 17 . 2 (𝜑 → ((𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))))
16720, 163, 166mpbir2and 713 1 (𝜑 → (𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089  wal 1541   = wceq 1543  wcel 2112  wrex 3065  Vcvv 3423  cdif 3880  cun 3881  wss 3883  cotp 4565   ciun 4920   class class class wbr 5069   I cid 5470   × cxp 5566  ccnv 5567  dom cdm 5568  ran crn 5569  cima 5571  ccom 5572  Fun wfun 6394   Fn wfn 6395  wf 6396  cfv 6400  (class class class)co 7234  Fincfn 8649  mVRcmvar 33166  mAxcmax 33170  mExcmex 33172  mDVcmdv 33173  mVarscmvrs 33174  mSubstcmsub 33176  mVHcmvh 33177  mPreStcmpst 33178  mStatcmsta 33180  mFScmfs 33181  mClscmcls 33182  mPPStcmpps 33183
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-cnex 10814  ax-resscn 10815  ax-1cn 10816  ax-icn 10817  ax-addcl 10818  ax-addrcl 10819  ax-mulcl 10820  ax-mulrcl 10821  ax-mulcom 10822  ax-addass 10823  ax-mulass 10824  ax-distr 10825  ax-i2m1 10826  ax-1ne0 10827  ax-1rid 10828  ax-rnegex 10829  ax-rrecex 10830  ax-cnre 10831  ax-pre-lttri 10832  ax-pre-lttrn 10833  ax-pre-ltadd 10834  ax-pre-mulgt0 10835
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-ot 4566  df-uni 4836  df-int 4876  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-om 7666  df-1st 7782  df-2nd 7783  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-1o 8225  df-er 8414  df-map 8533  df-pm 8534  df-en 8650  df-dom 8651  df-sdom 8652  df-fin 8653  df-card 9584  df-pnf 10898  df-mnf 10899  df-xr 10900  df-ltxr 10901  df-le 10902  df-sub 11093  df-neg 11094  df-nn 11860  df-2 11922  df-n0 12120  df-xnn0 12192  df-z 12206  df-uz 12468  df-fz 13125  df-fzo 13268  df-seq 13606  df-hash 13929  df-word 14102  df-lsw 14150  df-concat 14158  df-s1 14185  df-substr 14238  df-pfx 14268  df-struct 16732  df-sets 16749  df-slot 16767  df-ndx 16777  df-base 16793  df-ress 16817  df-plusg 16847  df-0g 16978  df-gsum 16979  df-mgm 18146  df-sgrp 18195  df-mnd 18206  df-mhm 18250  df-submnd 18251  df-frmd 18308  df-vrmd 18309  df-mrex 33191  df-mex 33192  df-mdv 33193  df-mvrs 33194  df-mrsub 33195  df-msub 33196  df-mvh 33197  df-mpst 33198  df-msr 33199  df-msta 33200  df-mfs 33201  df-mcls 33202
This theorem is referenced by:  mclspps  33289
  Copyright terms: Public domain W3C validator