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	eqabrd	$⊢ 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		eleq2w2	$⊢ 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		eleq2w2	$⊢ 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		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))$
38	36 37	simpl2im	$⊢ (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))$
39		rsp	$⊢ \forall o \in A (F (p) = F (o) \to p = o) \to (o \in A \to (F (p) = F (o) \to p = o))$
40	38 39	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)))$
41	40	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)$
42		fveq2	$⊢ p = o \to F (p) = F (o)$
43	41 42	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)$
44	31 43	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)$
45	44	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))$
46	45	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))$
47	46	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)$
48	47	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)$
49	30 48	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))$
50	49	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)))$
51	50	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))$
52	51	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))))$
53	9 10 52	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)))$
54	6 53	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)))$
55		rsp	$⊢ \forall o \in A (o \in y \leftrightarrow y = F (o)) \to (o \in A \to (o \in y \leftrightarrow y = F (o)))$
56	54 55	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))))$
57	56	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))))$
58	57	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)))$
59		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$
60	59	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)$
61	3 58 60	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)$
62	61	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$
63		nfv	$⊢ Ⅎ x q = o$
64		nfv	$⊢ Ⅎ y q = o$
65		nfvd	$⊢ q = o \to Ⅎ y q \in x$
66		nfvd	$⊢ q = o \to Ⅎ x o \in y$
67		elequ12	$⊢ (q = o \land x = y) \to (q \in x \leftrightarrow o \in y)$
68	67	ex	$⊢ q = o \to (x = y \to (q \in x \leftrightarrow o \in y))$
69	63 64 65 66 68	cbvreud	$⊢ q = o \to (\exists! x \in ran F q \in x \leftrightarrow \exists! y \in ran F o \in y)$
70	69	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$
71	62 70	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