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

Theorem msubvrs 34582
Description: The set of variables in a substitution is the union, indexed by the variables in the original expression, of the variables in the substitution to that variable. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
msubvrs.s 𝑆 = (mSubstβ€˜π‘‡)
msubvrs.e 𝐸 = (mExβ€˜π‘‡)
msubvrs.v 𝑉 = (mVarsβ€˜π‘‡)
msubvrs.h 𝐻 = (mVHβ€˜π‘‡)
Assertion
Ref Expression
msubvrs ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))
Distinct variable groups:   π‘₯,𝐸   π‘₯,𝐹   π‘₯,𝑇   π‘₯,𝑋   π‘₯,𝑉
Allowed substitution hints:   𝑆(π‘₯)   𝐻(π‘₯)

Proof of Theorem msubvrs
Dummy variables 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 msubvrs.e . . . . . 6 𝐸 = (mExβ€˜π‘‡)
2 eqid 2733 . . . . . 6 (mRSubstβ€˜π‘‡) = (mRSubstβ€˜π‘‡)
3 msubvrs.s . . . . . 6 𝑆 = (mSubstβ€˜π‘‡)
41, 2, 3elmsubrn 34550 . . . . 5 ran 𝑆 = ran (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩))
54eleq2i 2826 . . . 4 (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)))
6 eqid 2733 . . . . 5 (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)) = (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩))
71fvexi 6906 . . . . . 6 𝐸 ∈ V
87mptex 7225 . . . . 5 (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) ∈ V
96, 8elrnmpti 5960 . . . 4 (𝐹 ∈ ran (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)) ↔ βˆƒπ‘“ ∈ ran (mRSubstβ€˜π‘‡)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩))
105, 9bitri 275 . . 3 (𝐹 ∈ ran 𝑆 ↔ βˆƒπ‘“ ∈ ran (mRSubstβ€˜π‘‡)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩))
11 simp2 1138 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝑓 ∈ ran (mRSubstβ€˜π‘‡))
12 simp3 1139 . . . . . . . . . . 11 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝑋 ∈ 𝐸)
13 eqid 2733 . . . . . . . . . . . 12 (mTCβ€˜π‘‡) = (mTCβ€˜π‘‡)
14 eqid 2733 . . . . . . . . . . . 12 (mRExβ€˜π‘‡) = (mRExβ€˜π‘‡)
1513, 1, 14mexval 34524 . . . . . . . . . . 11 𝐸 = ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡))
1612, 15eleqtrdi 2844 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝑋 ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
17 xp2nd 8008 . . . . . . . . . 10 (𝑋 ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)) β†’ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡))
1816, 17syl 17 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡))
19 eqid 2733 . . . . . . . . . 10 (mVRβ€˜π‘‡) = (mVRβ€˜π‘‡)
202, 19, 14mrsubvrs 34544 . . . . . . . . 9 ((𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡)) β†’ (ran (π‘“β€˜(2nd β€˜π‘‹)) ∩ (mVRβ€˜π‘‡)) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
2111, 18, 20syl2anc 585 . . . . . . . 8 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (ran (π‘“β€˜(2nd β€˜π‘‹)) ∩ (mVRβ€˜π‘‡)) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
22 fveq2 6892 . . . . . . . . . . . . 13 (𝑒 = 𝑋 β†’ (1st β€˜π‘’) = (1st β€˜π‘‹))
23 2fveq3 6897 . . . . . . . . . . . . 13 (𝑒 = 𝑋 β†’ (π‘“β€˜(2nd β€˜π‘’)) = (π‘“β€˜(2nd β€˜π‘‹)))
2422, 23opeq12d 4882 . . . . . . . . . . . 12 (𝑒 = 𝑋 β†’ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩ = ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩)
25 eqid 2733 . . . . . . . . . . . 12 (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)
26 opex 5465 . . . . . . . . . . . 12 ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩ ∈ V
2724, 25, 26fvmpt3i 7004 . . . . . . . . . . 11 (𝑋 ∈ 𝐸 β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹) = ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩)
2812, 27syl 17 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹) = ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩)
2928fveq2d 6896 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)) = (π‘‰β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩))
30 xp1st 8007 . . . . . . . . . . . . 13 (𝑋 ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)) β†’ (1st β€˜π‘‹) ∈ (mTCβ€˜π‘‡))
3116, 30syl 17 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (1st β€˜π‘‹) ∈ (mTCβ€˜π‘‡))
322, 14mrsubf 34539 . . . . . . . . . . . . . 14 (𝑓 ∈ ran (mRSubstβ€˜π‘‡) β†’ 𝑓:(mRExβ€˜π‘‡)⟢(mRExβ€˜π‘‡))
3311, 32syl 17 . . . . . . . . . . . . 13 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝑓:(mRExβ€˜π‘‡)⟢(mRExβ€˜π‘‡))
3417, 15eleq2s 2852 . . . . . . . . . . . . . 14 (𝑋 ∈ 𝐸 β†’ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡))
3512, 34syl 17 . . . . . . . . . . . . 13 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡))
3633, 35ffvelcdmd 7088 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘“β€˜(2nd β€˜π‘‹)) ∈ (mRExβ€˜π‘‡))
37 opelxpi 5714 . . . . . . . . . . . 12 (((1st β€˜π‘‹) ∈ (mTCβ€˜π‘‡) ∧ (π‘“β€˜(2nd β€˜π‘‹)) ∈ (mRExβ€˜π‘‡)) β†’ ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩ ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
3831, 36, 37syl2anc 585 . . . . . . . . . . 11 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩ ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
3938, 15eleqtrrdi 2845 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩ ∈ 𝐸)
40 msubvrs.v . . . . . . . . . . 11 𝑉 = (mVarsβ€˜π‘‡)
4119, 1, 40mvrsval 34527 . . . . . . . . . 10 (⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩ ∈ 𝐸 β†’ (π‘‰β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) = (ran (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) ∩ (mVRβ€˜π‘‡)))
4239, 41syl 17 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) = (ran (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) ∩ (mVRβ€˜π‘‡)))
43 fvex 6905 . . . . . . . . . . . . 13 (1st β€˜π‘‹) ∈ V
44 fvex 6905 . . . . . . . . . . . . 13 (π‘“β€˜(2nd β€˜π‘‹)) ∈ V
4543, 44op2nd 7984 . . . . . . . . . . . 12 (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) = (π‘“β€˜(2nd β€˜π‘‹))
4645a1i 11 . . . . . . . . . . 11 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) = (π‘“β€˜(2nd β€˜π‘‹)))
4746rneqd 5938 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ ran (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) = ran (π‘“β€˜(2nd β€˜π‘‹)))
4847ineq1d 4212 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (ran (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) ∩ (mVRβ€˜π‘‡)) = (ran (π‘“β€˜(2nd β€˜π‘‹)) ∩ (mVRβ€˜π‘‡)))
4929, 42, 483eqtrd 2777 . . . . . . . 8 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)) = (ran (π‘“β€˜(2nd β€˜π‘‹)) ∩ (mVRβ€˜π‘‡)))
5019, 1, 40mvrsval 34527 . . . . . . . . . . 11 (𝑋 ∈ 𝐸 β†’ (π‘‰β€˜π‘‹) = (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡)))
5112, 50syl 17 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜π‘‹) = (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡)))
5251iuneq1d 5025 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))))
53 msubvrs.h . . . . . . . . . . . . . . . . 17 𝐻 = (mVHβ€˜π‘‡)
5419, 1, 53mvhf 34580 . . . . . . . . . . . . . . . 16 (𝑇 ∈ mFS β†’ 𝐻:(mVRβ€˜π‘‡)⟢𝐸)
55543ad2ant1 1134 . . . . . . . . . . . . . . 15 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝐻:(mVRβ€˜π‘‡)⟢𝐸)
56 inss2 4230 . . . . . . . . . . . . . . . 16 (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡)) βŠ† (mVRβ€˜π‘‡)
5756sseli 3979 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡)) β†’ π‘₯ ∈ (mVRβ€˜π‘‡))
58 ffvelcdm 7084 . . . . . . . . . . . . . . 15 ((𝐻:(mVRβ€˜π‘‡)⟢𝐸 ∧ π‘₯ ∈ (mVRβ€˜π‘‡)) β†’ (π»β€˜π‘₯) ∈ 𝐸)
5955, 57, 58syl2an 597 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π»β€˜π‘₯) ∈ 𝐸)
60 fveq2 6892 . . . . . . . . . . . . . . . 16 (𝑒 = (π»β€˜π‘₯) β†’ (1st β€˜π‘’) = (1st β€˜(π»β€˜π‘₯)))
61 2fveq3 6897 . . . . . . . . . . . . . . . 16 (𝑒 = (π»β€˜π‘₯) β†’ (π‘“β€˜(2nd β€˜π‘’)) = (π‘“β€˜(2nd β€˜(π»β€˜π‘₯))))
6260, 61opeq12d 4882 . . . . . . . . . . . . . . 15 (𝑒 = (π»β€˜π‘₯) β†’ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩ = ⟨(1st β€˜(π»β€˜π‘₯)), (π‘“β€˜(2nd β€˜(π»β€˜π‘₯)))⟩)
6362, 25, 26fvmpt3i 7004 . . . . . . . . . . . . . 14 ((π»β€˜π‘₯) ∈ 𝐸 β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)) = ⟨(1st β€˜(π»β€˜π‘₯)), (π‘“β€˜(2nd β€˜(π»β€˜π‘₯)))⟩)
6459, 63syl 17 . . . . . . . . . . . . 13 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)) = ⟨(1st β€˜(π»β€˜π‘₯)), (π‘“β€˜(2nd β€˜(π»β€˜π‘₯)))⟩)
6557adantl 483 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ π‘₯ ∈ (mVRβ€˜π‘‡))
66 eqid 2733 . . . . . . . . . . . . . . . . 17 (mTypeβ€˜π‘‡) = (mTypeβ€˜π‘‡)
6719, 66, 53mvhval 34556 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (mVRβ€˜π‘‡) β†’ (π»β€˜π‘₯) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), βŸ¨β€œπ‘₯β€βŸ©βŸ©)
6865, 67syl 17 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π»β€˜π‘₯) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), βŸ¨β€œπ‘₯β€βŸ©βŸ©)
69 fvex 6905 . . . . . . . . . . . . . . . 16 ((mTypeβ€˜π‘‡)β€˜π‘₯) ∈ V
70 s1cli 14555 . . . . . . . . . . . . . . . . 17 βŸ¨β€œπ‘₯β€βŸ© ∈ Word V
7170elexi 3494 . . . . . . . . . . . . . . . 16 βŸ¨β€œπ‘₯β€βŸ© ∈ V
7269, 71op1std 7985 . . . . . . . . . . . . . . 15 ((π»β€˜π‘₯) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), βŸ¨β€œπ‘₯β€βŸ©βŸ© β†’ (1st β€˜(π»β€˜π‘₯)) = ((mTypeβ€˜π‘‡)β€˜π‘₯))
7368, 72syl 17 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (1st β€˜(π»β€˜π‘₯)) = ((mTypeβ€˜π‘‡)β€˜π‘₯))
7469, 71op2ndd 7986 . . . . . . . . . . . . . . . 16 ((π»β€˜π‘₯) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), βŸ¨β€œπ‘₯β€βŸ©βŸ© β†’ (2nd β€˜(π»β€˜π‘₯)) = βŸ¨β€œπ‘₯β€βŸ©)
7568, 74syl 17 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (2nd β€˜(π»β€˜π‘₯)) = βŸ¨β€œπ‘₯β€βŸ©)
7675fveq2d 6896 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘“β€˜(2nd β€˜(π»β€˜π‘₯))) = (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©))
7773, 76opeq12d 4882 . . . . . . . . . . . . 13 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ⟨(1st β€˜(π»β€˜π‘₯)), (π‘“β€˜(2nd β€˜(π»β€˜π‘₯)))⟩ = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩)
7864, 77eqtrd 2773 . . . . . . . . . . . 12 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩)
7978fveq2d 6896 . . . . . . . . . . 11 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = (π‘‰β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩))
80 simpl1 1192 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ 𝑇 ∈ mFS)
8119, 13, 66mtyf2 34573 . . . . . . . . . . . . . . . 16 (𝑇 ∈ mFS β†’ (mTypeβ€˜π‘‡):(mVRβ€˜π‘‡)⟢(mTCβ€˜π‘‡))
8280, 81syl 17 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (mTypeβ€˜π‘‡):(mVRβ€˜π‘‡)⟢(mTCβ€˜π‘‡))
8382, 65ffvelcdmd 7088 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ((mTypeβ€˜π‘‡)β€˜π‘₯) ∈ (mTCβ€˜π‘‡))
8433adantr 482 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ 𝑓:(mRExβ€˜π‘‡)⟢(mRExβ€˜π‘‡))
85 elun2 4178 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (mVRβ€˜π‘‡) β†’ π‘₯ ∈ ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
8665, 85syl 17 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ π‘₯ ∈ ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
8786s1cld 14553 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ βŸ¨β€œπ‘₯β€βŸ© ∈ Word ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
88 eqid 2733 . . . . . . . . . . . . . . . . . 18 (mCNβ€˜π‘‡) = (mCNβ€˜π‘‡)
8988, 19, 14mrexval 34523 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ mFS β†’ (mRExβ€˜π‘‡) = Word ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
9080, 89syl 17 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (mRExβ€˜π‘‡) = Word ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
9187, 90eleqtrrd 2837 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ βŸ¨β€œπ‘₯β€βŸ© ∈ (mRExβ€˜π‘‡))
9284, 91ffvelcdmd 7088 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∈ (mRExβ€˜π‘‡))
93 opelxpi 5714 . . . . . . . . . . . . . 14 ((((mTypeβ€˜π‘‡)β€˜π‘₯) ∈ (mTCβ€˜π‘‡) ∧ (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∈ (mRExβ€˜π‘‡)) β†’ ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩ ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
9483, 92, 93syl2anc 585 . . . . . . . . . . . . 13 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩ ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
9594, 15eleqtrrdi 2845 . . . . . . . . . . . 12 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩ ∈ 𝐸)
9619, 1, 40mvrsval 34527 . . . . . . . . . . . 12 (⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩ ∈ 𝐸 β†’ (π‘‰β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = (ran (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) ∩ (mVRβ€˜π‘‡)))
9795, 96syl 17 . . . . . . . . . . 11 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘‰β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = (ran (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) ∩ (mVRβ€˜π‘‡)))
98 fvex 6905 . . . . . . . . . . . . . . 15 (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∈ V
9969, 98op2nd 7984 . . . . . . . . . . . . . 14 (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)
10099a1i 11 . . . . . . . . . . . . 13 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©))
101100rneqd 5938 . . . . . . . . . . . 12 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ran (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©))
102101ineq1d 4212 . . . . . . . . . . 11 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (ran (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) ∩ (mVRβ€˜π‘‡)) = (ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
10379, 97, 1023eqtrd 2777 . . . . . . . . . 10 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = (ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
104103iuneq2dv 5022 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
10552, 104eqtrd 2773 . . . . . . . 8 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
10621, 49, 1053eqtr4d 2783 . . . . . . 7 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))))
107 fveq1 6891 . . . . . . . . 9 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (πΉβ€˜π‘‹) = ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹))
108107fveq2d 6896 . . . . . . . 8 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)))
109 fveq1 6891 . . . . . . . . . 10 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (πΉβ€˜(π»β€˜π‘₯)) = ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)))
110109fveq2d 6896 . . . . . . . . 9 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))) = (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))))
111110iuneq2d 5027 . . . . . . . 8 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))))
112108, 111eqeq12d 2749 . . . . . . 7 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ ((π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))) ↔ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)))))
113106, 112syl5ibrcom 246 . . . . . 6 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯)))))
1141133expia 1122 . . . . 5 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡)) β†’ (𝑋 ∈ 𝐸 β†’ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))))
115114com23 86 . . . 4 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡)) β†’ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (𝑋 ∈ 𝐸 β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))))
116115rexlimdva 3156 . . 3 (𝑇 ∈ mFS β†’ (βˆƒπ‘“ ∈ ran (mRSubstβ€˜π‘‡)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (𝑋 ∈ 𝐸 β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))))
11710, 116biimtrid 241 . 2 (𝑇 ∈ mFS β†’ (𝐹 ∈ ran 𝑆 β†’ (𝑋 ∈ 𝐸 β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))))
1181173imp 1112 1 ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆƒwrex 3071  Vcvv 3475   βˆͺ cun 3947   ∩ cin 3948  βŸ¨cop 4635  βˆͺ ciun 4998   ↦ cmpt 5232   Γ— cxp 5675  ran crn 5678  βŸΆwf 6540  β€˜cfv 6544  1st c1st 7973  2nd c2nd 7974  Word cword 14464  βŸ¨β€œcs1 14545  mCNcmcn 34482  mVRcmvar 34483  mTypecmty 34484  mTCcmtc 34486  mRExcmrex 34488  mExcmex 34489  mVarscmvrs 34491  mRSubstcmrsub 34492  mSubstcmsub 34493  mVHcmvh 34494  mFScmfs 34498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-n0 12473  df-xnn0 12545  df-z 12559  df-uz 12823  df-fz 13485  df-fzo 13628  df-seq 13967  df-hash 14291  df-word 14465  df-lsw 14513  df-concat 14521  df-s1 14546  df-substr 14591  df-pfx 14621  df-struct 17080  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-ress 17174  df-plusg 17210  df-0g 17387  df-gsum 17388  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-submnd 18672  df-frmd 18730  df-mrex 34508  df-mex 34509  df-mvrs 34511  df-mrsub 34512  df-msub 34513  df-mvh 34514  df-mfs 34518
This theorem is referenced by:  mclsppslem  34605
  Copyright terms: Public domain W3C validator