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 34872
Description: The closure is closed under application of provable pre-statements. (Compare mclsax 34858.) 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 34821 . . . 4 (𝑠 ∈ ran 𝐿 β†’ 𝑠:𝐸⟢𝐸)
51, 4syl 17 . . 3 (πœ‘ β†’ 𝑠:𝐸⟢𝐸)
6 mclspps.1 . . . . . . . 8 (πœ‘ β†’ 𝑇 ∈ mFS)
7 eqid 2730 . . . . . . . . 9 (mAxβ€˜π‘‡) = (mAxβ€˜π‘‡)
8 eqid 2730 . . . . . . . . 9 (mStatβ€˜π‘‡) = (mStatβ€˜π‘‡)
97, 8maxsta 34843 . . . . . . . 8 (𝑇 ∈ mFS β†’ (mAxβ€˜π‘‡) βŠ† (mStatβ€˜π‘‡))
106, 9syl 17 . . . . . . 7 (πœ‘ β†’ (mAxβ€˜π‘‡) βŠ† (mStatβ€˜π‘‡))
11 eqid 2730 . . . . . . . 8 (mPreStβ€˜π‘‡) = (mPreStβ€˜π‘‡)
1211, 8mstapst 34836 . . . . . . 7 (mStatβ€˜π‘‡) βŠ† (mPreStβ€˜π‘‡)
1310, 12sstrdi 3993 . . . . . 6 (πœ‘ β†’ (mAxβ€˜π‘‡) βŠ† (mPreStβ€˜π‘‡))
14 mclsppslem.9 . . . . . 6 (πœ‘ β†’ βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‡))
1513, 14sseldd 3982 . . . . 5 (πœ‘ β†’ βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mPreStβ€˜π‘‡))
16 mclspps.d . . . . . 6 𝐷 = (mDVβ€˜π‘‡)
1716, 3, 11elmpst 34825 . . . . 5 (βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mPreStβ€˜π‘‡) ↔ ((π‘š βŠ† 𝐷 ∧ β—‘π‘š = π‘š) ∧ (π‘œ βŠ† 𝐸 ∧ π‘œ ∈ Fin) ∧ 𝑝 ∈ 𝐸))
1815, 17sylib 217 . . . 4 (πœ‘ β†’ ((π‘š βŠ† 𝐷 ∧ β—‘π‘š = π‘š) ∧ (π‘œ βŠ† 𝐸 ∧ π‘œ ∈ Fin) ∧ 𝑝 ∈ 𝐸))
1918simp3d 1142 . . 3 (πœ‘ β†’ 𝑝 ∈ 𝐸)
205, 19ffvelcdmd 7086 . 2 (πœ‘ β†’ (π‘ β€˜π‘) ∈ 𝐸)
21 fvco3 6989 . . . 4 ((𝑠:𝐸⟢𝐸 ∧ 𝑝 ∈ 𝐸) β†’ ((𝑆 ∘ 𝑠)β€˜π‘) = (π‘†β€˜(π‘ β€˜π‘)))
225, 19, 21syl2anc 582 . . 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 34820 . . . . 5 ((𝑆 ∈ ran 𝐿 ∧ 𝑠 ∈ ran 𝐿) β†’ (𝑆 ∘ 𝑠) ∈ ran 𝐿)
3129, 1, 30syl2anc 582 . . . 4 (πœ‘ β†’ (𝑆 ∘ 𝑠) ∈ ran 𝐿)
322, 3msubf 34821 . . . . . . . . 9 (𝑆 ∈ ran 𝐿 β†’ 𝑆:𝐸⟢𝐸)
3329, 32syl 17 . . . . . . . 8 (πœ‘ β†’ 𝑆:𝐸⟢𝐸)
34 fco 6740 . . . . . . . 8 ((𝑆:𝐸⟢𝐸 ∧ 𝑠:𝐸⟢𝐸) β†’ (𝑆 ∘ 𝑠):𝐸⟢𝐸)
3533, 5, 34syl2anc 582 . . . . . . 7 (πœ‘ β†’ (𝑆 ∘ 𝑠):𝐸⟢𝐸)
3635ffnd 6717 . . . . . 6 (πœ‘ β†’ (𝑆 ∘ 𝑠) Fn 𝐸)
3736adantr 479 . . . . 5 ((πœ‘ ∧ 𝑐 ∈ π‘œ) β†’ (𝑆 ∘ 𝑠) Fn 𝐸)
38 mclsppslem.11 . . . . . . . . 9 (πœ‘ β†’ (𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† (◑𝑆 β€œ (𝐾𝐢𝐡)))
395ffund 6720 . . . . . . . . . 10 (πœ‘ β†’ Fun 𝑠)
4017simp2bi 1144 . . . . . . . . . . . . . 14 (βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mPreStβ€˜π‘‡) β†’ (π‘œ βŠ† 𝐸 ∧ π‘œ ∈ Fin))
4115, 40syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘œ βŠ† 𝐸 ∧ π‘œ ∈ Fin))
4241simpld 493 . . . . . . . . . . . 12 (πœ‘ β†’ π‘œ βŠ† 𝐸)
4326, 3, 27mvhf 34847 . . . . . . . . . . . . 13 (𝑇 ∈ mFS β†’ 𝐻:π‘‰βŸΆπΈ)
44 frn 6723 . . . . . . . . . . . . 13 (𝐻:π‘‰βŸΆπΈ β†’ ran 𝐻 βŠ† 𝐸)
456, 43, 443syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ ran 𝐻 βŠ† 𝐸)
4642, 45unssd 4185 . . . . . . . . . . 11 (πœ‘ β†’ (π‘œ βˆͺ ran 𝐻) βŠ† 𝐸)
475fdmd 6727 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝑠 = 𝐸)
4846, 47sseqtrrd 4022 . . . . . . . . . 10 (πœ‘ β†’ (π‘œ βˆͺ ran 𝐻) βŠ† dom 𝑠)
49 funimass3 7054 . . . . . . . . . 10 ((Fun 𝑠 ∧ (π‘œ βˆͺ ran 𝐻) βŠ† dom 𝑠) β†’ ((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† (◑𝑆 β€œ (𝐾𝐢𝐡)) ↔ (π‘œ βˆͺ ran 𝐻) βŠ† (◑𝑠 β€œ (◑𝑆 β€œ (𝐾𝐢𝐡)))))
5039, 48, 49syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ ((𝑠 β€œ (π‘œ βˆͺ ran 𝐻)) βŠ† (◑𝑆 β€œ (𝐾𝐢𝐡)) ↔ (π‘œ βˆͺ ran 𝐻) βŠ† (◑𝑠 β€œ (◑𝑆 β€œ (𝐾𝐢𝐡)))))
5138, 50mpbid 231 . . . . . . . 8 (πœ‘ β†’ (π‘œ βˆͺ ran 𝐻) βŠ† (◑𝑠 β€œ (◑𝑆 β€œ (𝐾𝐢𝐡))))
52 cnvco 5884 . . . . . . . . . 10 β—‘(𝑆 ∘ 𝑠) = (◑𝑠 ∘ ◑𝑆)
5352imaeq1i 6055 . . . . . . . . 9 (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)) = ((◑𝑠 ∘ ◑𝑆) β€œ (𝐾𝐢𝐡))
54 imaco 6249 . . . . . . . . 9 ((◑𝑠 ∘ ◑𝑆) β€œ (𝐾𝐢𝐡)) = (◑𝑠 β€œ (◑𝑆 β€œ (𝐾𝐢𝐡)))
5553, 54eqtri 2758 . . . . . . . 8 (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)) = (◑𝑠 β€œ (◑𝑆 β€œ (𝐾𝐢𝐡)))
5651, 55sseqtrrdi 4032 . . . . . . 7 (πœ‘ β†’ (π‘œ βˆͺ ran 𝐻) βŠ† (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)))
5756unssad 4186 . . . . . 6 (πœ‘ β†’ π‘œ βŠ† (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)))
5857sselda 3981 . . . . 5 ((πœ‘ ∧ 𝑐 ∈ π‘œ) β†’ 𝑐 ∈ (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)))
59 elpreima 7058 . . . . . 6 ((𝑆 ∘ 𝑠) Fn 𝐸 β†’ (𝑐 ∈ (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)) ↔ (𝑐 ∈ 𝐸 ∧ ((𝑆 ∘ 𝑠)β€˜π‘) ∈ (𝐾𝐢𝐡))))
6059simplbda 498 . . . . 5 (((𝑆 ∘ 𝑠) Fn 𝐸 ∧ 𝑐 ∈ (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡))) β†’ ((𝑆 ∘ 𝑠)β€˜π‘) ∈ (𝐾𝐢𝐡))
6137, 58, 60syl2anc 582 . . . 4 ((πœ‘ ∧ 𝑐 ∈ π‘œ) β†’ ((𝑆 ∘ 𝑠)β€˜π‘) ∈ (𝐾𝐢𝐡))
6236adantr 479 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝑉) β†’ (𝑆 ∘ 𝑠) Fn 𝐸)
6356unssbd 4187 . . . . . . 7 (πœ‘ β†’ ran 𝐻 βŠ† (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)))
6463adantr 479 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝑉) β†’ ran 𝐻 βŠ† (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)))
65 ffn 6716 . . . . . . . 8 (𝐻:π‘‰βŸΆπΈ β†’ 𝐻 Fn 𝑉)
666, 43, 653syl 18 . . . . . . 7 (πœ‘ β†’ 𝐻 Fn 𝑉)
67 fnfvelrn 7081 . . . . . . 7 ((𝐻 Fn 𝑉 ∧ 𝑑 ∈ 𝑉) β†’ (π»β€˜π‘‘) ∈ ran 𝐻)
6866, 67sylan 578 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝑉) β†’ (π»β€˜π‘‘) ∈ ran 𝐻)
6964, 68sseldd 3982 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝑉) β†’ (π»β€˜π‘‘) ∈ (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)))
70 elpreima 7058 . . . . . 6 ((𝑆 ∘ 𝑠) Fn 𝐸 β†’ ((π»β€˜π‘‘) ∈ (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡)) ↔ ((π»β€˜π‘‘) ∈ 𝐸 ∧ ((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘)) ∈ (𝐾𝐢𝐡))))
7170simplbda 498 . . . . 5 (((𝑆 ∘ 𝑠) Fn 𝐸 ∧ (π»β€˜π‘‘) ∈ (β—‘(𝑆 ∘ 𝑠) β€œ (𝐾𝐢𝐡))) β†’ ((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘)) ∈ (𝐾𝐢𝐡))
7262, 69, 71syl2anc 582 . . . 4 ((πœ‘ ∧ 𝑑 ∈ 𝑉) β†’ ((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘)) ∈ (𝐾𝐢𝐡))
735adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ 𝑠:𝐸⟢𝐸)
746, 43syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐻:π‘‰βŸΆπΈ)
7574adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ 𝐻:π‘‰βŸΆπΈ)
7618simp1d 1140 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘š βŠ† 𝐷 ∧ β—‘π‘š = π‘š))
7776simpld 493 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ π‘š βŠ† 𝐷)
7826, 16mdvval 34793 . . . . . . . . . . . . . . . . . . . 20 𝐷 = ((𝑉 Γ— 𝑉) βˆ– I )
79 difss 4130 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 Γ— 𝑉) βˆ– I ) βŠ† (𝑉 Γ— 𝑉)
8078, 79eqsstri 4015 . . . . . . . . . . . . . . . . . . 19 𝐷 βŠ† (𝑉 Γ— 𝑉)
8177, 80sstrdi 3993 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘š βŠ† (𝑉 Γ— 𝑉))
8281ssbrd 5190 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π‘π‘šπ‘‘ β†’ 𝑐(𝑉 Γ— 𝑉)𝑑))
8382imp 405 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ 𝑐(𝑉 Γ— 𝑉)𝑑)
84 brxp 5724 . . . . . . . . . . . . . . . 16 (𝑐(𝑉 Γ— 𝑉)𝑑 ↔ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))
8583, 84sylib 217 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))
8685simpld 493 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ 𝑐 ∈ 𝑉)
8775, 86ffvelcdmd 7086 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π»β€˜π‘) ∈ 𝐸)
88 fvco3 6989 . . . . . . . . . . . . 13 ((𝑠:𝐸⟢𝐸 ∧ (π»β€˜π‘) ∈ 𝐸) β†’ ((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘)) = (π‘†β€˜(π‘ β€˜(π»β€˜π‘))))
8973, 87, 88syl2anc 582 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ ((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘)) = (π‘†β€˜(π‘ β€˜(π»β€˜π‘))))
9089fveq2d 6894 . . . . . . . . . . 11 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘))) = (π‘Šβ€˜(π‘†β€˜(π‘ β€˜(π»β€˜π‘)))))
916adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ 𝑇 ∈ mFS)
9229adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ 𝑆 ∈ ran 𝐿)
9373, 87ffvelcdmd 7086 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘ β€˜(π»β€˜π‘)) ∈ 𝐸)
942, 3, 28, 27msubvrs 34849 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (π‘ β€˜(π»β€˜π‘)) ∈ 𝐸) β†’ (π‘Šβ€˜(π‘†β€˜(π‘ β€˜(π»β€˜π‘)))) = βˆͺ 𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))))
9591, 92, 93, 94syl3anc 1369 . . . . . . . . . . 11 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘Šβ€˜(π‘†β€˜(π‘ β€˜(π»β€˜π‘)))) = βˆͺ 𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))))
9690, 95eqtrd 2770 . . . . . . . . . 10 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘))) = βˆͺ 𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))))
9796eleq2d 2817 . . . . . . . . 9 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘Ž ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘))) ↔ π‘Ž ∈ βˆͺ 𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’)))))
98 eliun 5000 . . . . . . . . 9 (π‘Ž ∈ βˆͺ 𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ↔ βˆƒπ‘’ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))))
9997, 98bitrdi 286 . . . . . . . 8 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘Ž ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘))) ↔ βˆƒπ‘’ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’)))))
10085simprd 494 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ 𝑑 ∈ 𝑉)
10175, 100ffvelcdmd 7086 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π»β€˜π‘‘) ∈ 𝐸)
102 fvco3 6989 . . . . . . . . . . . . 13 ((𝑠:𝐸⟢𝐸 ∧ (π»β€˜π‘‘) ∈ 𝐸) β†’ ((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘)) = (π‘†β€˜(π‘ β€˜(π»β€˜π‘‘))))
10373, 101, 102syl2anc 582 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ ((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘)) = (π‘†β€˜(π‘ β€˜(π»β€˜π‘‘))))
104103fveq2d 6894 . . . . . . . . . . 11 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘))) = (π‘Šβ€˜(π‘†β€˜(π‘ β€˜(π»β€˜π‘‘)))))
10573, 101ffvelcdmd 7086 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘ β€˜(π»β€˜π‘‘)) ∈ 𝐸)
1062, 3, 28, 27msubvrs 34849 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑆 ∈ ran 𝐿 ∧ (π‘ β€˜(π»β€˜π‘‘)) ∈ 𝐸) β†’ (π‘Šβ€˜(π‘†β€˜(π‘ β€˜(π»β€˜π‘‘)))) = βˆͺ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))))
10791, 92, 105, 106syl3anc 1369 . . . . . . . . . . 11 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘Šβ€˜(π‘†β€˜(π‘ β€˜(π»β€˜π‘‘)))) = βˆͺ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))))
108104, 107eqtrd 2770 . . . . . . . . . 10 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘))) = βˆͺ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))))
109108eleq2d 2817 . . . . . . . . 9 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (𝑏 ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘))) ↔ 𝑏 ∈ βˆͺ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))))
110 eliun 5000 . . . . . . . . 9 (𝑏 ∈ βˆͺ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))(π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))) ↔ βˆƒπ‘£ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))))
111109, 110bitrdi 286 . . . . . . . 8 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (𝑏 ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘))) ↔ βˆƒπ‘£ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))))
11299, 111anbi12d 629 . . . . . . 7 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ ((π‘Ž ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘))) ∧ 𝑏 ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘)))) ↔ (βˆƒπ‘’ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ βˆƒπ‘£ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))))))
113 reeanv 3224 . . . . . . . 8 (βˆƒπ‘’ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))βˆƒπ‘£ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))(π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))) ↔ (βˆƒπ‘’ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ βˆƒπ‘£ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))))
114 simpll 763 . . . . . . . . . 10 (((πœ‘ ∧ π‘π‘šπ‘‘) ∧ (𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) ∧ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘))))) β†’ πœ‘)
115 brxp 5724 . . . . . . . . . . . 12 (𝑒((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘))))𝑣 ↔ (𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) ∧ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))))
116 mclsppslem.12 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘§βˆ€π‘€(π‘§π‘šπ‘€ β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘§))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘€)))) βŠ† 𝑀))
117 breq12 5152 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ (π‘§π‘šπ‘€ ↔ π‘π‘šπ‘‘))
118 simpl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ 𝑧 = 𝑐)
119118fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ (π»β€˜π‘§) = (π»β€˜π‘))
120119fveq2d 6894 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ (π‘ β€˜(π»β€˜π‘§)) = (π‘ β€˜(π»β€˜π‘)))
121120fveq2d 6894 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘§))) = (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))))
122 simpr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ 𝑀 = 𝑑)
123122fveq2d 6894 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ (π»β€˜π‘€) = (π»β€˜π‘‘))
124123fveq2d 6894 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ (π‘ β€˜(π»β€˜π‘€)) = (π‘ β€˜(π»β€˜π‘‘)))
125124fveq2d 6894 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘€))) = (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘))))
126121, 125xpeq12d 5706 . . . . . . . . . . . . . . . . . . 19 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘§))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘€)))) = ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))))
127126sseq1d 4012 . . . . . . . . . . . . . . . . . 18 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ (((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘§))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘€)))) βŠ† 𝑀 ↔ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))) βŠ† 𝑀))
128117, 127imbi12d 343 . . . . . . . . . . . . . . . . 17 ((𝑧 = 𝑐 ∧ 𝑀 = 𝑑) β†’ ((π‘§π‘šπ‘€ β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘§))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘€)))) βŠ† 𝑀) ↔ (π‘π‘šπ‘‘ β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))) βŠ† 𝑀)))
129128spc2gv 3589 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ V ∧ 𝑑 ∈ V) β†’ (βˆ€π‘§βˆ€π‘€(π‘§π‘šπ‘€ β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘§))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘€)))) βŠ† 𝑀) β†’ (π‘π‘šπ‘‘ β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))) βŠ† 𝑀)))
130129el2v 3480 . . . . . . . . . . . . . . 15 (βˆ€π‘§βˆ€π‘€(π‘§π‘šπ‘€ β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘§))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘€)))) βŠ† 𝑀) β†’ (π‘π‘šπ‘‘ β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))) βŠ† 𝑀))
131116, 130syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘π‘šπ‘‘ β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))) βŠ† 𝑀))
132131imp 405 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ ((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))) βŠ† 𝑀)
133132ssbrd 5190 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (𝑒((π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) Γ— (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘))))𝑣 β†’ 𝑒𝑀𝑣))
134115, 133biimtrrid 242 . . . . . . . . . . 11 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ ((𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) ∧ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))) β†’ 𝑒𝑀𝑣))
135134imp 405 . . . . . . . . . 10 (((πœ‘ ∧ π‘π‘šπ‘‘) ∧ (𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) ∧ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘))))) β†’ 𝑒𝑀𝑣)
136 vex 3476 . . . . . . . . . . . . 13 𝑒 ∈ V
137 vex 3476 . . . . . . . . . . . . 13 𝑣 ∈ V
138 breq12 5152 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π‘₯𝑀𝑦 ↔ 𝑒𝑀𝑣))
139 simpl 481 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ π‘₯ = 𝑒)
140139fveq2d 6894 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π»β€˜π‘₯) = (π»β€˜π‘’))
141140fveq2d 6894 . . . . . . . . . . . . . . . . . 18 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π‘†β€˜(π»β€˜π‘₯)) = (π‘†β€˜(π»β€˜π‘’)))
142141fveq2d 6894 . . . . . . . . . . . . . . . . 17 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘₯))) = (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))))
143142eleq2d 2817 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘₯))) ↔ π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’)))))
144 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ 𝑦 = 𝑣)
145144fveq2d 6894 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π»β€˜π‘¦) = (π»β€˜π‘£))
146145fveq2d 6894 . . . . . . . . . . . . . . . . . 18 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π‘†β€˜(π»β€˜π‘¦)) = (π‘†β€˜(π»β€˜π‘£)))
147146fveq2d 6894 . . . . . . . . . . . . . . . . 17 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘¦))) = (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))))
148147eleq2d 2817 . . . . . . . . . . . . . . . 16 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘¦))) ↔ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))))
149138, 143, 1483anbi123d 1434 . . . . . . . . . . . . . . 15 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ ((π‘₯𝑀𝑦 ∧ π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘₯))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘¦)))) ↔ (𝑒𝑀𝑣 ∧ π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))))))
150149anbi2d 627 . . . . . . . . . . . . . 14 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ ((πœ‘ ∧ (π‘₯𝑀𝑦 ∧ π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘₯))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘¦))))) ↔ (πœ‘ ∧ (𝑒𝑀𝑣 ∧ π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))))))
151150imbi1d 340 . . . . . . . . . . . . 13 ((π‘₯ = 𝑒 ∧ 𝑦 = 𝑣) β†’ (((πœ‘ ∧ (π‘₯𝑀𝑦 ∧ π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘₯))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘¦))))) β†’ π‘ŽπΎπ‘) ↔ ((πœ‘ ∧ (𝑒𝑀𝑣 ∧ π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))))) β†’ π‘ŽπΎπ‘)))
152 mclspps.8 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘₯𝑀𝑦 ∧ π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘₯))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘¦))))) β†’ π‘ŽπΎπ‘)
153136, 137, 151, 152vtocl2 3553 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑒𝑀𝑣 ∧ π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))))) β†’ π‘ŽπΎπ‘)
1541533exp2 1352 . . . . . . . . . . 11 (πœ‘ β†’ (𝑒𝑀𝑣 β†’ (π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) β†’ (𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£))) β†’ π‘ŽπΎπ‘))))
155154imp4b 420 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒𝑀𝑣) β†’ ((π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))) β†’ π‘ŽπΎπ‘))
156114, 135, 155syl2anc 582 . . . . . . . . 9 (((πœ‘ ∧ π‘π‘šπ‘‘) ∧ (𝑒 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘))) ∧ 𝑣 ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘))))) β†’ ((π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))) β†’ π‘ŽπΎπ‘))
157156rexlimdvva 3209 . . . . . . . 8 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ (βˆƒπ‘’ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))βˆƒπ‘£ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))(π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ 𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))) β†’ π‘ŽπΎπ‘))
158113, 157biimtrrid 242 . . . . . . 7 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ ((βˆƒπ‘’ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘)))π‘Ž ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘’))) ∧ βˆƒπ‘£ ∈ (π‘Šβ€˜(π‘ β€˜(π»β€˜π‘‘)))𝑏 ∈ (π‘Šβ€˜(π‘†β€˜(π»β€˜π‘£)))) β†’ π‘ŽπΎπ‘))
159112, 158sylbid 239 . . . . . 6 ((πœ‘ ∧ π‘π‘šπ‘‘) β†’ ((π‘Ž ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘))) ∧ 𝑏 ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘)))) β†’ π‘ŽπΎπ‘))
160159exp4b 429 . . . . 5 (πœ‘ β†’ (π‘π‘šπ‘‘ β†’ (π‘Ž ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘))) β†’ (𝑏 ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘))) β†’ π‘ŽπΎπ‘))))
1611603imp2 1347 . . . 4 ((πœ‘ ∧ (π‘π‘šπ‘‘ ∧ π‘Ž ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘))) ∧ 𝑏 ∈ (π‘Šβ€˜((𝑆 ∘ 𝑠)β€˜(π»β€˜π‘‘))))) β†’ π‘ŽπΎπ‘)
16216, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 61, 72, 161mclsax 34858 . . 3 (πœ‘ β†’ ((𝑆 ∘ 𝑠)β€˜π‘) ∈ (𝐾𝐢𝐡))
16322, 162eqeltrrd 2832 . 2 (πœ‘ β†’ (π‘†β€˜(π‘ β€˜π‘)) ∈ (𝐾𝐢𝐡))
16433ffnd 6717 . . 3 (πœ‘ β†’ 𝑆 Fn 𝐸)
165 elpreima 7058 . . 3 (𝑆 Fn 𝐸 β†’ ((π‘ β€˜π‘) ∈ (◑𝑆 β€œ (𝐾𝐢𝐡)) ↔ ((π‘ β€˜π‘) ∈ 𝐸 ∧ (π‘†β€˜(π‘ β€˜π‘)) ∈ (𝐾𝐢𝐡))))
166164, 165syl 17 . 2 (πœ‘ β†’ ((π‘ β€˜π‘) ∈ (◑𝑆 β€œ (𝐾𝐢𝐡)) ↔ ((π‘ β€˜π‘) ∈ 𝐸 ∧ (π‘†β€˜(π‘ β€˜π‘)) ∈ (𝐾𝐢𝐡))))
16720, 163, 166mpbir2and 709 1 (πœ‘ β†’ (π‘ β€˜π‘) ∈ (◑𝑆 β€œ (𝐾𝐢𝐡)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085  βˆ€wal 1537   = wceq 1539   ∈ wcel 2104  βˆƒwrex 3068  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   βŠ† wss 3947  βŸ¨cotp 4635  βˆͺ ciun 4996   class class class wbr 5147   I cid 5572   Γ— cxp 5673  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β€œ cima 5678   ∘ ccom 5679  Fun wfun 6536   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411  Fincfn 8941  mVRcmvar 34750  mAxcmax 34754  mExcmex 34756  mDVcmdv 34757  mVarscmvrs 34758  mSubstcmsub 34760  mVHcmvh 34761  mPreStcmpst 34762  mStatcmsta 34764  mFScmfs 34765  mClscmcls 34766  mPPStcmpps 34767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-ot 4636  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  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 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-fz 13489  df-fzo 13632  df-seq 13971  df-hash 14295  df-word 14469  df-lsw 14517  df-concat 14525  df-s1 14550  df-substr 14595  df-pfx 14625  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-0g 17391  df-gsum 17392  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-mhm 18705  df-submnd 18706  df-frmd 18766  df-vrmd 18767  df-mrex 34775  df-mex 34776  df-mdv 34777  df-mvrs 34778  df-mrsub 34779  df-msub 34780  df-mvh 34781  df-mpst 34782  df-msr 34783  df-msta 34784  df-mfs 34785  df-mcls 34786
This theorem is referenced by:  mclspps  34873
  Copyright terms: Public domain W3C validator