Theorem evthf

Description: A version of evth using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	evthf.1	$$⊢\underset{\_}{Ⅎ}xF$$
	evthf.2	$$⊢\underset{\_}{Ⅎ}yF$$
	evthf.3	$$⊢\underset{\_}{Ⅎ}xX$$
	evthf.4	$$⊢\underset{\_}{Ⅎ}yX$$
	evthf.5	$$⊢Ⅎx\phi$$
	evthf.6	$$⊢Ⅎy\phi$$
	evthf.7	$$⊢X=\bigcup J$$
	evthf.8	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	evthf.9	$$⊢\phi \to J\in \mathrm{Comp}$$
	evthf.10	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
	evthf.11	$$⊢\phi \to X\ne \varnothing$$
Assertion	evthf	$$⊢\phi \to \exists x\in X\forall y\in XF\left(y\right)\le F\left(x\right)$$

Proof

Step	Hyp	Ref	Expression
1		evthf.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		evthf.2	$$⊢\underset{\_}{Ⅎ}yF$$
3		evthf.3	$$⊢\underset{\_}{Ⅎ}xX$$
4		evthf.4	$$⊢\underset{\_}{Ⅎ}yX$$
5		evthf.5	$$⊢Ⅎx\phi$$
6		evthf.6	$$⊢Ⅎy\phi$$
7		evthf.7	$$⊢X=\bigcup J$$
8		evthf.8	$$⊢K=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
9		evthf.9	$$⊢\phi \to J\in \mathrm{Comp}$$
10		evthf.10	$$⊢\phi \to F\in \left(J\mathrm{Cn}K\right)$$
11		evthf.11	$$⊢\phi \to X\ne \varnothing$$
12	7 8 9 10 11	evth	$$⊢\phi \to \exists a\in X\forall b\in XF\left(b\right)\le F\left(a\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}bX$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}yb$$
15	2 14	nffv	$$⊢\underset{\_}{Ⅎ}yF\left(b\right)$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}y\le$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}ya$$
18	2 17	nffv	$$⊢\underset{\_}{Ⅎ}yF\left(a\right)$$
19	15 16 18	nfbr	$$⊢ℲyF\left(b\right)\le F\left(a\right)$$
20		nfv	$$⊢ℲbF\left(y\right)\le F\left(a\right)$$
21		fveq2	$$⊢b=y\to F\left(b\right)=F\left(y\right)$$
22	21	breq1d	$$⊢b=y\to \left(F\left(b\right)\le F\left(a\right)\leftrightarrow F\left(y\right)\le F\left(a\right)\right)$$
23	13 4 19 20 22	cbvralfw	$$⊢\forall b\in XF\left(b\right)\le F\left(a\right)\leftrightarrow \forall y\in XF\left(y\right)\le F\left(a\right)$$
24	23	rexbii	$$⊢\exists a\in X\forall b\in XF\left(b\right)\le F\left(a\right)\leftrightarrow \exists a\in X\forall y\in XF\left(y\right)\le F\left(a\right)$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}aX$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
27	1 26	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(y\right)$$
28		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}xa$$
30	1 29	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(a\right)$$
31	27 28 30	nfbr	$$⊢ℲxF\left(y\right)\le F\left(a\right)$$
32	3 31	nfralw	$$⊢Ⅎx\forall y\in XF\left(y\right)\le F\left(a\right)$$
33		nfv	$$⊢Ⅎa\forall y\in XF\left(y\right)\le F\left(x\right)$$
34		fveq2	$$⊢a=x\to F\left(a\right)=F\left(x\right)$$
35	34	breq2d	$$⊢a=x\to \left(F\left(y\right)\le F\left(a\right)\leftrightarrow F\left(y\right)\le F\left(x\right)\right)$$
36	35	ralbidv	$$⊢a=x\to \left(\forall y\in XF\left(y\right)\le F\left(a\right)\leftrightarrow \forall y\in XF\left(y\right)\le F\left(x\right)\right)$$
37	25 3 32 33 36	cbvrexfw	$$⊢\exists a\in X\forall y\in XF\left(y\right)\le F\left(a\right)\leftrightarrow \exists x\in X\forall y\in XF\left(y\right)\le F\left(x\right)$$
38	24 37	bitri	$$⊢\exists a\in X\forall b\in XF\left(b\right)\le F\left(a\right)\leftrightarrow \exists x\in X\forall y\in XF\left(y\right)\le F\left(x\right)$$
39	12 38	sylib	$$⊢\phi \to \exists x\in X\forall y\in XF\left(y\right)\le F\left(x\right)$$