fvineqsneu

Description: A theorem about functions where the image of every point intersects the domain only at that point. (Contributed by ML, 27-Mar-2021)

		Ref	Expression
	Assertion	fvineqsneu	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to \forall q \in A \exists! x \in ran F q \in x$

Proof

Step	Hyp	Ref	Expression
1		fnfvelrn	$⊢ (F Fn A \land o \in A) \to F (o) \in ran F$
2	1	ex	$⊢ F Fn A \to (o \in A \to F (o) \in ran F)$
3	2	adantr	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (o \in A \to F (o) \in ran F)$
4		fnrnfv	$⊢ F Fn A \to ran F = \{y \| \exists p \in A y = F (p)\}$
5	4	abeq2d	$⊢ F Fn A \to (y \in ran F \leftrightarrow \exists p \in A y = F (p))$
6	5	adantr	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (y \in ran F \leftrightarrow \exists p \in A y = F (p))$
7		nfv	$⊢ Ⅎ p F Fn A$
8		nfra1	$⊢ Ⅎ p \forall p \in A F (p) \cap A = \{p\}$
9	7 8	nfan	$⊢ Ⅎ p (F Fn A \land \forall p \in A F (p) \cap A = \{p\})$
10		nfv	$⊢ Ⅎ p \forall o \in A (o \in y \leftrightarrow y = F (o))$
11		eleq2	$⊢ y = F (p) \to (o \in y \leftrightarrow o \in F (p))$
12		elin	$⊢ o \in (F (p) \cap A) \leftrightarrow (o \in F (p) \land o \in A)$
13	12	rbaib	$⊢ o \in A \to (o \in (F (p) \cap A) \leftrightarrow o \in F (p))$
14	13	ad2antll	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land o \in A)) \to (o \in (F (p) \cap A) \leftrightarrow o \in F (p))$
15		rsp	$⊢ \forall p \in A F (p) \cap A = \{p\} \to (p \in A \to F (p) \cap A = \{p\})$
16		eleq2	$⊢ F (p) \cap A = \{p\} \to (o \in (F (p) \cap A) \leftrightarrow o \in \{p\})$
17		velsn	$⊢ o \in \{p\} \leftrightarrow o = p$
18		equcom	$⊢ o = p \leftrightarrow p = o$
19	17 18	bitri	$⊢ o \in \{p\} \leftrightarrow p = o$
20	16 19	bitrdi	$⊢ F (p) \cap A = \{p\} \to (o \in (F (p) \cap A) \leftrightarrow p = o)$
21	15 20	syl6	$⊢ \forall p \in A F (p) \cap A = \{p\} \to (p \in A \to (o \in (F (p) \cap A) \leftrightarrow p = o))$
22	21	adantl	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (p \in A \to (o \in (F (p) \cap A) \leftrightarrow p = o))$
23	22	adantrd	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to ((p \in A \land o \in A) \to (o \in (F (p) \cap A) \leftrightarrow p = o))$
24	23	imp	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land o \in A)) \to (o \in (F (p) \cap A) \leftrightarrow p = o)$
25	14 24	bitr3d	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land o \in A)) \to (o \in F (p) \leftrightarrow p = o)$
26	11 25	sylan9bbr	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land o \in A)) \land y = F (p)) \to (o \in y \leftrightarrow p = o)$
27	26	ex	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land o \in A)) \to (y = F (p) \to (o \in y \leftrightarrow p = o))$
28	27	anass1rs	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land o \in A) \land p \in A) \to (y = F (p) \to (o \in y \leftrightarrow p = o))$
29	28	impr	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land o \in A) \land (p \in A \land y = F (p))) \to (o \in y \leftrightarrow p = o)$
30	29	an32s	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land y = F (p))) \land o \in A) \to (o \in y \leftrightarrow p = o)$
31		eqeq1	$⊢ y = F (p) \to (y = F (o) \leftrightarrow F (p) = F (o))$
32		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
33		fvineqsnf1	$⊢ (F : A ⟶ ran F \land \forall p \in A F (p) \cap A = \{p\}) \to F : A \underset{1-1}{⟶} ran F$
34	32 33	sylanb	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to F : A \underset{1-1}{⟶} ran F$
35		dff13	$⊢ F : A \underset{1-1}{⟶} ran F \leftrightarrow (F : A ⟶ ran F \land \forall p \in A \forall o \in A (F (p) = F (o) \to p = o))$
36	34 35	sylib	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (F : A ⟶ ran F \land \forall p \in A \forall o \in A (F (p) = F (o) \to p = o))$
37	36	simprd	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to \forall p \in A \forall o \in A (F (p) = F (o) \to p = o)$
38		rsp	$⊢ \forall p \in A \forall o \in A (F (p) = F (o) \to p = o) \to (p \in A \to \forall o \in A (F (p) = F (o) \to p = o))$
39	37 38	syl	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (p \in A \to \forall o \in A (F (p) = F (o) \to p = o))$
40		rsp	$⊢ \forall o \in A (F (p) = F (o) \to p = o) \to (o \in A \to (F (p) = F (o) \to p = o))$
41	39 40	syl6	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (p \in A \to (o \in A \to (F (p) = F (o) \to p = o)))$
42	41	imp32	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land o \in A)) \to (F (p) = F (o) \to p = o)$
43		fveq2	$⊢ p = o \to F (p) = F (o)$
44	42 43	impbid1	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land o \in A)) \to (F (p) = F (o) \leftrightarrow p = o)$
45	31 44	sylan9bbr	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land o \in A)) \land y = F (p)) \to (y = F (o) \leftrightarrow p = o)$
46	45	ex	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land o \in A)) \to (y = F (p) \to (y = F (o) \leftrightarrow p = o))$
47	46	anass1rs	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land o \in A) \land p \in A) \to (y = F (p) \to (y = F (o) \leftrightarrow p = o))$
48	47	impr	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land o \in A) \land (p \in A \land y = F (p))) \to (y = F (o) \leftrightarrow p = o)$
49	48	an32s	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land y = F (p))) \land o \in A) \to (y = F (o) \leftrightarrow p = o)$
50	30 49	bitr4d	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land y = F (p))) \land o \in A) \to (o \in y \leftrightarrow y = F (o))$
51	50	ex	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land y = F (p))) \to (o \in A \to (o \in y \leftrightarrow y = F (o)))$
52	51	ralrimiv	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (p \in A \land y = F (p))) \to \forall o \in A (o \in y \leftrightarrow y = F (o))$
53	52	exp32	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (p \in A \to (y = F (p) \to \forall o \in A (o \in y \leftrightarrow y = F (o))))$
54	9 10 53	rexlimd	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (\exists p \in A y = F (p) \to \forall o \in A (o \in y \leftrightarrow y = F (o)))$
55	6 54	sylbid	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (y \in ran F \to \forall o \in A (o \in y \leftrightarrow y = F (o)))$
56		rsp	$⊢ \forall o \in A (o \in y \leftrightarrow y = F (o)) \to (o \in A \to (o \in y \leftrightarrow y = F (o)))$
57	55 56	syl6	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (y \in ran F \to (o \in A \to (o \in y \leftrightarrow y = F (o))))$
58	57	com23	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (o \in A \to (y \in ran F \to (o \in y \leftrightarrow y = F (o))))$
59	58	ralrimdv	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (o \in A \to \forall y \in ran F (o \in y \leftrightarrow y = F (o)))$
60		reu6i	$⊢ (F (o) \in ran F \land \forall y \in ran F (o \in y \leftrightarrow y = F (o))) \to \exists! y \in ran F o \in y$
61	60	ex	$⊢ F (o) \in ran F \to (\forall y \in ran F (o \in y \leftrightarrow y = F (o)) \to \exists! y \in ran F o \in y)$
62	3 59 61	syl6c	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (o \in A \to \exists! y \in ran F o \in y)$
63	62	ralrimiv	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to \forall o \in A \exists! y \in ran F o \in y$
64		nfv	$⊢ Ⅎ x q = o$
65		nfv	$⊢ Ⅎ y q = o$
66		nfvd	$⊢ q = o \to Ⅎ y q \in x$
67		nfvd	$⊢ q = o \to Ⅎ x o \in y$
68		eleq12	$⊢ (q = o \land x = y) \to (q \in x \leftrightarrow o \in y)$
69	68	ex	$⊢ q = o \to (x = y \to (q \in x \leftrightarrow o \in y))$
70	64 65 66 67 69	cbvreud	$⊢ q = o \to (\exists! x \in ran F q \in x \leftrightarrow \exists! y \in ran F o \in y)$
71	70	cbvralvw	$⊢ \forall q \in A \exists! x \in ran F q \in x \leftrightarrow \forall o \in A \exists! y \in ran F o \in y$
72	63 71	sylibr	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to \forall q \in A \exists! x \in ran F q \in x$

Metamath Proof Explorer

Theorem fvineqsneu

Proof