Theorem evth2f

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

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

Proof

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