Theorem afv2orxorb

Description: If a set is in the range of a function, the alternate function value at a class A equals this set or is not in the range of the function iff the alternate function value at the class A either equals this set or is not in the range of the function. If B e/ ran F , both disjuncts of the exclusive or can be true: ( F '''' A ) = B -> ( F '''' A ) e/ ran F . (Contributed by AV, 11-Sep-2022)

	Ref	Expression
Assertion	afv2orxorb	$$⊢B\in \mathrm{ran}F\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\leftrightarrow \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B⊻\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢B=\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\to \left(B\in \mathrm{ran}F\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F\right)$$
2	1	eqcoms	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \left(B\in \mathrm{ran}F\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F\right)$$
3	2	biimpa	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\wedge B\in \mathrm{ran}F\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F$$
4		nnel	$$⊢\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F$$
5	3 4	sylibr	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\wedge B\in \mathrm{ran}F\right)\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F$$
6	5	a1d	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\wedge B\in \mathrm{ran}F\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$
7		simpl	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\wedge B\in \mathrm{ran}F\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B$$
8	7	a1d	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\wedge B\in \mathrm{ran}F\right)\to \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)$$
9	6 8	jca	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\wedge B\in \mathrm{ran}F\right)\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\wedge \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)\right)$$
10	9	ex	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \left(B\in \mathrm{ran}F\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\wedge \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)\right)\right)$$
11		eleq1	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F\leftrightarrow B\in \mathrm{ran}F\right)$$
12	11	anbi2d	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\wedge \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F\right)\leftrightarrow \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\wedge B\in \mathrm{ran}F\right)\right)$$
13		pm2.24nel	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$
14	13	impcom	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\wedge \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{ran}F\right)\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F$$
15	12 14	syl6bir	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\wedge B\in \mathrm{ran}F\right)\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$
16	15	com12	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\wedge B\in \mathrm{ran}F\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$
17		pm2.24	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)$$
18	17	adantr	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\wedge B\in \mathrm{ran}F\right)\to \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)$$
19	16 18	jca	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\wedge B\in \mathrm{ran}F\right)\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\wedge \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)\right)$$
20	19	ex	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(B\in \mathrm{ran}F\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\wedge \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)\right)\right)$$
21	10 20	jaoi	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\to \left(B\in \mathrm{ran}F\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\wedge \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)\right)\right)$$
22	21	com12	$$⊢B\in \mathrm{ran}F\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\wedge \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)\right)\right)$$
23		df-xor	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B⊻\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\leftrightarrow \neg \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$
24		xor3	$$⊢\neg \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\leftrightarrow \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\leftrightarrow \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$
25		dfbi2	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\leftrightarrow \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\leftrightarrow \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\wedge \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)\right)$$
26	23 24 25	3bitri	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B⊻\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\leftrightarrow \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\to \neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\wedge \left(\neg \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\right)\right)$$
27	22 26	syl6ibr	$$⊢B\in \mathrm{ran}F\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B⊻\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\right)$$
28		xoror	$$⊢\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B⊻\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)$$
29	27 28	impbid1	$$⊢B\in \mathrm{ran}F\to \left(\left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B\vee \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\leftrightarrow \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=B⊻\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F\right)\right)$$