Theorem f1otrgds

Description: Convenient lemma for f1otrg . (Contributed by Thierry Arnoux, 19-Mar-2019)

	Ref	Expression
Hypotheses	f1otrkg.p	$$⊢P={\mathrm{Base}}_G$$
	f1otrkg.d	$$⊢D=\mathrm{dist}\left(G\right)$$
	f1otrkg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	f1otrkg.b	$$⊢B={\mathrm{Base}}_H$$
	f1otrkg.e	$$⊢E=\mathrm{dist}\left(H\right)$$
	f1otrkg.j	$$⊢J=\mathrm{Itv}\left(H\right)$$
	f1otrkg.f	$$⊢\phi \to F:B\underset{1-1\; onto}{⟶}P$$
	f1otrkg.1	$$⊢\left(\phi \wedge \left(e\in B\wedge f\in B\right)\right)\to eEf=F\left(e\right)DF\left(f\right)$$
	f1otrkg.2	$$⊢\left(\phi \wedge \left(e\in B\wedge f\in B\wedge g\in B\right)\right)\to \left(g\in \left(eJf\right)\leftrightarrow F\left(g\right)\in \left(F\left(e\right)IF\left(f\right)\right)\right)$$
	f1otrgitv.x	$$⊢\phi \to X\in B$$
	f1otrgitv.y	$$⊢\phi \to Y\in B$$
Assertion	f1otrgds	$$⊢\phi \to XEY=F\left(X\right)DF\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1otrkg.p	$$⊢P={\mathrm{Base}}_G$$
2		f1otrkg.d	$$⊢D=\mathrm{dist}\left(G\right)$$
3		f1otrkg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		f1otrkg.b	$$⊢B={\mathrm{Base}}_H$$
5		f1otrkg.e	$$⊢E=\mathrm{dist}\left(H\right)$$
6		f1otrkg.j	$$⊢J=\mathrm{Itv}\left(H\right)$$
7		f1otrkg.f	$$⊢\phi \to F:B\underset{1-1\; onto}{⟶}P$$
8		f1otrkg.1	$$⊢\left(\phi \wedge \left(e\in B\wedge f\in B\right)\right)\to eEf=F\left(e\right)DF\left(f\right)$$
9		f1otrkg.2	$$⊢\left(\phi \wedge \left(e\in B\wedge f\in B\wedge g\in B\right)\right)\to \left(g\in \left(eJf\right)\leftrightarrow F\left(g\right)\in \left(F\left(e\right)IF\left(f\right)\right)\right)$$
10		f1otrgitv.x	$$⊢\phi \to X\in B$$
11		f1otrgitv.y	$$⊢\phi \to Y\in B$$
12	8	ralrimivva	$$⊢\phi \to \forall e\in B\forall f\in BeEf=F\left(e\right)DF\left(f\right)$$
13		oveq1	$$⊢e=X\to eEf=XEf$$
14		fveq2	$$⊢e=X\to F\left(e\right)=F\left(X\right)$$
15	14	oveq1d	$$⊢e=X\to F\left(e\right)DF\left(f\right)=F\left(X\right)DF\left(f\right)$$
16	13 15	eqeq12d	$$⊢e=X\to \left(eEf=F\left(e\right)DF\left(f\right)\leftrightarrow XEf=F\left(X\right)DF\left(f\right)\right)$$
17		oveq2	$$⊢f=Y\to XEf=XEY$$
18		fveq2	$$⊢f=Y\to F\left(f\right)=F\left(Y\right)$$
19	18	oveq2d	$$⊢f=Y\to F\left(X\right)DF\left(f\right)=F\left(X\right)DF\left(Y\right)$$
20	17 19	eqeq12d	$$⊢f=Y\to \left(XEf=F\left(X\right)DF\left(f\right)\leftrightarrow XEY=F\left(X\right)DF\left(Y\right)\right)$$
21	16 20	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall e\in B\forall f\in BeEf=F\left(e\right)DF\left(f\right)\to XEY=F\left(X\right)DF\left(Y\right)\right)$$
22	10 11 21	syl2anc	$$⊢\phi \to \left(\forall e\in B\forall f\in BeEf=F\left(e\right)DF\left(f\right)\to XEY=F\left(X\right)DF\left(Y\right)\right)$$
23	12 22	mpd	$$⊢\phi \to XEY=F\left(X\right)DF\left(Y\right)$$