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 34837
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 2732 . . . . . 6 (mRSubstβ€˜π‘‡) = (mRSubstβ€˜π‘‡)
3 msubvrs.s . . . . . 6 𝑆 = (mSubstβ€˜π‘‡)
41, 2, 3elmsubrn 34805 . . . . 5 ran 𝑆 = ran (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩))
54eleq2i 2825 . . . 4 (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)))
6 eqid 2732 . . . . 5 (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)) = (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩))
71fvexi 6905 . . . . . 6 𝐸 ∈ V
87mptex 7227 . . . . 5 (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) ∈ V
96, 8elrnmpti 5959 . . . 4 (𝐹 ∈ ran (𝑓 ∈ ran (mRSubstβ€˜π‘‡) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)) ↔ βˆƒπ‘“ ∈ ran (mRSubstβ€˜π‘‡)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩))
105, 9bitri 274 . . 3 (𝐹 ∈ ran 𝑆 ↔ βˆƒπ‘“ ∈ ran (mRSubstβ€˜π‘‡)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩))
11 simp2 1137 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝑓 ∈ ran (mRSubstβ€˜π‘‡))
12 simp3 1138 . . . . . . . . . . 11 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝑋 ∈ 𝐸)
13 eqid 2732 . . . . . . . . . . . 12 (mTCβ€˜π‘‡) = (mTCβ€˜π‘‡)
14 eqid 2732 . . . . . . . . . . . 12 (mRExβ€˜π‘‡) = (mRExβ€˜π‘‡)
1513, 1, 14mexval 34779 . . . . . . . . . . 11 𝐸 = ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡))
1612, 15eleqtrdi 2843 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝑋 ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
17 xp2nd 8010 . . . . . . . . . 10 (𝑋 ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)) β†’ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡))
1816, 17syl 17 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡))
19 eqid 2732 . . . . . . . . . 10 (mVRβ€˜π‘‡) = (mVRβ€˜π‘‡)
202, 19, 14mrsubvrs 34799 . . . . . . . . 9 ((𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡)) β†’ (ran (π‘“β€˜(2nd β€˜π‘‹)) ∩ (mVRβ€˜π‘‡)) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
2111, 18, 20syl2anc 584 . . . . . . . 8 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (ran (π‘“β€˜(2nd β€˜π‘‹)) ∩ (mVRβ€˜π‘‡)) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
22 fveq2 6891 . . . . . . . . . . . . 13 (𝑒 = 𝑋 β†’ (1st β€˜π‘’) = (1st β€˜π‘‹))
23 2fveq3 6896 . . . . . . . . . . . . 13 (𝑒 = 𝑋 β†’ (π‘“β€˜(2nd β€˜π‘’)) = (π‘“β€˜(2nd β€˜π‘‹)))
2422, 23opeq12d 4881 . . . . . . . . . . . 12 (𝑒 = 𝑋 β†’ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩ = ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩)
25 eqid 2732 . . . . . . . . . . . 12 (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)
26 opex 5464 . . . . . . . . . . . 12 ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩ ∈ V
2724, 25, 26fvmpt3i 7003 . . . . . . . . . . 11 (𝑋 ∈ 𝐸 β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹) = ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩)
2812, 27syl 17 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹) = ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩)
2928fveq2d 6895 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)) = (π‘‰β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩))
30 xp1st 8009 . . . . . . . . . . . . 13 (𝑋 ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)) β†’ (1st β€˜π‘‹) ∈ (mTCβ€˜π‘‡))
3116, 30syl 17 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (1st β€˜π‘‹) ∈ (mTCβ€˜π‘‡))
322, 14mrsubf 34794 . . . . . . . . . . . . . 14 (𝑓 ∈ ran (mRSubstβ€˜π‘‡) β†’ 𝑓:(mRExβ€˜π‘‡)⟢(mRExβ€˜π‘‡))
3311, 32syl 17 . . . . . . . . . . . . 13 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝑓:(mRExβ€˜π‘‡)⟢(mRExβ€˜π‘‡))
3417, 15eleq2s 2851 . . . . . . . . . . . . . 14 (𝑋 ∈ 𝐸 β†’ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡))
3512, 34syl 17 . . . . . . . . . . . . 13 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (2nd β€˜π‘‹) ∈ (mRExβ€˜π‘‡))
3633, 35ffvelcdmd 7087 . . . . . . . . . . . 12 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘“β€˜(2nd β€˜π‘‹)) ∈ (mRExβ€˜π‘‡))
37 opelxpi 5713 . . . . . . . . . . . 12 (((1st β€˜π‘‹) ∈ (mTCβ€˜π‘‡) ∧ (π‘“β€˜(2nd β€˜π‘‹)) ∈ (mRExβ€˜π‘‡)) β†’ ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩ ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
3831, 36, 37syl2anc 584 . . . . . . . . . . 11 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩ ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
3938, 15eleqtrrdi 2844 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ ⟨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩ ∈ 𝐸)
40 msubvrs.v . . . . . . . . . . 11 𝑉 = (mVarsβ€˜π‘‡)
4119, 1, 40mvrsval 34782 . . . . . . . . . 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 6904 . . . . . . . . . . . . 13 (1st β€˜π‘‹) ∈ V
44 fvex 6904 . . . . . . . . . . . . 13 (π‘“β€˜(2nd β€˜π‘‹)) ∈ V
4543, 44op2nd 7986 . . . . . . . . . . . 12 (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) = (π‘“β€˜(2nd β€˜π‘‹))
4645a1i 11 . . . . . . . . . . 11 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) = (π‘“β€˜(2nd β€˜π‘‹)))
4746rneqd 5937 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ ran (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) = ran (π‘“β€˜(2nd β€˜π‘‹)))
4847ineq1d 4211 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (ran (2nd β€˜βŸ¨(1st β€˜π‘‹), (π‘“β€˜(2nd β€˜π‘‹))⟩) ∩ (mVRβ€˜π‘‡)) = (ran (π‘“β€˜(2nd β€˜π‘‹)) ∩ (mVRβ€˜π‘‡)))
4929, 42, 483eqtrd 2776 . . . . . . . 8 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)) = (ran (π‘“β€˜(2nd β€˜π‘‹)) ∩ (mVRβ€˜π‘‡)))
5019, 1, 40mvrsval 34782 . . . . . . . . . . 11 (𝑋 ∈ 𝐸 β†’ (π‘‰β€˜π‘‹) = (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡)))
5112, 50syl 17 . . . . . . . . . 10 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜π‘‹) = (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡)))
5251iuneq1d 5024 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))))
53 msubvrs.h . . . . . . . . . . . . . . . . 17 𝐻 = (mVHβ€˜π‘‡)
5419, 1, 53mvhf 34835 . . . . . . . . . . . . . . . 16 (𝑇 ∈ mFS β†’ 𝐻:(mVRβ€˜π‘‡)⟢𝐸)
55543ad2ant1 1133 . . . . . . . . . . . . . . 15 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ 𝐻:(mVRβ€˜π‘‡)⟢𝐸)
56 inss2 4229 . . . . . . . . . . . . . . . 16 (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡)) βŠ† (mVRβ€˜π‘‡)
5756sseli 3978 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡)) β†’ π‘₯ ∈ (mVRβ€˜π‘‡))
58 ffvelcdm 7083 . . . . . . . . . . . . . . 15 ((𝐻:(mVRβ€˜π‘‡)⟢𝐸 ∧ π‘₯ ∈ (mVRβ€˜π‘‡)) β†’ (π»β€˜π‘₯) ∈ 𝐸)
5955, 57, 58syl2an 596 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π»β€˜π‘₯) ∈ 𝐸)
60 fveq2 6891 . . . . . . . . . . . . . . . 16 (𝑒 = (π»β€˜π‘₯) β†’ (1st β€˜π‘’) = (1st β€˜(π»β€˜π‘₯)))
61 2fveq3 6896 . . . . . . . . . . . . . . . 16 (𝑒 = (π»β€˜π‘₯) β†’ (π‘“β€˜(2nd β€˜π‘’)) = (π‘“β€˜(2nd β€˜(π»β€˜π‘₯))))
6260, 61opeq12d 4881 . . . . . . . . . . . . . . 15 (𝑒 = (π»β€˜π‘₯) β†’ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩ = ⟨(1st β€˜(π»β€˜π‘₯)), (π‘“β€˜(2nd β€˜(π»β€˜π‘₯)))⟩)
6362, 25, 26fvmpt3i 7003 . . . . . . . . . . . . . 14 ((π»β€˜π‘₯) ∈ 𝐸 β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)) = ⟨(1st β€˜(π»β€˜π‘₯)), (π‘“β€˜(2nd β€˜(π»β€˜π‘₯)))⟩)
6459, 63syl 17 . . . . . . . . . . . . 13 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)) = ⟨(1st β€˜(π»β€˜π‘₯)), (π‘“β€˜(2nd β€˜(π»β€˜π‘₯)))⟩)
6557adantl 482 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ π‘₯ ∈ (mVRβ€˜π‘‡))
66 eqid 2732 . . . . . . . . . . . . . . . . 17 (mTypeβ€˜π‘‡) = (mTypeβ€˜π‘‡)
6719, 66, 53mvhval 34811 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (mVRβ€˜π‘‡) β†’ (π»β€˜π‘₯) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), βŸ¨β€œπ‘₯β€βŸ©βŸ©)
6865, 67syl 17 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π»β€˜π‘₯) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), βŸ¨β€œπ‘₯β€βŸ©βŸ©)
69 fvex 6904 . . . . . . . . . . . . . . . 16 ((mTypeβ€˜π‘‡)β€˜π‘₯) ∈ V
70 s1cli 14559 . . . . . . . . . . . . . . . . 17 βŸ¨β€œπ‘₯β€βŸ© ∈ Word V
7170elexi 3493 . . . . . . . . . . . . . . . 16 βŸ¨β€œπ‘₯β€βŸ© ∈ V
7269, 71op1std 7987 . . . . . . . . . . . . . . 15 ((π»β€˜π‘₯) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), βŸ¨β€œπ‘₯β€βŸ©βŸ© β†’ (1st β€˜(π»β€˜π‘₯)) = ((mTypeβ€˜π‘‡)β€˜π‘₯))
7368, 72syl 17 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (1st β€˜(π»β€˜π‘₯)) = ((mTypeβ€˜π‘‡)β€˜π‘₯))
7469, 71op2ndd 7988 . . . . . . . . . . . . . . . 16 ((π»β€˜π‘₯) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), βŸ¨β€œπ‘₯β€βŸ©βŸ© β†’ (2nd β€˜(π»β€˜π‘₯)) = βŸ¨β€œπ‘₯β€βŸ©)
7568, 74syl 17 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (2nd β€˜(π»β€˜π‘₯)) = βŸ¨β€œπ‘₯β€βŸ©)
7675fveq2d 6895 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘“β€˜(2nd β€˜(π»β€˜π‘₯))) = (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©))
7773, 76opeq12d 4881 . . . . . . . . . . . . 13 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ⟨(1st β€˜(π»β€˜π‘₯)), (π‘“β€˜(2nd β€˜(π»β€˜π‘₯)))⟩ = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩)
7864, 77eqtrd 2772 . . . . . . . . . . . 12 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)) = ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩)
7978fveq2d 6895 . . . . . . . . . . 11 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = (π‘‰β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩))
80 simpl1 1191 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ 𝑇 ∈ mFS)
8119, 13, 66mtyf2 34828 . . . . . . . . . . . . . . . 16 (𝑇 ∈ mFS β†’ (mTypeβ€˜π‘‡):(mVRβ€˜π‘‡)⟢(mTCβ€˜π‘‡))
8280, 81syl 17 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (mTypeβ€˜π‘‡):(mVRβ€˜π‘‡)⟢(mTCβ€˜π‘‡))
8382, 65ffvelcdmd 7087 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ((mTypeβ€˜π‘‡)β€˜π‘₯) ∈ (mTCβ€˜π‘‡))
8433adantr 481 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ 𝑓:(mRExβ€˜π‘‡)⟢(mRExβ€˜π‘‡))
85 elun2 4177 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (mVRβ€˜π‘‡) β†’ π‘₯ ∈ ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
8665, 85syl 17 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ π‘₯ ∈ ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
8786s1cld 14557 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ βŸ¨β€œπ‘₯β€βŸ© ∈ Word ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
88 eqid 2732 . . . . . . . . . . . . . . . . . 18 (mCNβ€˜π‘‡) = (mCNβ€˜π‘‡)
8988, 19, 14mrexval 34778 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ mFS β†’ (mRExβ€˜π‘‡) = Word ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
9080, 89syl 17 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (mRExβ€˜π‘‡) = Word ((mCNβ€˜π‘‡) βˆͺ (mVRβ€˜π‘‡)))
9187, 90eleqtrrd 2836 . . . . . . . . . . . . . . 15 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ βŸ¨β€œπ‘₯β€βŸ© ∈ (mRExβ€˜π‘‡))
9284, 91ffvelcdmd 7087 . . . . . . . . . . . . . 14 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∈ (mRExβ€˜π‘‡))
93 opelxpi 5713 . . . . . . . . . . . . . 14 ((((mTypeβ€˜π‘‡)β€˜π‘₯) ∈ (mTCβ€˜π‘‡) ∧ (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∈ (mRExβ€˜π‘‡)) β†’ ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩ ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
9483, 92, 93syl2anc 584 . . . . . . . . . . . . 13 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩ ∈ ((mTCβ€˜π‘‡) Γ— (mRExβ€˜π‘‡)))
9594, 15eleqtrrdi 2844 . . . . . . . . . . . 12 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩ ∈ 𝐸)
9619, 1, 40mvrsval 34782 . . . . . . . . . . . 12 (⟨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩ ∈ 𝐸 β†’ (π‘‰β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = (ran (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) ∩ (mVRβ€˜π‘‡)))
9795, 96syl 17 . . . . . . . . . . 11 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘‰β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = (ran (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) ∩ (mVRβ€˜π‘‡)))
98 fvex 6904 . . . . . . . . . . . . . . 15 (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∈ V
9969, 98op2nd 7986 . . . . . . . . . . . . . 14 (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)
10099a1i 11 . . . . . . . . . . . . 13 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©))
101100rneqd 5937 . . . . . . . . . . . 12 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ ran (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) = ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©))
102101ineq1d 4211 . . . . . . . . . . 11 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (ran (2nd β€˜βŸ¨((mTypeβ€˜π‘‡)β€˜π‘₯), (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©)⟩) ∩ (mVRβ€˜π‘‡)) = (ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
10379, 97, 1023eqtrd 2776 . . . . . . . . . 10 (((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) ∧ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = (ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
104103iuneq2dv 5021 . . . . . . . . 9 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
10552, 104eqtrd 2772 . . . . . . . 8 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))) = βˆͺ π‘₯ ∈ (ran (2nd β€˜π‘‹) ∩ (mVRβ€˜π‘‡))(ran (π‘“β€˜βŸ¨β€œπ‘₯β€βŸ©) ∩ (mVRβ€˜π‘‡)))
10621, 49, 1053eqtr4d 2782 . . . . . . 7 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))))
107 fveq1 6890 . . . . . . . . 9 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (πΉβ€˜π‘‹) = ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹))
108107fveq2d 6895 . . . . . . . 8 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)))
109 fveq1 6890 . . . . . . . . . 10 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (πΉβ€˜(π»β€˜π‘₯)) = ((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)))
110109fveq2d 6895 . . . . . . . . 9 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))) = (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))))
111110iuneq2d 5026 . . . . . . . 8 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯))))
112108, 111eqeq12d 2748 . . . . . . 7 (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ ((π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))) ↔ (π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜((𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩)β€˜(π»β€˜π‘₯)))))
113106, 112syl5ibrcom 246 . . . . . 6 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡) ∧ 𝑋 ∈ 𝐸) β†’ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯)))))
1141133expia 1121 . . . . 5 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡)) β†’ (𝑋 ∈ 𝐸 β†’ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))))
115114com23 86 . . . 4 ((𝑇 ∈ mFS ∧ 𝑓 ∈ ran (mRSubstβ€˜π‘‡)) β†’ (𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (𝑋 ∈ 𝐸 β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))))
116115rexlimdva 3155 . . 3 (𝑇 ∈ mFS β†’ (βˆƒπ‘“ ∈ ran (mRSubstβ€˜π‘‡)𝐹 = (𝑒 ∈ 𝐸 ↦ ⟨(1st β€˜π‘’), (π‘“β€˜(2nd β€˜π‘’))⟩) β†’ (𝑋 ∈ 𝐸 β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))))
11710, 116biimtrid 241 . 2 (𝑇 ∈ mFS β†’ (𝐹 ∈ ran 𝑆 β†’ (𝑋 ∈ 𝐸 β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))))
1181173imp 1111 1 ((𝑇 ∈ mFS ∧ 𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝐸) β†’ (π‘‰β€˜(πΉβ€˜π‘‹)) = βˆͺ π‘₯ ∈ (π‘‰β€˜π‘‹)(π‘‰β€˜(πΉβ€˜(π»β€˜π‘₯))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆƒwrex 3070  Vcvv 3474   βˆͺ cun 3946   ∩ cin 3947  βŸ¨cop 4634  βˆͺ ciun 4997   ↦ cmpt 5231   Γ— cxp 5674  ran crn 5677  βŸΆwf 6539  β€˜cfv 6543  1st c1st 7975  2nd c2nd 7976  Word cword 14468  βŸ¨β€œcs1 14549  mCNcmcn 34737  mVRcmvar 34738  mTypecmty 34739  mTCcmtc 34741  mRExcmrex 34743  mExcmex 34744  mVarscmvrs 34746  mRSubstcmrsub 34747  mSubstcmsub 34748  mVHcmvh 34749  mFScmfs 34753
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  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 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  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-submnd 18706  df-frmd 18766  df-mrex 34763  df-mex 34764  df-mvrs 34766  df-mrsub 34767  df-msub 34768  df-mvh 34769  df-mfs 34773
This theorem is referenced by:  mclsppslem  34860
  Copyright terms: Public domain W3C validator