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 32838
Description: The closure is closed under application of provable pre-statements. (Compare mclsax 32824.) 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 32787 . . . 4 (𝑠 ∈ ran 𝐿𝑠:𝐸𝐸)
51, 4syl 17 . . 3 (𝜑𝑠:𝐸𝐸)
6 mclspps.1 . . . . . . . 8 (𝜑𝑇 ∈ mFS)
7 eqid 2821 . . . . . . . . 9 (mAx‘𝑇) = (mAx‘𝑇)
8 eqid 2821 . . . . . . . . 9 (mStat‘𝑇) = (mStat‘𝑇)
97, 8maxsta 32809 . . . . . . . 8 (𝑇 ∈ mFS → (mAx‘𝑇) ⊆ (mStat‘𝑇))
106, 9syl 17 . . . . . . 7 (𝜑 → (mAx‘𝑇) ⊆ (mStat‘𝑇))
11 eqid 2821 . . . . . . . 8 (mPreSt‘𝑇) = (mPreSt‘𝑇)
1211, 8mstapst 32802 . . . . . . 7 (mStat‘𝑇) ⊆ (mPreSt‘𝑇)
1310, 12sstrdi 3955 . . . . . 6 (𝜑 → (mAx‘𝑇) ⊆ (mPreSt‘𝑇))
14 mclsppslem.9 . . . . . 6 (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑇))
1513, 14sseldd 3944 . . . . 5 (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇))
16 mclspps.d . . . . . 6 𝐷 = (mDV‘𝑇)
1716, 3, 11elmpst 32791 . . . . 5 (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑚𝐷𝑚 = 𝑚) ∧ (𝑜𝐸𝑜 ∈ Fin) ∧ 𝑝𝐸))
1815, 17sylib 221 . . . 4 (𝜑 → ((𝑚𝐷𝑚 = 𝑚) ∧ (𝑜𝐸𝑜 ∈ Fin) ∧ 𝑝𝐸))
1918simp3d 1141 . . 3 (𝜑𝑝𝐸)
205, 19ffvelrnd 6825 . 2 (𝜑 → (𝑠𝑝) ∈ 𝐸)
21 fvco3 6733 . . . 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 32786 . . . . 5 ((𝑆 ∈ ran 𝐿𝑠 ∈ ran 𝐿) → (𝑆𝑠) ∈ ran 𝐿)
3129, 1, 30syl2anc 587 . . . 4 (𝜑 → (𝑆𝑠) ∈ ran 𝐿)
322, 3msubf 32787 . . . . . . . . 9 (𝑆 ∈ ran 𝐿𝑆:𝐸𝐸)
3329, 32syl 17 . . . . . . . 8 (𝜑𝑆:𝐸𝐸)
34 fco 6504 . . . . . . . 8 ((𝑆:𝐸𝐸𝑠:𝐸𝐸) → (𝑆𝑠):𝐸𝐸)
3533, 5, 34syl2anc 587 . . . . . . 7 (𝜑 → (𝑆𝑠):𝐸𝐸)
3635ffnd 6488 . . . . . 6 (𝜑 → (𝑆𝑠) Fn 𝐸)
3736adantr 484 . . . . 5 ((𝜑𝑐𝑜) → (𝑆𝑠) Fn 𝐸)
38 mclsppslem.11 . . . . . . . . 9 (𝜑 → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)))
395ffund 6491 . . . . . . . . . 10 (𝜑 → Fun 𝑠)
4017simp2bi 1143 . . . . . . . . . . . . . 14 (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) → (𝑜𝐸𝑜 ∈ Fin))
4115, 40syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑜𝐸𝑜 ∈ Fin))
4241simpld 498 . . . . . . . . . . . 12 (𝜑𝑜𝐸)
4326, 3, 27mvhf 32813 . . . . . . . . . . . . 13 (𝑇 ∈ mFS → 𝐻:𝑉𝐸)
44 frn 6493 . . . . . . . . . . . . 13 (𝐻:𝑉𝐸 → ran 𝐻𝐸)
456, 43, 443syl 18 . . . . . . . . . . . 12 (𝜑 → ran 𝐻𝐸)
4642, 45unssd 4138 . . . . . . . . . . 11 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ 𝐸)
475fdmd 6496 . . . . . . . . . . 11 (𝜑 → dom 𝑠 = 𝐸)
4846, 47sseqtrrd 3984 . . . . . . . . . 10 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠)
49 funimass3 6797 . . . . . . . . . 10 ((Fun 𝑠 ∧ (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))))
5039, 48, 49syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))))
5138, 50mpbid 235 . . . . . . . 8 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵))))
52 cnvco 5729 . . . . . . . . . 10 (𝑆𝑠) = (𝑠𝑆)
5352imaeq1i 5899 . . . . . . . . 9 ((𝑆𝑠) “ (𝐾𝐶𝐵)) = ((𝑠𝑆) “ (𝐾𝐶𝐵))
54 imaco 6077 . . . . . . . . 9 ((𝑠𝑆) “ (𝐾𝐶𝐵)) = (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))
5553, 54eqtri 2844 . . . . . . . 8 ((𝑆𝑠) “ (𝐾𝐶𝐵)) = (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))
5651, 55sseqtrrdi 3994 . . . . . . 7 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
5756unssad 4139 . . . . . 6 (𝜑𝑜 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
5857sselda 3943 . . . . 5 ((𝜑𝑐𝑜) → 𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
59 elpreima 6801 . . . . . 6 ((𝑆𝑠) Fn 𝐸 → (𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)) ↔ (𝑐𝐸 ∧ ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))))
6059simplbda 503 . . . . 5 (((𝑆𝑠) Fn 𝐸𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵))) → ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
6137, 58, 60syl2anc 587 . . . 4 ((𝜑𝑐𝑜) → ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
6236adantr 484 . . . . 5 ((𝜑𝑡𝑉) → (𝑆𝑠) Fn 𝐸)
6356unssbd 4140 . . . . . . 7 (𝜑 → ran 𝐻 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
6463adantr 484 . . . . . 6 ((𝜑𝑡𝑉) → ran 𝐻 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
65 ffn 6487 . . . . . . . 8 (𝐻:𝑉𝐸𝐻 Fn 𝑉)
666, 43, 653syl 18 . . . . . . 7 (𝜑𝐻 Fn 𝑉)
67 fnfvelrn 6821 . . . . . . 7 ((𝐻 Fn 𝑉𝑡𝑉) → (𝐻𝑡) ∈ ran 𝐻)
6866, 67sylan 583 . . . . . 6 ((𝜑𝑡𝑉) → (𝐻𝑡) ∈ ran 𝐻)
6964, 68sseldd 3944 . . . . 5 ((𝜑𝑡𝑉) → (𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
70 elpreima 6801 . . . . . 6 ((𝑆𝑠) Fn 𝐸 → ((𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)) ↔ ((𝐻𝑡) ∈ 𝐸 ∧ ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))))
7170simplbda 503 . . . . 5 (((𝑆𝑠) Fn 𝐸 ∧ (𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵))) → ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))
7262, 69, 71syl2anc 587 . . . 4 ((𝜑𝑡𝑉) → ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))
735adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → 𝑠:𝐸𝐸)
746, 43syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝑉𝐸)
7574adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝐻:𝑉𝐸)
7618simp1d 1139 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑚𝐷𝑚 = 𝑚))
7776simpld 498 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑚𝐷)
7826, 16mdvval 32759 . . . . . . . . . . . . . . . . . . . 20 𝐷 = ((𝑉 × 𝑉) ∖ I )
79 difss 4084 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 × 𝑉) ∖ I ) ⊆ (𝑉 × 𝑉)
8078, 79eqsstri 3977 . . . . . . . . . . . . . . . . . . 19 𝐷 ⊆ (𝑉 × 𝑉)
8177, 80sstrdi 3955 . . . . . . . . . . . . . . . . . 18 (𝜑𝑚 ⊆ (𝑉 × 𝑉))
8281ssbrd 5082 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑐𝑚𝑑𝑐(𝑉 × 𝑉)𝑑))
8382imp 410 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝑚𝑑) → 𝑐(𝑉 × 𝑉)𝑑)
84 brxp 5574 . . . . . . . . . . . . . . . 16 (𝑐(𝑉 × 𝑉)𝑑 ↔ (𝑐𝑉𝑑𝑉))
8583, 84sylib 221 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑚𝑑) → (𝑐𝑉𝑑𝑉))
8685simpld 498 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝑐𝑉)
8775, 86ffvelrnd 6825 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → (𝐻𝑐) ∈ 𝐸)
88 fvco3 6733 . . . . . . . . . . . . 13 ((𝑠:𝐸𝐸 ∧ (𝐻𝑐) ∈ 𝐸) → ((𝑆𝑠)‘(𝐻𝑐)) = (𝑆‘(𝑠‘(𝐻𝑐))))
8973, 87, 88syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → ((𝑆𝑠)‘(𝐻𝑐)) = (𝑆‘(𝑠‘(𝐻𝑐))))
9089fveq2d 6647 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) = (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))))
916adantr 484 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → 𝑇 ∈ mFS)
9229adantr 484 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → 𝑆 ∈ ran 𝐿)
9373, 87ffvelrnd 6825 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑠‘(𝐻𝑐)) ∈ 𝐸)
942, 3, 28, 27msubvrs 32815 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻𝑐)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9591, 92, 93, 94syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9690, 95eqtrd 2856 . . . . . . . . . 10 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9796eleq2d 2897 . . . . . . . . 9 ((𝜑𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ↔ 𝑎 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢)))))
98 eliun 4896 . . . . . . . . 9 (𝑎 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))))
9997, 98syl6bb 290 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢)))))
10085simprd 499 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝑑𝑉)
10175, 100ffvelrnd 6825 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → (𝐻𝑑) ∈ 𝐸)
102 fvco3 6733 . . . . . . . . . . . . 13 ((𝑠:𝐸𝐸 ∧ (𝐻𝑑) ∈ 𝐸) → ((𝑆𝑠)‘(𝐻𝑑)) = (𝑆‘(𝑠‘(𝐻𝑑))))
10373, 101, 102syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → ((𝑆𝑠)‘(𝐻𝑑)) = (𝑆‘(𝑠‘(𝐻𝑑))))
104103fveq2d 6647 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) = (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))))
10573, 101ffvelrnd 6825 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑠‘(𝐻𝑑)) ∈ 𝐸)
1062, 3, 28, 27msubvrs 32815 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻𝑑)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
10791, 92, 105, 106syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
108104, 107eqtrd 2856 . . . . . . . . . 10 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
109108eleq2d 2897 . . . . . . . . 9 ((𝜑𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) ↔ 𝑏 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣)))))
110 eliun 4896 . . . . . . . . 9 (𝑏 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))
111109, 110syl6bb 290 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
11299, 111anbi12d 633 . . . . . . 7 ((𝜑𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))))
113 reeanv 3352 . . . . . . . 8 (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
114 simpll 766 . . . . . . . . . 10 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → 𝜑)
115 brxp 5574 . . . . . . . . . . . 12 (𝑢((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑))))𝑣 ↔ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))))
116 mclsppslem.12 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀))
117 breq12 5044 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑧𝑚𝑤𝑐𝑚𝑑))
118 simpl 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑐𝑤 = 𝑑) → 𝑧 = 𝑐)
119118fveq2d 6647 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝐻𝑧) = (𝐻𝑐))
120119fveq2d 6647 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑠‘(𝐻𝑧)) = (𝑠‘(𝐻𝑐)))
121120fveq2d 6647 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻𝑧))) = (𝑊‘(𝑠‘(𝐻𝑐))))
122 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑐𝑤 = 𝑑) → 𝑤 = 𝑑)
123122fveq2d 6647 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝐻𝑤) = (𝐻𝑑))
124123fveq2d 6647 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑠‘(𝐻𝑤)) = (𝑠‘(𝐻𝑑)))
125124fveq2d 6647 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻𝑤))) = (𝑊‘(𝑠‘(𝐻𝑑))))
126121, 125xpeq12d 5559 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = 𝑐𝑤 = 𝑑) → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) = ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))))
127126sseq1d 3974 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑐𝑤 = 𝑑) → (((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀 ↔ ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
128117, 127imbi12d 348 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑐𝑤 = 𝑑) → ((𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) ↔ (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)))
129128spc2gv 3578 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ V ∧ 𝑑 ∈ V) → (∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)))
130129el2v 3478 . . . . . . . . . . . . . . 15 (∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
131116, 130syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
132131imp 410 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)
133132ssbrd 5082 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑢((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑))))𝑣𝑢𝑀𝑣))
134115, 133syl5bir 246 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → ((𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))) → 𝑢𝑀𝑣))
135134imp 410 . . . . . . . . . 10 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → 𝑢𝑀𝑣)
136 vex 3474 . . . . . . . . . . . . 13 𝑢 ∈ V
137 vex 3474 . . . . . . . . . . . . 13 𝑣 ∈ V
138 breq12 5044 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥𝑀𝑦𝑢𝑀𝑣))
139 simpl 486 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
140139fveq2d 6647 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐻𝑥) = (𝐻𝑢))
141140fveq2d 6647 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑆‘(𝐻𝑥)) = (𝑆‘(𝐻𝑢)))
142141fveq2d 6647 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻𝑥))) = (𝑊‘(𝑆‘(𝐻𝑢))))
143142eleq2d 2897 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ↔ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢)))))
144 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
145144fveq2d 6647 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐻𝑦) = (𝐻𝑣))
146145fveq2d 6647 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑆‘(𝐻𝑦)) = (𝑆‘(𝐻𝑣)))
147146fveq2d 6647 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻𝑦))) = (𝑊‘(𝑆‘(𝐻𝑣))))
148147eleq2d 2897 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))) ↔ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
149138, 143, 1483anbi123d 1433 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦)))) ↔ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))))
150149anbi2d 631 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) ↔ (𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))))
151150imbi1d 345 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) → 𝑎𝐾𝑏) ↔ ((𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))) → 𝑎𝐾𝑏)))
152 mclspps.8 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) → 𝑎𝐾𝑏)
153136, 137, 151, 152vtocl2 3538 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))) → 𝑎𝐾𝑏)
1541533exp2 1351 . . . . . . . . . . 11 (𝜑 → (𝑢𝑀𝑣 → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))) → 𝑎𝐾𝑏))))
155154imp4b 425 . . . . . . . . . 10 ((𝜑𝑢𝑀𝑣) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
156114, 135, 155syl2anc 587 . . . . . . . . 9 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
157156rexlimdvva 3280 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
158113, 157syl5bir 246 . . . . . . 7 ((𝜑𝑐𝑚𝑑) → ((∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
159112, 158sylbid 243 . . . . . 6 ((𝜑𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑)))) → 𝑎𝐾𝑏))
160159exp4b 434 . . . . 5 (𝜑 → (𝑐𝑚𝑑 → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) → 𝑎𝐾𝑏))))
1611603imp2 1346 . . . 4 ((𝜑 ∧ (𝑐𝑚𝑑𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))))) → 𝑎𝐾𝑏)
16216, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 61, 72, 161mclsax 32824 . . 3 (𝜑 → ((𝑆𝑠)‘𝑝) ∈ (𝐾𝐶𝐵))
16322, 162eqeltrrd 2913 . 2 (𝜑 → (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))
16433ffnd 6488 . . 3 (𝜑𝑆 Fn 𝐸)
165 elpreima 6801 . . 3 (𝑆 Fn 𝐸 → ((𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))))
166164, 165syl 17 . 2 (𝜑 → ((𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))))
16720, 163, 166mpbir2and 712 1 (𝜑 → (𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084  wal 1536   = wceq 1538  wcel 2115  wrex 3127  Vcvv 3471  cdif 3907  cun 3908  wss 3910  cotp 4548   ciun 4892   class class class wbr 5039   I cid 5432   × cxp 5526  ccnv 5527  dom cdm 5528  ran crn 5529  cima 5531  ccom 5532  Fun wfun 6322   Fn wfn 6323  wf 6324  cfv 6328  (class class class)co 7130  Fincfn 8484  mVRcmvar 32716  mAxcmax 32720  mExcmex 32722  mDVcmdv 32723  mVarscmvrs 32724  mSubstcmsub 32726  mVHcmvh 32727  mPreStcmpst 32728  mStatcmsta 32730  mFScmfs 32731  mClscmcls 32732  mPPStcmpps 32733
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-ot 4549  df-uni 4812  df-int 4850  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-om 7556  df-1st 7664  df-2nd 7665  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-oadd 8081  df-er 8264  df-map 8383  df-pm 8384  df-en 8485  df-dom 8486  df-sdom 8487  df-fin 8488  df-card 9344  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-nn 11616  df-2 11678  df-n0 11876  df-xnn0 11946  df-z 11960  df-uz 12222  df-fz 12876  df-fzo 13017  df-seq 13353  df-hash 13675  df-word 13846  df-lsw 13894  df-concat 13902  df-s1 13929  df-substr 13982  df-pfx 14012  df-struct 16464  df-ndx 16465  df-slot 16466  df-base 16468  df-sets 16469  df-ress 16470  df-plusg 16557  df-0g 16694  df-gsum 16695  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-mhm 17935  df-submnd 17936  df-frmd 17993  df-vrmd 17994  df-mrex 32741  df-mex 32742  df-mdv 32743  df-mvrs 32744  df-mrsub 32745  df-msub 32746  df-mvh 32747  df-mpst 32748  df-msr 32749  df-msta 32750  df-mfs 32751  df-mcls 32752
This theorem is referenced by:  mclspps  32839
  Copyright terms: Public domain W3C validator