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 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.
StepHypRef Expression
1 mclsppslem.10 . . . 4 (𝜑𝑠 ∈ ran 𝐿)
2 mclspps.l . . . . 5 𝐿 = (mSubst‘𝑇)
3 mclspps.e . . . . 5 𝐸 = (mEx‘𝑇)
42, 3msubf 35132 . . . 4 (𝑠 ∈ ran 𝐿𝑠:𝐸𝐸)
51, 4syl 17 . . 3 (𝜑𝑠:𝐸𝐸)
6 mclspps.1 . . . . . . . 8 (𝜑𝑇 ∈ mFS)
7 eqid 2727 . . . . . . . . 9 (mAx‘𝑇) = (mAx‘𝑇)
8 eqid 2727 . . . . . . . . 9 (mStat‘𝑇) = (mStat‘𝑇)
97, 8maxsta 35154 . . . . . . . 8 (𝑇 ∈ mFS → (mAx‘𝑇) ⊆ (mStat‘𝑇))
106, 9syl 17 . . . . . . 7 (𝜑 → (mAx‘𝑇) ⊆ (mStat‘𝑇))
11 eqid 2727 . . . . . . . 8 (mPreSt‘𝑇) = (mPreSt‘𝑇)
1211, 8mstapst 35147 . . . . . . 7 (mStat‘𝑇) ⊆ (mPreSt‘𝑇)
1310, 12sstrdi 3990 . . . . . 6 (𝜑 → (mAx‘𝑇) ⊆ (mPreSt‘𝑇))
14 mclsppslem.9 . . . . . 6 (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑇))
1513, 14sseldd 3979 . . . . 5 (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇))
16 mclspps.d . . . . . 6 𝐷 = (mDV‘𝑇)
1716, 3, 11elmpst 35136 . . . . 5 (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑚𝐷𝑚 = 𝑚) ∧ (𝑜𝐸𝑜 ∈ Fin) ∧ 𝑝𝐸))
1815, 17sylib 217 . . . 4 (𝜑 → ((𝑚𝐷𝑚 = 𝑚) ∧ (𝑜𝐸𝑜 ∈ Fin) ∧ 𝑝𝐸))
1918simp3d 1142 . . 3 (𝜑𝑝𝐸)
205, 19ffvelcdmd 7089 . 2 (𝜑 → (𝑠𝑝) ∈ 𝐸)
21 fvco3 6991 . . . 4 ((𝑠:𝐸𝐸𝑝𝐸) → ((𝑆𝑠)‘𝑝) = (𝑆‘(𝑠𝑝)))
225, 19, 21syl2anc 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 𝐿)
302msubco 35131 . . . . 5 ((𝑆 ∈ ran 𝐿𝑠 ∈ ran 𝐿) → (𝑆𝑠) ∈ ran 𝐿)
3129, 1, 30syl2anc 583 . . . 4 (𝜑 → (𝑆𝑠) ∈ ran 𝐿)
322, 3msubf 35132 . . . . . . . . 9 (𝑆 ∈ ran 𝐿𝑆:𝐸𝐸)
3329, 32syl 17 . . . . . . . 8 (𝜑𝑆:𝐸𝐸)
34 fco 6741 . . . . . . . 8 ((𝑆:𝐸𝐸𝑠:𝐸𝐸) → (𝑆𝑠):𝐸𝐸)
3533, 5, 34syl2anc 583 . . . . . . 7 (𝜑 → (𝑆𝑠):𝐸𝐸)
3635ffnd 6717 . . . . . 6 (𝜑 → (𝑆𝑠) Fn 𝐸)
3736adantr 480 . . . . 5 ((𝜑𝑐𝑜) → (𝑆𝑠) Fn 𝐸)
38 mclsppslem.11 . . . . . . . . 9 (𝜑 → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)))
395ffund 6720 . . . . . . . . . 10 (𝜑 → Fun 𝑠)
4017simp2bi 1144 . . . . . . . . . . . . . 14 (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) → (𝑜𝐸𝑜 ∈ Fin))
4115, 40syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑜𝐸𝑜 ∈ Fin))
4241simpld 494 . . . . . . . . . . . 12 (𝜑𝑜𝐸)
4326, 3, 27mvhf 35158 . . . . . . . . . . . . 13 (𝑇 ∈ mFS → 𝐻:𝑉𝐸)
44 frn 6723 . . . . . . . . . . . . 13 (𝐻:𝑉𝐸 → ran 𝐻𝐸)
456, 43, 443syl 18 . . . . . . . . . . . 12 (𝜑 → ran 𝐻𝐸)
4642, 45unssd 4182 . . . . . . . . . . 11 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ 𝐸)
475fdmd 6727 . . . . . . . . . . 11 (𝜑 → dom 𝑠 = 𝐸)
4846, 47sseqtrrd 4019 . . . . . . . . . 10 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠)
49 funimass3 7057 . . . . . . . . . 10 ((Fun 𝑠 ∧ (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))))
5039, 48, 49syl2anc 583 . . . . . . . . 9 (𝜑 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))))
5138, 50mpbid 231 . . . . . . . 8 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵))))
52 cnvco 5882 . . . . . . . . . 10 (𝑆𝑠) = (𝑠𝑆)
5352imaeq1i 6054 . . . . . . . . 9 ((𝑆𝑠) “ (𝐾𝐶𝐵)) = ((𝑠𝑆) “ (𝐾𝐶𝐵))
54 imaco 6249 . . . . . . . . 9 ((𝑠𝑆) “ (𝐾𝐶𝐵)) = (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))
5553, 54eqtri 2755 . . . . . . . 8 ((𝑆𝑠) “ (𝐾𝐶𝐵)) = (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))
5651, 55sseqtrrdi 4029 . . . . . . 7 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
5756unssad 4183 . . . . . 6 (𝜑𝑜 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
5857sselda 3978 . . . . 5 ((𝜑𝑐𝑜) → 𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
59 elpreima 7061 . . . . . 6 ((𝑆𝑠) Fn 𝐸 → (𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)) ↔ (𝑐𝐸 ∧ ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))))
6059simplbda 499 . . . . 5 (((𝑆𝑠) Fn 𝐸𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵))) → ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
6137, 58, 60syl2anc 583 . . . 4 ((𝜑𝑐𝑜) → ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
6236adantr 480 . . . . 5 ((𝜑𝑡𝑉) → (𝑆𝑠) Fn 𝐸)
6356unssbd 4184 . . . . . . 7 (𝜑 → ran 𝐻 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
6463adantr 480 . . . . . 6 ((𝜑𝑡𝑉) → ran 𝐻 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
65 ffn 6716 . . . . . . . 8 (𝐻:𝑉𝐸𝐻 Fn 𝑉)
666, 43, 653syl 18 . . . . . . 7 (𝜑𝐻 Fn 𝑉)
67 fnfvelrn 7084 . . . . . . 7 ((𝐻 Fn 𝑉𝑡𝑉) → (𝐻𝑡) ∈ ran 𝐻)
6866, 67sylan 579 . . . . . 6 ((𝜑𝑡𝑉) → (𝐻𝑡) ∈ ran 𝐻)
6964, 68sseldd 3979 . . . . 5 ((𝜑𝑡𝑉) → (𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
70 elpreima 7061 . . . . . 6 ((𝑆𝑠) Fn 𝐸 → ((𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)) ↔ ((𝐻𝑡) ∈ 𝐸 ∧ ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))))
7170simplbda 499 . . . . 5 (((𝑆𝑠) Fn 𝐸 ∧ (𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵))) → ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))
7262, 69, 71syl2anc 583 . . . 4 ((𝜑𝑡𝑉) → ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))
735adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → 𝑠:𝐸𝐸)
746, 43syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝑉𝐸)
7574adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝐻:𝑉𝐸)
7618simp1d 1140 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑚𝐷𝑚 = 𝑚))
7776simpld 494 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑚𝐷)
7826, 16mdvval 35104 . . . . . . . . . . . . . . . . . . . 20 𝐷 = ((𝑉 × 𝑉) ∖ I )
79 difss 4127 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 × 𝑉) ∖ I ) ⊆ (𝑉 × 𝑉)
8078, 79eqsstri 4012 . . . . . . . . . . . . . . . . . . 19 𝐷 ⊆ (𝑉 × 𝑉)
8177, 80sstrdi 3990 . . . . . . . . . . . . . . . . . 18 (𝜑𝑚 ⊆ (𝑉 × 𝑉))
8281ssbrd 5185 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑐𝑚𝑑𝑐(𝑉 × 𝑉)𝑑))
8382imp 406 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝑚𝑑) → 𝑐(𝑉 × 𝑉)𝑑)
84 brxp 5721 . . . . . . . . . . . . . . . 16 (𝑐(𝑉 × 𝑉)𝑑 ↔ (𝑐𝑉𝑑𝑉))
8583, 84sylib 217 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑚𝑑) → (𝑐𝑉𝑑𝑉))
8685simpld 494 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝑐𝑉)
8775, 86ffvelcdmd 7089 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → (𝐻𝑐) ∈ 𝐸)
88 fvco3 6991 . . . . . . . . . . . . 13 ((𝑠:𝐸𝐸 ∧ (𝐻𝑐) ∈ 𝐸) → ((𝑆𝑠)‘(𝐻𝑐)) = (𝑆‘(𝑠‘(𝐻𝑐))))
8973, 87, 88syl2anc 583 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → ((𝑆𝑠)‘(𝐻𝑐)) = (𝑆‘(𝑠‘(𝐻𝑐))))
9089fveq2d 6895 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) = (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))))
916adantr 480 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → 𝑇 ∈ mFS)
9229adantr 480 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → 𝑆 ∈ ran 𝐿)
9373, 87ffvelcdmd 7089 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑠‘(𝐻𝑐)) ∈ 𝐸)
942, 3, 28, 27msubvrs 35160 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻𝑐)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9591, 92, 93, 94syl3anc 1369 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9690, 95eqtrd 2767 . . . . . . . . . 10 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9796eleq2d 2814 . . . . . . . . 9 ((𝜑𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ↔ 𝑎 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢)))))
98 eliun 4995 . . . . . . . . 9 (𝑎 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))))
9997, 98bitrdi 287 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢)))))
10085simprd 495 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝑑𝑉)
10175, 100ffvelcdmd 7089 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → (𝐻𝑑) ∈ 𝐸)
102 fvco3 6991 . . . . . . . . . . . . 13 ((𝑠:𝐸𝐸 ∧ (𝐻𝑑) ∈ 𝐸) → ((𝑆𝑠)‘(𝐻𝑑)) = (𝑆‘(𝑠‘(𝐻𝑑))))
10373, 101, 102syl2anc 583 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → ((𝑆𝑠)‘(𝐻𝑑)) = (𝑆‘(𝑠‘(𝐻𝑑))))
104103fveq2d 6895 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) = (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))))
10573, 101ffvelcdmd 7089 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑠‘(𝐻𝑑)) ∈ 𝐸)
1062, 3, 28, 27msubvrs 35160 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻𝑑)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
10791, 92, 105, 106syl3anc 1369 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
108104, 107eqtrd 2767 . . . . . . . . . 10 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
109108eleq2d 2814 . . . . . . . . 9 ((𝜑𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) ↔ 𝑏 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣)))))
110 eliun 4995 . . . . . . . . 9 (𝑏 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))
111109, 110bitrdi 287 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
11299, 111anbi12d 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 ((𝑧 = 𝑐𝑤 = 𝑑) → 𝑧 = 𝑐)
119118fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝐻𝑧) = (𝐻𝑐))
120119fveq2d 6895 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑠‘(𝐻𝑧)) = (𝑠‘(𝐻𝑐)))
121120fveq2d 6895 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻𝑧))) = (𝑊‘(𝑠‘(𝐻𝑐))))
122 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑐𝑤 = 𝑑) → 𝑤 = 𝑑)
123122fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝐻𝑤) = (𝐻𝑑))
124123fveq2d 6895 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑠‘(𝐻𝑤)) = (𝑠‘(𝐻𝑑)))
125124fveq2d 6895 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻𝑤))) = (𝑊‘(𝑠‘(𝐻𝑑))))
126121, 125xpeq12d 5703 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = 𝑐𝑤 = 𝑑) → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) = ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))))
127126sseq1d 4009 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑐𝑤 = 𝑑) → (((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀 ↔ ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
128117, 127imbi12d 344 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑐𝑤 = 𝑑) → ((𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) ↔ (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)))
129128spc2gv 3585 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ V ∧ 𝑑 ∈ V) → (∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)))
130129el2v 3477 . . . . . . . . . . . . . . 15 (∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
131116, 130syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
132131imp 406 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)
133132ssbrd 5185 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑢((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑))))𝑣𝑢𝑀𝑣))
134115, 133biimtrrid 242 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → ((𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))) → 𝑢𝑀𝑣))
135134imp 406 . . . . . . . . . 10 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → 𝑢𝑀𝑣)
136 vex 3473 . . . . . . . . . . . . 13 𝑢 ∈ V
137 vex 3473 . . . . . . . . . . . . 13 𝑣 ∈ V
138 breq12 5147 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥𝑀𝑦𝑢𝑀𝑣))
139 simpl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
140139fveq2d 6895 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐻𝑥) = (𝐻𝑢))
141140fveq2d 6895 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑆‘(𝐻𝑥)) = (𝑆‘(𝐻𝑢)))
142141fveq2d 6895 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻𝑥))) = (𝑊‘(𝑆‘(𝐻𝑢))))
143142eleq2d 2814 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ↔ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢)))))
144 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
145144fveq2d 6895 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐻𝑦) = (𝐻𝑣))
146145fveq2d 6895 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑆‘(𝐻𝑦)) = (𝑆‘(𝐻𝑣)))
147146fveq2d 6895 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻𝑦))) = (𝑊‘(𝑆‘(𝐻𝑣))))
148147eleq2d 2814 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))) ↔ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
149138, 143, 1483anbi123d 1433 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦)))) ↔ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))))
150149anbi2d 628 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) ↔ (𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))))
151150imbi1d 341 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) → 𝑎𝐾𝑏) ↔ ((𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))) → 𝑎𝐾𝑏)))
152 mclspps.8 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) → 𝑎𝐾𝑏)
153136, 137, 151, 152vtocl2 3550 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))) → 𝑎𝐾𝑏)
1541533exp2 1352 . . . . . . . . . . 11 (𝜑 → (𝑢𝑀𝑣 → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))) → 𝑎𝐾𝑏))))
155154imp4b 421 . . . . . . . . . 10 ((𝜑𝑢𝑀𝑣) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
156114, 135, 155syl2anc 583 . . . . . . . . 9 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
157156rexlimdvva 3206 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
158113, 157biimtrrid 242 . . . . . . 7 ((𝜑𝑐𝑚𝑑) → ((∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
159112, 158sylbid 239 . . . . . 6 ((𝜑𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑)))) → 𝑎𝐾𝑏))
160159exp4b 430 . . . . 5 (𝜑 → (𝑐𝑚𝑑 → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) → 𝑎𝐾𝑏))))
1611603imp2 1347 . . . 4 ((𝜑 ∧ (𝑐𝑚𝑑𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))))) → 𝑎𝐾𝑏)
16216, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 61, 72, 161mclsax 35169 . . 3 (𝜑 → ((𝑆𝑠)‘𝑝) ∈ (𝐾𝐶𝐵))
16322, 162eqeltrrd 2829 . 2 (𝜑 → (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))
16433ffnd 6717 . . 3 (𝜑𝑆 Fn 𝐸)
165 elpreima 7061 . . 3 (𝑆 Fn 𝐸 → ((𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))))
166164, 165syl 17 . 2 (𝜑 → ((𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))))
16720, 163, 166mpbir2and 712 1 (𝜑 → (𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator