fvineqsneq

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

		Ref	Expression
	Assertion	fvineqsneq	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (Z \subseteq ran F \land A \subseteq ⋃ Z)) \to Z = ran F$

Proof

Step	Hyp	Ref	Expression
1		pssnel	$⊢ Z \subset ran F \to \exists x (x \in ran F \land \neg x \in Z)$
2	1	adantl	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists x (x \in ran F \land \neg x \in Z)$
3		df-rex	$⊢ \exists x \in ran F \neg x \in Z \leftrightarrow \exists x (x \in ran F \land \neg x \in Z)$
4	2 3	sylibr	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists x \in ran F \neg x \in Z$
5		fnrnfv	$⊢ F Fn A \to ran F = \{x \| \exists p \in A x = F (p)\}$
6	5	eqabrd	$⊢ F Fn A \to (x \in ran F \leftrightarrow \exists p \in A x = F (p))$
7	6	biimpd	$⊢ F Fn A \to (x \in ran F \to \exists p \in A x = F (p))$
8	7	ralrimiv	$⊢ F Fn A \to \forall x \in ran F \exists p \in A x = F (p)$
9	8	adantr	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to \forall x \in ran F \exists p \in A x = F (p)$
10	9	adantr	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \forall x \in ran F \exists p \in A x = F (p)$
11		r19.29r	$⊢ (\exists x \in ran F \neg x \in Z \land \forall x \in ran F \exists p \in A x = F (p)) \to \exists x \in ran F (\neg x \in Z \land \exists p \in A x = F (p))$
12	4 10 11	syl2anc	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists x \in ran F (\neg x \in Z \land \exists p \in A x = F (p))$
13		nfra1	$⊢ Ⅎ p \forall p \in A F (p) \cap A = \{p\}$
14		rsp	$⊢ \forall p \in A F (p) \cap A = \{p\} \to (p \in A \to F (p) \cap A = \{p\})$
15		vsnid	$⊢ p \in \{p\}$
16		eleq2	$⊢ F (p) \cap A = \{p\} \to (p \in (F (p) \cap A) \leftrightarrow p \in \{p\})$
17	15 16	mpbiri	$⊢ F (p) \cap A = \{p\} \to p \in (F (p) \cap A)$
18	17	elin1d	$⊢ F (p) \cap A = \{p\} \to p \in F (p)$
19	14 18	syl6	$⊢ \forall p \in A F (p) \cap A = \{p\} \to (p \in A \to p \in F (p))$
20	19	adantr	$⊢ (\forall p \in A F (p) \cap A = \{p\} \land x = F (p)) \to (p \in A \to p \in F (p))$
21		eleq2	$⊢ x = F (p) \to (p \in x \leftrightarrow p \in F (p))$
22	21	adantl	$⊢ (\forall p \in A F (p) \cap A = \{p\} \land x = F (p)) \to (p \in x \leftrightarrow p \in F (p))$
23	20 22	sylibrd	$⊢ (\forall p \in A F (p) \cap A = \{p\} \land x = F (p)) \to (p \in A \to p \in x)$
24	23	ex	$⊢ \forall p \in A F (p) \cap A = \{p\} \to (x = F (p) \to (p \in A \to p \in x))$
25	24	com23	$⊢ \forall p \in A F (p) \cap A = \{p\} \to (p \in A \to (x = F (p) \to p \in x))$
26	13 25	reximdai	$⊢ \forall p \in A F (p) \cap A = \{p\} \to (\exists p \in A x = F (p) \to \exists p \in A p \in x)$
27	26	adantl	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (\exists p \in A x = F (p) \to \exists p \in A p \in x)$
28	27	adantr	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to (\exists p \in A x = F (p) \to \exists p \in A p \in x)$
29	28	anim2d	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to ((\neg x \in Z \land \exists p \in A x = F (p)) \to (\neg x \in Z \land \exists p \in A p \in x))$
30	29	reximdv	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to (\exists x \in ran F (\neg x \in Z \land \exists p \in A x = F (p)) \to \exists x \in ran F (\neg x \in Z \land \exists p \in A p \in x))$
31	12 30	mpd	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists x \in ran F (\neg x \in Z \land \exists p \in A p \in x)$
32		ancom	$⊢ (\neg x \in Z \land \exists p \in A p \in x) \leftrightarrow (\exists p \in A p \in x \land \neg x \in Z)$
33		r19.41v	$⊢ \exists p \in A (p \in x \land \neg x \in Z) \leftrightarrow (\exists p \in A p \in x \land \neg x \in Z)$
34	32 33	bitr4i	$⊢ (\neg x \in Z \land \exists p \in A p \in x) \leftrightarrow \exists p \in A (p \in x \land \neg x \in Z)$
35	34	rexbii	$⊢ \exists x \in ran F (\neg x \in Z \land \exists p \in A p \in x) \leftrightarrow \exists x \in ran F \exists p \in A (p \in x \land \neg x \in Z)$
36	31 35	sylib	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists x \in ran F \exists p \in A (p \in x \land \neg x \in Z)$
37		rexcom	$⊢ \exists p \in A \exists x \in ran F (p \in x \land \neg x \in Z) \leftrightarrow \exists x \in ran F \exists p \in A (p \in x \land \neg x \in Z)$
38	36 37	sylibr	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists p \in A \exists x \in ran F (p \in x \land \neg x \in Z)$
39		nfre1	$⊢ Ⅎ x \exists x \in ran F (p \in x \land \neg x \in Z)$
40	39	19.3	$⊢ \forall x \exists x \in ran F (p \in x \land \neg x \in Z) \leftrightarrow \exists x \in ran F (p \in x \land \neg x \in Z)$
41		alral	$⊢ \forall x \exists x \in ran F (p \in x \land \neg x \in Z) \to \forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z)$
42	40 41	sylbir	$⊢ \exists x \in ran F (p \in x \land \neg x \in Z) \to \forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z)$
43	42	reximi	$⊢ \exists p \in A \exists x \in ran F (p \in x \land \neg x \in Z) \to \exists p \in A \forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z)$
44	38 43	syl	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists p \in A \forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z)$
45		nfv	$⊢ Ⅎ p F Fn A$
46	45 13	nfan	$⊢ Ⅎ p (F Fn A \land \forall p \in A F (p) \cap A = \{p\})$
47		nfv	$⊢ Ⅎ p Z \subset ran F$
48	46 47	nfan	$⊢ Ⅎ p ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F)$
49		nfv	$⊢ Ⅎ x (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land p \in A)$
50		fvineqsneu	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to \forall p \in A \exists! x \in ran F p \in x$
51	50	adantr	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \forall p \in A \exists! x \in ran F p \in x$
52		rsp	$⊢ \forall p \in A \exists! x \in ran F p \in x \to (p \in A \to \exists! x \in ran F p \in x)$
53	51 52	syl	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to (p \in A \to \exists! x \in ran F p \in x)$
54	53	adantrd	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to ((p \in A \land x \in ran F) \to \exists! x \in ran F p \in x)$
55	54	imp	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land (p \in A \land x \in ran F)) \to \exists! x \in ran F p \in x$
56		reupick3	$⊢ (\exists! x \in ran F p \in x \land \exists x \in ran F (p \in x \land \neg x \in Z) \land x \in ran F) \to (p \in x \to \neg x \in Z)$
57	56	3expa	$⊢ ((\exists! x \in ran F p \in x \land \exists x \in ran F (p \in x \land \neg x \in Z)) \land x \in ran F) \to (p \in x \to \neg x \in Z)$
58	57	expcom	$⊢ x \in ran F \to ((\exists! x \in ran F p \in x \land \exists x \in ran F (p \in x \land \neg x \in Z)) \to (p \in x \to \neg x \in Z))$
59	58	adantl	$⊢ (p \in A \land x \in ran F) \to ((\exists! x \in ran F p \in x \land \exists x \in ran F (p \in x \land \neg x \in Z)) \to (p \in x \to \neg x \in Z))$
60	59	adantl	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land (p \in A \land x \in ran F)) \to ((\exists! x \in ran F p \in x \land \exists x \in ran F (p \in x \land \neg x \in Z)) \to (p \in x \to \neg x \in Z))$
61	55 60	mpand	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land (p \in A \land x \in ran F)) \to (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z))$
62	61	expr	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land p \in A) \to (x \in ran F \to (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z)))$
63	49 62	ralrimi	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land p \in A) \to \forall x \in ran F (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z))$
64	63	ex	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to (p \in A \to \forall x \in ran F (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z)))$
65	48 64	ralrimi	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \forall p \in A \forall x \in ran F (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z))$
66		r19.29r	$⊢ (\exists p \in A \forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z) \land \forall p \in A \forall x \in ran F (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z))) \to \exists p \in A (\forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z) \land \forall x \in ran F (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z)))$
67	44 65 66	syl2anc	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists p \in A (\forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z) \land \forall x \in ran F (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z)))$
68		ralim	$⊢ \forall x \in ran F (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z)) \to (\forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z) \to \forall x \in ran F (p \in x \to \neg x \in Z))$
69	68	impcom	$⊢ (\forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z) \land \forall x \in ran F (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z))) \to \forall x \in ran F (p \in x \to \neg x \in Z)$
70	69	reximi	$⊢ \exists p \in A (\forall x \in ran F \exists x \in ran F (p \in x \land \neg x \in Z) \land \forall x \in ran F (\exists x \in ran F (p \in x \land \neg x \in Z) \to (p \in x \to \neg x \in Z))) \to \exists p \in A \forall x \in ran F (p \in x \to \neg x \in Z)$
71	67 70	syl	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists p \in A \forall x \in ran F (p \in x \to \neg x \in Z)$
72		con2b	$⊢ (p \in x \to \neg x \in Z) \leftrightarrow (x \in Z \to \neg p \in x)$
73	72	ralbii	$⊢ \forall x \in ran F (p \in x \to \neg x \in Z) \leftrightarrow \forall x \in ran F (x \in Z \to \neg p \in x)$
74		df-ral	$⊢ \forall x \in ran F (x \in Z \to \neg p \in x) \leftrightarrow \forall x (x \in ran F \to (x \in Z \to \neg p \in x))$
75		bi2.04	$⊢ (x \in ran F \to (x \in Z \to \neg p \in x)) \leftrightarrow (x \in Z \to (x \in ran F \to \neg p \in x))$
76	75	albii	$⊢ \forall x (x \in ran F \to (x \in Z \to \neg p \in x)) \leftrightarrow \forall x (x \in Z \to (x \in ran F \to \neg p \in x))$
77	73 74 76	3bitri	$⊢ \forall x \in ran F (p \in x \to \neg x \in Z) \leftrightarrow \forall x (x \in Z \to (x \in ran F \to \neg p \in x))$
78	77	a1i	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to (\forall x \in ran F (p \in x \to \neg x \in Z) \leftrightarrow \forall x (x \in Z \to (x \in ran F \to \neg p \in x)))$
79	48 78	rexbid	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to (\exists p \in A \forall x \in ran F (p \in x \to \neg x \in Z) \leftrightarrow \exists p \in A \forall x (x \in Z \to (x \in ran F \to \neg p \in x)))$
80	71 79	mpbid	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists p \in A \forall x (x \in Z \to (x \in ran F \to \neg p \in x))$
81		nfv	$⊢ Ⅎ x ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F)$
82		nfa1	$⊢ Ⅎ x \forall x (x \in Z \to (x \in ran F \to \neg p \in x))$
83	81 82	nfan	$⊢ Ⅎ x (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land \forall x (x \in Z \to (x \in ran F \to \neg p \in x)))$
84		pssss	$⊢ Z \subset ran F \to Z \subseteq ran F$
85		df-ss	$⊢ Z \subseteq ran F \leftrightarrow \forall x (x \in Z \to x \in ran F)$
86	84 85	sylib	$⊢ Z \subset ran F \to \forall x (x \in Z \to x \in ran F)$
87	86	adantl	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \forall x (x \in Z \to x \in ran F)$
88		df-ral	$⊢ \forall x \in Z x \in ran F \leftrightarrow \forall x (x \in Z \to x \in ran F)$
89	87 88	sylibr	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \forall x \in Z x \in ran F$
90	89	adantr	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land \forall x (x \in Z \to (x \in ran F \to \neg p \in x))) \to \forall x \in Z x \in ran F$
91		rsp	$⊢ \forall x \in Z x \in ran F \to (x \in Z \to x \in ran F)$
92	90 91	syl	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land \forall x (x \in Z \to (x \in ran F \to \neg p \in x))) \to (x \in Z \to x \in ran F)$
93		df-ral	$⊢ \forall x \in Z (x \in ran F \to \neg p \in x) \leftrightarrow \forall x (x \in Z \to (x \in ran F \to \neg p \in x))$
94	93	bilanri	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land \forall x (x \in Z \to (x \in ran F \to \neg p \in x))) \to \forall x \in Z (x \in ran F \to \neg p \in x)$
95		rsp	$⊢ \forall x \in Z (x \in ran F \to \neg p \in x) \to (x \in Z \to (x \in ran F \to \neg p \in x))$
96	94 95	syl	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land \forall x (x \in Z \to (x \in ran F \to \neg p \in x))) \to (x \in Z \to (x \in ran F \to \neg p \in x))$
97	92 96	mpdd	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land \forall x (x \in Z \to (x \in ran F \to \neg p \in x))) \to (x \in Z \to \neg p \in x)$
98	83 97	ralrimi	$⊢ (((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \land \forall x (x \in Z \to (x \in ran F \to \neg p \in x))) \to \forall x \in Z \neg p \in x$
99	98	ex	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to (\forall x (x \in Z \to (x \in ran F \to \neg p \in x)) \to \forall x \in Z \neg p \in x)$
100	99	a1d	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to (p \in A \to (\forall x (x \in Z \to (x \in ran F \to \neg p \in x)) \to \forall x \in Z \neg p \in x))$
101	48 100	reximdai	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to (\exists p \in A \forall x (x \in Z \to (x \in ran F \to \neg p \in x)) \to \exists p \in A \forall x \in Z \neg p \in x)$
102	80 101	mpd	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists p \in A \forall x \in Z \neg p \in x$
103		ralnex	$⊢ \forall x \in Z \neg p \in x \leftrightarrow \neg \exists x \in Z p \in x$
104	103	rexbii	$⊢ \exists p \in A \forall x \in Z \neg p \in x \leftrightarrow \exists p \in A \neg \exists x \in Z p \in x$
105	102 104	sylib	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists p \in A \neg \exists x \in Z p \in x$
106		eluni2	$⊢ p \in ⋃ Z \leftrightarrow \exists x \in Z p \in x$
107	106	notbii	$⊢ \neg p \in ⋃ Z \leftrightarrow \neg \exists x \in Z p \in x$
108	107	rexbii	$⊢ \exists p \in A \neg p \in ⋃ Z \leftrightarrow \exists p \in A \neg \exists x \in Z p \in x$
109	105 108	sylibr	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \exists p \in A \neg p \in ⋃ Z$
110		dfss3	$⊢ A \subseteq ⋃ Z \leftrightarrow \forall p \in A p \in ⋃ Z$
111		dfral2	$⊢ \forall p \in A p \in ⋃ Z \leftrightarrow \neg \exists p \in A \neg p \in ⋃ Z$
112	110 111	bitri	$⊢ A \subseteq ⋃ Z \leftrightarrow \neg \exists p \in A \neg p \in ⋃ Z$
113	112	con2bii2	$⊢ \neg A \subseteq ⋃ Z \leftrightarrow \exists p \in A \neg p \in ⋃ Z$
114	109 113	sylibr	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land Z \subset ran F) \to \neg A \subseteq ⋃ Z$
115	114	ex	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (Z \subset ran F \to \neg A \subseteq ⋃ Z)$
116	115	con2d	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (A \subseteq ⋃ Z \to \neg Z \subset ran F)$
117		npss	$⊢ \neg Z \subset ran F \leftrightarrow (Z \subseteq ran F \to Z = ran F)$
118	116 117	imbitrdi	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (A \subseteq ⋃ Z \to (Z \subseteq ran F \to Z = ran F))$
119	118	com23	$⊢ (F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \to (Z \subseteq ran F \to (A \subseteq ⋃ Z \to Z = ran F))$
120	119	imp32	$⊢ ((F Fn A \land \forall p \in A F (p) \cap A = \{p\}) \land (Z \subseteq ran F \land A \subseteq ⋃ Z)) \to Z = ran F$

Metamath Proof Explorer

Theorem fvineqsneq

Proof