Theorem fvineqsnf1

Description: A theorem about functions where the image of every point intersects the domain only at that point. If J is a topology and A is a set with no limit points, then there exists an F such that this antecedent is true. See nlpfvineqsn for a proof of this fact. (Contributed by ML, 23-Mar-2021)

	Ref	Expression
Assertion	fvineqsnf1	$$⊢\left(F:A⟶J\wedge \forall p\in AF\left(p\right)\cap A=\left\{p\right\}\right)\to F:A\underset{1-1}{⟶}J$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢p=q\to F\left(p\right)=F\left(q\right)$$
2	1	ineq1d	$$⊢p=q\to F\left(p\right)\cap A=F\left(q\right)\cap A$$
3		sneq	$$⊢p=q\to \left\{p\right\}=\left\{q\right\}$$
4	2 3	eqeq12d	$$⊢p=q\to \left(F\left(p\right)\cap A=\left\{p\right\}\leftrightarrow F\left(q\right)\cap A=\left\{q\right\}\right)$$
5	4	cbvralvw	$$⊢\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\leftrightarrow \forall q\in AF\left(q\right)\cap A=\left\{q\right\}$$
6	5	biimpi	$$⊢\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\to \forall q\in AF\left(q\right)\cap A=\left\{q\right\}$$
7		ax-5	$$⊢\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\to \forall q\forall p\in AF\left(p\right)\cap A=\left\{p\right\}$$
8		alral	$$⊢\forall q\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\to \forall q\in A\forall p\in AF\left(p\right)\cap A=\left\{p\right\}$$
9		ralcom	$$⊢\forall q\in A\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\leftrightarrow \forall p\in A\forall q\in AF\left(p\right)\cap A=\left\{p\right\}$$
10	9	biimpi	$$⊢\forall q\in A\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\to \forall p\in A\forall q\in AF\left(p\right)\cap A=\left\{p\right\}$$
11	7 8 10	3syl	$$⊢\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\to \forall p\in A\forall q\in AF\left(p\right)\cap A=\left\{p\right\}$$
12		ax-5	$$⊢\forall q\in AF\left(q\right)\cap A=\left\{q\right\}\to \forall p\forall q\in AF\left(q\right)\cap A=\left\{q\right\}$$
13		alral	$$⊢\forall p\forall q\in AF\left(q\right)\cap A=\left\{q\right\}\to \forall p\in A\forall q\in AF\left(q\right)\cap A=\left\{q\right\}$$
14	12 13	syl	$$⊢\forall q\in AF\left(q\right)\cap A=\left\{q\right\}\to \forall p\in A\forall q\in AF\left(q\right)\cap A=\left\{q\right\}$$
15	11 14	anim12i	$$⊢\left(\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\wedge \forall q\in AF\left(q\right)\cap A=\left\{q\right\}\right)\to \left(\forall p\in A\forall q\in AF\left(p\right)\cap A=\left\{p\right\}\wedge \forall p\in A\forall q\in AF\left(q\right)\cap A=\left\{q\right\}\right)$$
16	6 15	mpdan	$$⊢\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\to \left(\forall p\in A\forall q\in AF\left(p\right)\cap A=\left\{p\right\}\wedge \forall p\in A\forall q\in AF\left(q\right)\cap A=\left\{q\right\}\right)$$
17		r19.26-2	$$⊢\forall p\in A\forall q\in A\left(F\left(p\right)\cap A=\left\{p\right\}\wedge F\left(q\right)\cap A=\left\{q\right\}\right)\leftrightarrow \left(\forall p\in A\forall q\in AF\left(p\right)\cap A=\left\{p\right\}\wedge \forall p\in A\forall q\in AF\left(q\right)\cap A=\left\{q\right\}\right)$$
18	16 17	sylibr	$$⊢\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\to \forall p\in A\forall q\in A\left(F\left(p\right)\cap A=\left\{p\right\}\wedge F\left(q\right)\cap A=\left\{q\right\}\right)$$
19		ineq1	$$⊢F\left(p\right)=F\left(q\right)\to F\left(p\right)\cap A=F\left(q\right)\cap A$$
20		eqeq1	$$⊢F\left(p\right)\cap A=\left\{p\right\}\to \left(F\left(p\right)\cap A=F\left(q\right)\cap A\leftrightarrow \left\{p\right\}=F\left(q\right)\cap A\right)$$
21		eqcom	$$⊢\left\{p\right\}=F\left(q\right)\cap A\leftrightarrow F\left(q\right)\cap A=\left\{p\right\}$$
22	20 21	bitrdi	$$⊢F\left(p\right)\cap A=\left\{p\right\}\to \left(F\left(p\right)\cap A=F\left(q\right)\cap A\leftrightarrow F\left(q\right)\cap A=\left\{p\right\}\right)$$
23		eqeq1	$$⊢F\left(q\right)\cap A=\left\{q\right\}\to \left(F\left(q\right)\cap A=\left\{p\right\}\leftrightarrow \left\{q\right\}=\left\{p\right\}\right)$$
24		eqcom	$$⊢\left\{q\right\}=\left\{p\right\}\leftrightarrow \left\{p\right\}=\left\{q\right\}$$
25		vex	$$⊢p\in \mathrm{V}$$
26		sneqbg	$$⊢p\in \mathrm{V}\to \left(\left\{p\right\}=\left\{q\right\}\leftrightarrow p=q\right)$$
27	25 26	ax-mp	$$⊢\left\{p\right\}=\left\{q\right\}\leftrightarrow p=q$$
28	24 27	bitri	$$⊢\left\{q\right\}=\left\{p\right\}\leftrightarrow p=q$$
29	23 28	bitrdi	$$⊢F\left(q\right)\cap A=\left\{q\right\}\to \left(F\left(q\right)\cap A=\left\{p\right\}\leftrightarrow p=q\right)$$
30	22 29	sylan9bb	$$⊢\left(F\left(p\right)\cap A=\left\{p\right\}\wedge F\left(q\right)\cap A=\left\{q\right\}\right)\to \left(F\left(p\right)\cap A=F\left(q\right)\cap A\leftrightarrow p=q\right)$$
31	19 30	syl5ib	$$⊢\left(F\left(p\right)\cap A=\left\{p\right\}\wedge F\left(q\right)\cap A=\left\{q\right\}\right)\to \left(F\left(p\right)=F\left(q\right)\to p=q\right)$$
32	31	ralimi	$$⊢\forall q\in A\left(F\left(p\right)\cap A=\left\{p\right\}\wedge F\left(q\right)\cap A=\left\{q\right\}\right)\to \forall q\in A\left(F\left(p\right)=F\left(q\right)\to p=q\right)$$
33	32	ralimi	$$⊢\forall p\in A\forall q\in A\left(F\left(p\right)\cap A=\left\{p\right\}\wedge F\left(q\right)\cap A=\left\{q\right\}\right)\to \forall p\in A\forall q\in A\left(F\left(p\right)=F\left(q\right)\to p=q\right)$$
34	18 33	syl	$$⊢\forall p\in AF\left(p\right)\cap A=\left\{p\right\}\to \forall p\in A\forall q\in A\left(F\left(p\right)=F\left(q\right)\to p=q\right)$$
35	34	anim2i	$$⊢\left(F:A⟶J\wedge \forall p\in AF\left(p\right)\cap A=\left\{p\right\}\right)\to \left(F:A⟶J\wedge \forall p\in A\forall q\in A\left(F\left(p\right)=F\left(q\right)\to p=q\right)\right)$$
36		dff13	$$⊢F:A\underset{1-1}{⟶}J\leftrightarrow \left(F:A⟶J\wedge \forall p\in A\forall q\in A\left(F\left(p\right)=F\left(q\right)\to p=q\right)\right)$$
37	35 36	sylibr	$$⊢\left(F:A⟶J\wedge \forall p\in AF\left(p\right)\cap A=\left\{p\right\}\right)\to F:A\underset{1-1}{⟶}J$$