Theorem indexfi

Description: If for every element of a finite indexing set A there exists a corresponding element of another set B , then there exists a finite subset of B consisting only of those elements which are indexed by A . Proven without the Axiom of Choice, unlike indexdom . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Assertion	indexfi	$$⊢\left(A\in \mathrm{Fin}\wedge B\in M\wedge \forall x\in A\exists y\in B\phi \right)\to \exists c\in \mathrm{Fin}\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎz\phi$$
2		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
3		sbceq1a	$$⊢y=z\to \left(\phi \leftrightarrow \underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right)$$
4	1 2 3	cbvrexw	$$⊢\exists y\in B\phi \leftrightarrow \exists z\in B\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
5	4	ralbii	$$⊢\forall x\in A\exists y\in B\phi \leftrightarrow \forall x\in A\exists z\in B\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
6		dfsbcq	$$⊢z=f\left(x\right)\to \left(\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)$$
7	6	ac6sfi	$$⊢\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists z\in B\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)$$
8	5 7	sylan2b	$$⊢\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)$$
9		simpll	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to A\in \mathrm{Fin}$$
10		ffn	$$⊢f:A⟶B\to fFnA$$
11	10	ad2antrl	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to fFnA$$
12		dffn4	$$⊢fFnA\leftrightarrow f:A\underset{onto}{⟶}\mathrm{ran}f$$
13	11 12	sylib	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to f:A\underset{onto}{⟶}\mathrm{ran}f$$
14		fofi	$$⊢\left(A\in \mathrm{Fin}\wedge f:A\underset{onto}{⟶}\mathrm{ran}f\right)\to \mathrm{ran}f\in \mathrm{Fin}$$
15	9 13 14	syl2anc	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \mathrm{ran}f\in \mathrm{Fin}$$
16		frn	$$⊢f:A⟶B\to \mathrm{ran}f\subseteq B$$
17	16	ad2antrl	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \mathrm{ran}f\subseteq B$$
18		fnfvelrn	$$⊢\left(fFnA\wedge x\in A\right)\to f\left(x\right)\in \mathrm{ran}f$$
19	10 18	sylan	$$⊢\left(f:A⟶B\wedge x\in A\right)\to f\left(x\right)\in \mathrm{ran}f$$
20		rspesbca	$$⊢\left(f\left(x\right)\in \mathrm{ran}f\wedge \underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\to \exists y\in \mathrm{ran}f\phi$$
21	20	ex	$$⊢f\left(x\right)\in \mathrm{ran}f\to \left(\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \to \exists y\in \mathrm{ran}f\phi \right)$$
22	19 21	syl	$$⊢\left(f:A⟶B\wedge x\in A\right)\to \left(\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \to \exists y\in \mathrm{ran}f\phi \right)$$
23	22	ralimdva	$$⊢f:A⟶B\to \left(\forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \to \forall x\in A\exists y\in \mathrm{ran}f\phi \right)$$
24	23	imp	$$⊢\left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\to \forall x\in A\exists y\in \mathrm{ran}f\phi$$
25	24	adantl	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \forall x\in A\exists y\in \mathrm{ran}f\phi$$
26		simpr	$$⊢\left(\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\wedge w\in A\right)\to w\in A$$
27		simprr	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi$$
28		nfv	$$⊢Ⅎw\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi$$
29		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi$$
30		fveq2	$$⊢x=w\to f\left(x\right)=f\left(w\right)$$
31	30	sbceq1d	$$⊢x=w\to \left(\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
32		sbceq1a	$$⊢x=w\to \left(\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
33	31 32	bitrd	$$⊢x=w\to \left(\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
34	28 29 33	cbvralw	$$⊢\forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \forall w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi$$
35	27 34	sylib	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \forall w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi$$
36	35	r19.21bi	$$⊢\left(\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\wedge w\in A\right)\to \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi$$
37		rspesbca	$$⊢\left(w\in A\wedge \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi \right)\to \exists x\in A\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi$$
38	26 36 37	syl2anc	$$⊢\left(\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\wedge w\in A\right)\to \exists x\in A\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi$$
39	38	ralrimiva	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \forall w\in A\exists x\in A\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi$$
40		dfsbcq	$$⊢z=f\left(w\right)\to \left(\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
41	40	rexbidv	$$⊢z=f\left(w\right)\to \left(\exists x\in A\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \exists x\in A\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
42	41	ralrn	$$⊢fFnA\to \left(\forall z\in \mathrm{ran}f\exists x\in A\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \forall w\in A\exists x\in A\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
43	11 42	syl	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \left(\forall z\in \mathrm{ran}f\exists x\in A\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \forall w\in A\exists x\in A\underset{\dot{}}{[}f\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
44	39 43	mpbird	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \forall z\in \mathrm{ran}f\exists x\in A\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
45		nfv	$$⊢Ⅎz\exists x\in A\phi$$
46		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
47	46 2	nfrex	$$⊢Ⅎy\exists x\in A\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
48	3	rexbidv	$$⊢y=z\to \left(\exists x\in A\phi \leftrightarrow \exists x\in A\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right)$$
49	45 47 48	cbvralw	$$⊢\forall y\in \mathrm{ran}f\exists x\in A\phi \leftrightarrow \forall z\in \mathrm{ran}f\exists x\in A\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
50	44 49	sylibr	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \forall y\in \mathrm{ran}f\exists x\in A\phi$$
51		sseq1	$$⊢c=\mathrm{ran}f\to \left(c\subseteq B\leftrightarrow \mathrm{ran}f\subseteq B\right)$$
52		rexeq	$$⊢c=\mathrm{ran}f\to \left(\exists y\in c\phi \leftrightarrow \exists y\in \mathrm{ran}f\phi \right)$$
53	52	ralbidv	$$⊢c=\mathrm{ran}f\to \left(\forall x\in A\exists y\in c\phi \leftrightarrow \forall x\in A\exists y\in \mathrm{ran}f\phi \right)$$
54		raleq	$$⊢c=\mathrm{ran}f\to \left(\forall y\in c\exists x\in A\phi \leftrightarrow \forall y\in \mathrm{ran}f\exists x\in A\phi \right)$$
55	51 53 54	3anbi123d	$$⊢c=\mathrm{ran}f\to \left(\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)\leftrightarrow \left(\mathrm{ran}f\subseteq B\wedge \forall x\in A\exists y\in \mathrm{ran}f\phi \wedge \forall y\in \mathrm{ran}f\exists x\in A\phi \right)\right)$$
56	55	rspcev	$$⊢\left(\mathrm{ran}f\in \mathrm{Fin}\wedge \left(\mathrm{ran}f\subseteq B\wedge \forall x\in A\exists y\in \mathrm{ran}f\phi \wedge \forall y\in \mathrm{ran}f\exists x\in A\phi \right)\right)\to \exists c\in \mathrm{Fin}\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)$$
57	15 17 25 50 56	syl13anc	$$⊢\left(\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(f:A⟶B\wedge \forall x\in A\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \right)\right)\to \exists c\in \mathrm{Fin}\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)$$
58	8 57	exlimddv	$$⊢\left(A\in \mathrm{Fin}\wedge \forall x\in A\exists y\in B\phi \right)\to \exists c\in \mathrm{Fin}\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)$$
59	58	3adant2	$$⊢\left(A\in \mathrm{Fin}\wedge B\in M\wedge \forall x\in A\exists y\in B\phi \right)\to \exists c\in \mathrm{Fin}\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)$$