Theorem strfv2d

Description: Deduction version of strfv2 . (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	strfv2d.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	strfv2d.s	$$⊢\phi \to S\in V$$
	strfv2d.f	$$⊢\phi \to \mathrm{Fun}{S^{-1}}^{-1}$$
	strfv2d.n	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
	strfv2d.c	$$⊢\phi \to C\in W$$
Assertion	strfv2d	$$⊢\phi \to C=E\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		strfv2d.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
2		strfv2d.s	$$⊢\phi \to S\in V$$
3		strfv2d.f	$$⊢\phi \to \mathrm{Fun}{S^{-1}}^{-1}$$
4		strfv2d.n	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
5		strfv2d.c	$$⊢\phi \to C\in W$$
6	1 2	strfvnd	$$⊢\phi \to E\left(S\right)=S\left(E\left(\mathrm{ndx}\right)\right)$$
7		cnvcnv2	$$⊢{S^{-1}}^{-1}={S\upharpoonright }_{\mathrm{V}}$$
8	7	fveq1i	$$⊢{S^{-1}}^{-1}\left(E\left(\mathrm{ndx}\right)\right)=\left({S\upharpoonright }_{\mathrm{V}}\right)\left(E\left(\mathrm{ndx}\right)\right)$$
9		fvex	$$⊢E\left(\mathrm{ndx}\right)\in \mathrm{V}$$
10		fvres	$$⊢E\left(\mathrm{ndx}\right)\in \mathrm{V}\to \left({S\upharpoonright }_{\mathrm{V}}\right)\left(E\left(\mathrm{ndx}\right)\right)=S\left(E\left(\mathrm{ndx}\right)\right)$$
11	9 10	ax-mp	$$⊢\left({S\upharpoonright }_{\mathrm{V}}\right)\left(E\left(\mathrm{ndx}\right)\right)=S\left(E\left(\mathrm{ndx}\right)\right)$$
12	8 11	eqtri	$$⊢{S^{-1}}^{-1}\left(E\left(\mathrm{ndx}\right)\right)=S\left(E\left(\mathrm{ndx}\right)\right)$$
13	5	elexd	$$⊢\phi \to C\in \mathrm{V}$$
14		opelxpi	$$⊢\left(E\left(\mathrm{ndx}\right)\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to ⟨E\left(\mathrm{ndx}\right),C⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
15	9 13 14	sylancr	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
16	4 15	elind	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in \left(S\cap \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
17		cnvcnv	$$⊢{S^{-1}}^{-1}=S\cap \left(\mathrm{V}\times \mathrm{V}\right)$$
18	16 17	eleqtrrdi	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in {S^{-1}}^{-1}$$
19		funopfv	$$⊢\mathrm{Fun}{S^{-1}}^{-1}\to \left(⟨E\left(\mathrm{ndx}\right),C⟩\in {S^{-1}}^{-1}\to {S^{-1}}^{-1}\left(E\left(\mathrm{ndx}\right)\right)=C\right)$$
20	3 18 19	sylc	$$⊢\phi \to {S^{-1}}^{-1}\left(E\left(\mathrm{ndx}\right)\right)=C$$
21	12 20	eqtr3id	$$⊢\phi \to S\left(E\left(\mathrm{ndx}\right)\right)=C$$
22	6 21	eqtr2d	$$⊢\phi \to C=E\left(S\right)$$