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 35567
Description: The closure is closed under application of provable pre-statements. (Compare mclsax 35553.) 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 35516 . . . 4 (𝑠 ∈ ran 𝐿𝑠:𝐸𝐸)
51, 4syl 17 . . 3 (𝜑𝑠:𝐸𝐸)
6 mclspps.1 . . . . . . . 8 (𝜑𝑇 ∈ mFS)
7 eqid 2734 . . . . . . . . 9 (mAx‘𝑇) = (mAx‘𝑇)
8 eqid 2734 . . . . . . . . 9 (mStat‘𝑇) = (mStat‘𝑇)
97, 8maxsta 35538 . . . . . . . 8 (𝑇 ∈ mFS → (mAx‘𝑇) ⊆ (mStat‘𝑇))
106, 9syl 17 . . . . . . 7 (𝜑 → (mAx‘𝑇) ⊆ (mStat‘𝑇))
11 eqid 2734 . . . . . . . 8 (mPreSt‘𝑇) = (mPreSt‘𝑇)
1211, 8mstapst 35531 . . . . . . 7 (mStat‘𝑇) ⊆ (mPreSt‘𝑇)
1310, 12sstrdi 4007 . . . . . 6 (𝜑 → (mAx‘𝑇) ⊆ (mPreSt‘𝑇))
14 mclsppslem.9 . . . . . 6 (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑇))
1513, 14sseldd 3995 . . . . 5 (𝜑 → ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇))
16 mclspps.d . . . . . 6 𝐷 = (mDV‘𝑇)
1716, 3, 11elmpst 35520 . . . . 5 (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑚𝐷𝑚 = 𝑚) ∧ (𝑜𝐸𝑜 ∈ Fin) ∧ 𝑝𝐸))
1815, 17sylib 218 . . . 4 (𝜑 → ((𝑚𝐷𝑚 = 𝑚) ∧ (𝑜𝐸𝑜 ∈ Fin) ∧ 𝑝𝐸))
1918simp3d 1143 . . 3 (𝜑𝑝𝐸)
205, 19ffvelcdmd 7104 . 2 (𝜑 → (𝑠𝑝) ∈ 𝐸)
21 fvco3 7007 . . . 4 ((𝑠:𝐸𝐸𝑝𝐸) → ((𝑆𝑠)‘𝑝) = (𝑆‘(𝑠𝑝)))
225, 19, 21syl2anc 584 . . 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 35515 . . . . 5 ((𝑆 ∈ ran 𝐿𝑠 ∈ ran 𝐿) → (𝑆𝑠) ∈ ran 𝐿)
3129, 1, 30syl2anc 584 . . . 4 (𝜑 → (𝑆𝑠) ∈ ran 𝐿)
322, 3msubf 35516 . . . . . . . . 9 (𝑆 ∈ ran 𝐿𝑆:𝐸𝐸)
3329, 32syl 17 . . . . . . . 8 (𝜑𝑆:𝐸𝐸)
34 fco 6760 . . . . . . . 8 ((𝑆:𝐸𝐸𝑠:𝐸𝐸) → (𝑆𝑠):𝐸𝐸)
3533, 5, 34syl2anc 584 . . . . . . 7 (𝜑 → (𝑆𝑠):𝐸𝐸)
3635ffnd 6737 . . . . . 6 (𝜑 → (𝑆𝑠) Fn 𝐸)
3736adantr 480 . . . . 5 ((𝜑𝑐𝑜) → (𝑆𝑠) Fn 𝐸)
38 mclsppslem.11 . . . . . . . . 9 (𝜑 → (𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)))
395ffund 6740 . . . . . . . . . 10 (𝜑 → Fun 𝑠)
4017simp2bi 1145 . . . . . . . . . . . . . 14 (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mPreSt‘𝑇) → (𝑜𝐸𝑜 ∈ Fin))
4115, 40syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑜𝐸𝑜 ∈ Fin))
4241simpld 494 . . . . . . . . . . . 12 (𝜑𝑜𝐸)
4326, 3, 27mvhf 35542 . . . . . . . . . . . . 13 (𝑇 ∈ mFS → 𝐻:𝑉𝐸)
44 frn 6743 . . . . . . . . . . . . 13 (𝐻:𝑉𝐸 → ran 𝐻𝐸)
456, 43, 443syl 18 . . . . . . . . . . . 12 (𝜑 → ran 𝐻𝐸)
4642, 45unssd 4201 . . . . . . . . . . 11 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ 𝐸)
475fdmd 6746 . . . . . . . . . . 11 (𝜑 → dom 𝑠 = 𝐸)
4846, 47sseqtrrd 4036 . . . . . . . . . 10 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠)
49 funimass3 7073 . . . . . . . . . 10 ((Fun 𝑠 ∧ (𝑜 ∪ ran 𝐻) ⊆ dom 𝑠) → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))))
5039, 48, 49syl2anc 584 . . . . . . . . 9 (𝜑 → ((𝑠 “ (𝑜 ∪ ran 𝐻)) ⊆ (𝑆 “ (𝐾𝐶𝐵)) ↔ (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))))
5138, 50mpbid 232 . . . . . . . 8 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ (𝑠 “ (𝑆 “ (𝐾𝐶𝐵))))
52 cnvco 5898 . . . . . . . . . 10 (𝑆𝑠) = (𝑠𝑆)
5352imaeq1i 6076 . . . . . . . . 9 ((𝑆𝑠) “ (𝐾𝐶𝐵)) = ((𝑠𝑆) “ (𝐾𝐶𝐵))
54 imaco 6272 . . . . . . . . 9 ((𝑠𝑆) “ (𝐾𝐶𝐵)) = (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))
5553, 54eqtri 2762 . . . . . . . 8 ((𝑆𝑠) “ (𝐾𝐶𝐵)) = (𝑠 “ (𝑆 “ (𝐾𝐶𝐵)))
5651, 55sseqtrrdi 4046 . . . . . . 7 (𝜑 → (𝑜 ∪ ran 𝐻) ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
5756unssad 4202 . . . . . 6 (𝜑𝑜 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
5857sselda 3994 . . . . 5 ((𝜑𝑐𝑜) → 𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
59 elpreima 7077 . . . . . 6 ((𝑆𝑠) Fn 𝐸 → (𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)) ↔ (𝑐𝐸 ∧ ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))))
6059simplbda 499 . . . . 5 (((𝑆𝑠) Fn 𝐸𝑐 ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵))) → ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
6137, 58, 60syl2anc 584 . . . 4 ((𝜑𝑐𝑜) → ((𝑆𝑠)‘𝑐) ∈ (𝐾𝐶𝐵))
6236adantr 480 . . . . 5 ((𝜑𝑡𝑉) → (𝑆𝑠) Fn 𝐸)
6356unssbd 4203 . . . . . . 7 (𝜑 → ran 𝐻 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
6463adantr 480 . . . . . 6 ((𝜑𝑡𝑉) → ran 𝐻 ⊆ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
65 ffn 6736 . . . . . . . 8 (𝐻:𝑉𝐸𝐻 Fn 𝑉)
666, 43, 653syl 18 . . . . . . 7 (𝜑𝐻 Fn 𝑉)
67 fnfvelrn 7099 . . . . . . 7 ((𝐻 Fn 𝑉𝑡𝑉) → (𝐻𝑡) ∈ ran 𝐻)
6866, 67sylan 580 . . . . . 6 ((𝜑𝑡𝑉) → (𝐻𝑡) ∈ ran 𝐻)
6964, 68sseldd 3995 . . . . 5 ((𝜑𝑡𝑉) → (𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)))
70 elpreima 7077 . . . . . 6 ((𝑆𝑠) Fn 𝐸 → ((𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵)) ↔ ((𝐻𝑡) ∈ 𝐸 ∧ ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))))
7170simplbda 499 . . . . 5 (((𝑆𝑠) Fn 𝐸 ∧ (𝐻𝑡) ∈ ((𝑆𝑠) “ (𝐾𝐶𝐵))) → ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))
7262, 69, 71syl2anc 584 . . . 4 ((𝜑𝑡𝑉) → ((𝑆𝑠)‘(𝐻𝑡)) ∈ (𝐾𝐶𝐵))
735adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → 𝑠:𝐸𝐸)
746, 43syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝑉𝐸)
7574adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝐻:𝑉𝐸)
7618simp1d 1141 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑚𝐷𝑚 = 𝑚))
7776simpld 494 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑚𝐷)
7826, 16mdvval 35488 . . . . . . . . . . . . . . . . . . . 20 𝐷 = ((𝑉 × 𝑉) ∖ I )
79 difss 4145 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 × 𝑉) ∖ I ) ⊆ (𝑉 × 𝑉)
8078, 79eqsstri 4029 . . . . . . . . . . . . . . . . . . 19 𝐷 ⊆ (𝑉 × 𝑉)
8177, 80sstrdi 4007 . . . . . . . . . . . . . . . . . 18 (𝜑𝑚 ⊆ (𝑉 × 𝑉))
8281ssbrd 5190 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑐𝑚𝑑𝑐(𝑉 × 𝑉)𝑑))
8382imp 406 . . . . . . . . . . . . . . . 16 ((𝜑𝑐𝑚𝑑) → 𝑐(𝑉 × 𝑉)𝑑)
84 brxp 5737 . . . . . . . . . . . . . . . 16 (𝑐(𝑉 × 𝑉)𝑑 ↔ (𝑐𝑉𝑑𝑉))
8583, 84sylib 218 . . . . . . . . . . . . . . 15 ((𝜑𝑐𝑚𝑑) → (𝑐𝑉𝑑𝑉))
8685simpld 494 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝑐𝑉)
8775, 86ffvelcdmd 7104 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → (𝐻𝑐) ∈ 𝐸)
88 fvco3 7007 . . . . . . . . . . . . 13 ((𝑠:𝐸𝐸 ∧ (𝐻𝑐) ∈ 𝐸) → ((𝑆𝑠)‘(𝐻𝑐)) = (𝑆‘(𝑠‘(𝐻𝑐))))
8973, 87, 88syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → ((𝑆𝑠)‘(𝐻𝑐)) = (𝑆‘(𝑠‘(𝐻𝑐))))
9089fveq2d 6910 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) = (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))))
916adantr 480 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → 𝑇 ∈ mFS)
9229adantr 480 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → 𝑆 ∈ ran 𝐿)
9373, 87ffvelcdmd 7104 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑠‘(𝐻𝑐)) ∈ 𝐸)
942, 3, 28, 27msubvrs 35544 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻𝑐)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9591, 92, 93, 94syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑐)))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9690, 95eqtrd 2774 . . . . . . . . . 10 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) = 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))))
9796eleq2d 2824 . . . . . . . . 9 ((𝜑𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ↔ 𝑎 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢)))))
98 eliun 4999 . . . . . . . . 9 (𝑎 𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))(𝑊‘(𝑆‘(𝐻𝑢))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))))
9997, 98bitrdi 287 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ↔ ∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢)))))
10085simprd 495 . . . . . . . . . . . . . 14 ((𝜑𝑐𝑚𝑑) → 𝑑𝑉)
10175, 100ffvelcdmd 7104 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → (𝐻𝑑) ∈ 𝐸)
102 fvco3 7007 . . . . . . . . . . . . 13 ((𝑠:𝐸𝐸 ∧ (𝐻𝑑) ∈ 𝐸) → ((𝑆𝑠)‘(𝐻𝑑)) = (𝑆‘(𝑠‘(𝐻𝑑))))
10373, 101, 102syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → ((𝑆𝑠)‘(𝐻𝑑)) = (𝑆‘(𝑠‘(𝐻𝑑))))
104103fveq2d 6910 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) = (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))))
10573, 101ffvelcdmd 7104 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑠‘(𝐻𝑑)) ∈ 𝐸)
1062, 3, 28, 27msubvrs 35544 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (𝑠‘(𝐻𝑑)) ∈ 𝐸) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
10791, 92, 105, 106syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → (𝑊‘(𝑆‘(𝑠‘(𝐻𝑑)))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
108104, 107eqtrd 2774 . . . . . . . . . 10 ((𝜑𝑐𝑚𝑑) → (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) = 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))))
109108eleq2d 2824 . . . . . . . . 9 ((𝜑𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) ↔ 𝑏 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣)))))
110 eliun 4999 . . . . . . . . 9 (𝑏 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑊‘(𝑆‘(𝐻𝑣))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))
111109, 110bitrdi 287 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) ↔ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
11299, 111anbi12d 632 . . . . . . 7 ((𝜑𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))))
113 reeanv 3226 . . . . . . . 8 (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) ↔ (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
114 simpll 767 . . . . . . . . . 10 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → 𝜑)
115 brxp 5737 . . . . . . . . . . . 12 (𝑢((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑))))𝑣 ↔ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))))
116 mclsppslem.12 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀))
117 breq12 5152 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑧𝑚𝑤𝑐𝑚𝑑))
118 simpl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑐𝑤 = 𝑑) → 𝑧 = 𝑐)
119118fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝐻𝑧) = (𝐻𝑐))
120119fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑠‘(𝐻𝑧)) = (𝑠‘(𝐻𝑐)))
121120fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻𝑧))) = (𝑊‘(𝑠‘(𝐻𝑐))))
122 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑐𝑤 = 𝑑) → 𝑤 = 𝑑)
123122fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝐻𝑤) = (𝐻𝑑))
124123fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑠‘(𝐻𝑤)) = (𝑠‘(𝐻𝑑)))
125124fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐𝑤 = 𝑑) → (𝑊‘(𝑠‘(𝐻𝑤))) = (𝑊‘(𝑠‘(𝐻𝑑))))
126121, 125xpeq12d 5719 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = 𝑐𝑤 = 𝑑) → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) = ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))))
127126sseq1d 4026 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑐𝑤 = 𝑑) → (((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀 ↔ ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
128117, 127imbi12d 344 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑐𝑤 = 𝑑) → ((𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) ↔ (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)))
129128spc2gv 3599 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ V ∧ 𝑑 ∈ V) → (∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)))
130129el2v 3484 . . . . . . . . . . . . . . 15 (∀𝑧𝑤(𝑧𝑚𝑤 → ((𝑊‘(𝑠‘(𝐻𝑧))) × (𝑊‘(𝑠‘(𝐻𝑤)))) ⊆ 𝑀) → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
131116, 130syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑐𝑚𝑑 → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀))
132131imp 406 . . . . . . . . . . . . 13 ((𝜑𝑐𝑚𝑑) → ((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑)))) ⊆ 𝑀)
133132ssbrd 5190 . . . . . . . . . . . 12 ((𝜑𝑐𝑚𝑑) → (𝑢((𝑊‘(𝑠‘(𝐻𝑐))) × (𝑊‘(𝑠‘(𝐻𝑑))))𝑣𝑢𝑀𝑣))
134115, 133biimtrrid 243 . . . . . . . . . . 11 ((𝜑𝑐𝑚𝑑) → ((𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))) → 𝑢𝑀𝑣))
135134imp 406 . . . . . . . . . 10 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → 𝑢𝑀𝑣)
136 vex 3481 . . . . . . . . . . . . 13 𝑢 ∈ V
137 vex 3481 . . . . . . . . . . . . 13 𝑣 ∈ V
138 breq12 5152 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑥𝑀𝑦𝑢𝑀𝑣))
139 simpl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑥 = 𝑢)
140139fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐻𝑥) = (𝐻𝑢))
141140fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑆‘(𝐻𝑥)) = (𝑆‘(𝐻𝑢)))
142141fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻𝑥))) = (𝑊‘(𝑆‘(𝐻𝑢))))
143142eleq2d 2824 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ↔ 𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢)))))
144 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 = 𝑢𝑦 = 𝑣) → 𝑦 = 𝑣)
145144fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝐻𝑦) = (𝐻𝑣))
146145fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑆‘(𝐻𝑦)) = (𝑆‘(𝐻𝑣)))
147146fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑊‘(𝑆‘(𝐻𝑦))) = (𝑊‘(𝑆‘(𝐻𝑣))))
148147eleq2d 2824 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))) ↔ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))
149138, 143, 1483anbi123d 1435 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦)))) ↔ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))))
150149anbi2d 630 . . . . . . . . . . . . . 14 ((𝑥 = 𝑢𝑦 = 𝑣) → ((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) ↔ (𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))))))
151150imbi1d 341 . . . . . . . . . . . . 13 ((𝑥 = 𝑢𝑦 = 𝑣) → (((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) → 𝑎𝐾𝑏) ↔ ((𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))) → 𝑎𝐾𝑏)))
152 mclspps.8 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑀𝑦𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑥))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑦))))) → 𝑎𝐾𝑏)
153136, 137, 151, 152vtocl2 3565 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢𝑀𝑣𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))))) → 𝑎𝐾𝑏)
1541533exp2 1353 . . . . . . . . . . 11 (𝜑 → (𝑢𝑀𝑣 → (𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) → (𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣))) → 𝑎𝐾𝑏))))
155154imp4b 421 . . . . . . . . . 10 ((𝜑𝑢𝑀𝑣) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
156114, 135, 155syl2anc 584 . . . . . . . . 9 (((𝜑𝑐𝑚𝑑) ∧ (𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐))) ∧ 𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑))))) → ((𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
157156rexlimdvva 3210 . . . . . . . 8 ((𝜑𝑐𝑚𝑑) → (∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))(𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ 𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
158113, 157biimtrrid 243 . . . . . . 7 ((𝜑𝑐𝑚𝑑) → ((∃𝑢 ∈ (𝑊‘(𝑠‘(𝐻𝑐)))𝑎 ∈ (𝑊‘(𝑆‘(𝐻𝑢))) ∧ ∃𝑣 ∈ (𝑊‘(𝑠‘(𝐻𝑑)))𝑏 ∈ (𝑊‘(𝑆‘(𝐻𝑣)))) → 𝑎𝐾𝑏))
159112, 158sylbid 240 . . . . . 6 ((𝜑𝑐𝑚𝑑) → ((𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑)))) → 𝑎𝐾𝑏))
160159exp4b 430 . . . . 5 (𝜑 → (𝑐𝑚𝑑 → (𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) → (𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))) → 𝑎𝐾𝑏))))
1611603imp2 1348 . . . 4 ((𝜑 ∧ (𝑐𝑚𝑑𝑎 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑐))) ∧ 𝑏 ∈ (𝑊‘((𝑆𝑠)‘(𝐻𝑑))))) → 𝑎𝐾𝑏)
16216, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 61, 72, 161mclsax 35553 . . 3 (𝜑 → ((𝑆𝑠)‘𝑝) ∈ (𝐾𝐶𝐵))
16322, 162eqeltrrd 2839 . 2 (𝜑 → (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))
16433ffnd 6737 . . 3 (𝜑𝑆 Fn 𝐸)
165 elpreima 7077 . . 3 (𝑆 Fn 𝐸 → ((𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))))
166164, 165syl 17 . 2 (𝜑 → ((𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)) ↔ ((𝑠𝑝) ∈ 𝐸 ∧ (𝑆‘(𝑠𝑝)) ∈ (𝐾𝐶𝐵))))
16720, 163, 166mpbir2and 713 1 (𝜑 → (𝑠𝑝) ∈ (𝑆 “ (𝐾𝐶𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086  wal 1534   = wceq 1536  wcel 2105  wrex 3067  Vcvv 3477  cdif 3959  cun 3960  wss 3962  cotp 4638   ciun 4995   class class class wbr 5147   I cid 5581   × cxp 5686  ccnv 5687  dom cdm 5688  ran crn 5689  cima 5691  ccom 5692  Fun wfun 6556   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  Fincfn 8983  mVRcmvar 35445  mAxcmax 35449  mExcmex 35451  mDVcmdv 35452  mVarscmvrs 35453  mSubstcmsub 35455  mVHcmvh 35456  mPreStcmpst 35457  mStatcmsta 35459  mFScmfs 35460  mClscmcls 35461  mPPStcmpps 35462
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-ot 4639  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-n0 12524  df-xnn0 12597  df-z 12611  df-uz 12876  df-fz 13544  df-fzo 13691  df-seq 14039  df-hash 14366  df-word 14549  df-lsw 14597  df-concat 14605  df-s1 14630  df-substr 14675  df-pfx 14705  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-0g 17487  df-gsum 17488  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-frmd 18874  df-vrmd 18875  df-mrex 35470  df-mex 35471  df-mdv 35472  df-mvrs 35473  df-mrsub 35474  df-msub 35475  df-mvh 35476  df-mpst 35477  df-msr 35478  df-msta 35479  df-mfs 35480  df-mcls 35481
This theorem is referenced by:  mclspps  35568
  Copyright terms: Public domain W3C validator