Theorem frege124d

Description: If F is a function, A is the successor of X , and B follows X in the transitive closure of F , then A and B are the same or B follows A in the transitive closure of F . Similar to Proposition 124 of Frege1879 p. 80. Compare with frege124 . (Contributed by RP, 16-Jul-2020)

	Ref	Expression
Hypotheses	frege124d.f	$$⊢\phi \to F\in \mathrm{V}$$
	frege124d.x	$$⊢\phi \to X\in \mathrm{dom}F$$
	frege124d.a	$$⊢\phi \to A=F\left(X\right)$$
	frege124d.xb	$$⊢\phi \to X\mathrm{t+}\left(F\right)B$$
	frege124d.fun	$$⊢\phi \to \mathrm{Fun}F$$
Assertion	frege124d	$$⊢\phi \to \left(A\mathrm{t+}\left(F\right)B\vee A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		frege124d.f	$$⊢\phi \to F\in \mathrm{V}$$
2		frege124d.x	$$⊢\phi \to X\in \mathrm{dom}F$$
3		frege124d.a	$$⊢\phi \to A=F\left(X\right)$$
4		frege124d.xb	$$⊢\phi \to X\mathrm{t+}\left(F\right)B$$
5		frege124d.fun	$$⊢\phi \to \mathrm{Fun}F$$
6	3	eqcomd	$$⊢\phi \to F\left(X\right)=A$$
7		funbrfvb	$$⊢\left(\mathrm{Fun}F\wedge X\in \mathrm{dom}F\right)\to \left(F\left(X\right)=A\leftrightarrow XFA\right)$$
8	5 2 7	syl2anc	$$⊢\phi \to \left(F\left(X\right)=A\leftrightarrow XFA\right)$$
9	6 8	mpbid	$$⊢\phi \to XFA$$
10		funeu	$$⊢\left(\mathrm{Fun}F\wedge XFA\right)\to \exists !aXFa$$
11	5 9 10	syl2anc	$$⊢\phi \to \exists !aXFa$$
12		fvex	$$⊢F\left(X\right)\in \mathrm{V}$$
13	3 12	eqeltrdi	$$⊢\phi \to A\in \mathrm{V}$$
14		sbcan	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\left(XFa\wedge \neg a\mathrm{t+}\left(F\right)B\right)\leftrightarrow \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}XFa\wedge \underset{\dot{}}{[}A/a\underset{\dot{}}{]}\neg a\mathrm{t+}\left(F\right)B\right)$$
15		sbcbr2g	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}XFa\leftrightarrow XF⦋A/a⦌a\right)$$
16		csbvarg	$$⊢A\in \mathrm{V}\to ⦋A/a⦌a=A$$
17	16	breq2d	$$⊢A\in \mathrm{V}\to \left(XF⦋A/a⦌a\leftrightarrow XFA\right)$$
18	15 17	bitrd	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}XFa\leftrightarrow XFA\right)$$
19		sbcng	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\neg a\mathrm{t+}\left(F\right)B\leftrightarrow \neg \underset{\dot{}}{[}A/a\underset{\dot{}}{]}a\mathrm{t+}\left(F\right)B\right)$$
20		sbcbr1g	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}a\mathrm{t+}\left(F\right)B\leftrightarrow ⦋A/a⦌a\mathrm{t+}\left(F\right)B\right)$$
21	16	breq1d	$$⊢A\in \mathrm{V}\to \left(⦋A/a⦌a\mathrm{t+}\left(F\right)B\leftrightarrow A\mathrm{t+}\left(F\right)B\right)$$
22	20 21	bitrd	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}a\mathrm{t+}\left(F\right)B\leftrightarrow A\mathrm{t+}\left(F\right)B\right)$$
23	22	notbid	$$⊢A\in \mathrm{V}\to \left(\neg \underset{\dot{}}{[}A/a\underset{\dot{}}{]}a\mathrm{t+}\left(F\right)B\leftrightarrow \neg A\mathrm{t+}\left(F\right)B\right)$$
24	19 23	bitrd	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\neg a\mathrm{t+}\left(F\right)B\leftrightarrow \neg A\mathrm{t+}\left(F\right)B\right)$$
25	18 24	anbi12d	$$⊢A\in \mathrm{V}\to \left(\left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}XFa\wedge \underset{\dot{}}{[}A/a\underset{\dot{}}{]}\neg a\mathrm{t+}\left(F\right)B\right)\leftrightarrow \left(XFA\wedge \neg A\mathrm{t+}\left(F\right)B\right)\right)$$
26	14 25	syl5bb	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\left(XFa\wedge \neg a\mathrm{t+}\left(F\right)B\right)\leftrightarrow \left(XFA\wedge \neg A\mathrm{t+}\left(F\right)B\right)\right)$$
27	13 26	syl	$$⊢\phi \to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\left(XFa\wedge \neg a\mathrm{t+}\left(F\right)B\right)\leftrightarrow \left(XFA\wedge \neg A\mathrm{t+}\left(F\right)B\right)\right)$$
28		spesbc	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\left(XFa\wedge \neg a\mathrm{t+}\left(F\right)B\right)\to \exists a\left(XFa\wedge \neg a\mathrm{t+}\left(F\right)B\right)$$
29	27 28	syl6bir	$$⊢\phi \to \left(\left(XFA\wedge \neg A\mathrm{t+}\left(F\right)B\right)\to \exists a\left(XFa\wedge \neg a\mathrm{t+}\left(F\right)B\right)\right)$$
30	9 29	mpand	$$⊢\phi \to \left(\neg A\mathrm{t+}\left(F\right)B\to \exists a\left(XFa\wedge \neg a\mathrm{t+}\left(F\right)B\right)\right)$$
31		eupicka	$$⊢\left(\exists !aXFa\wedge \exists a\left(XFa\wedge \neg a\mathrm{t+}\left(F\right)B\right)\right)\to \forall a\left(XFa\to \neg a\mathrm{t+}\left(F\right)B\right)$$
32	11 30 31	syl6an	$$⊢\phi \to \left(\neg A\mathrm{t+}\left(F\right)B\to \forall a\left(XFa\to \neg a\mathrm{t+}\left(F\right)B\right)\right)$$
33		alinexa	$$⊢\forall a\left(XFa\to \neg a\mathrm{t+}\left(F\right)B\right)\leftrightarrow \neg \exists a\left(XFa\wedge a\mathrm{t+}\left(F\right)B\right)$$
34		funrel	$$⊢\mathrm{Fun}F\to \mathrm{Rel}F$$
35	5 34	syl	$$⊢\phi \to \mathrm{Rel}F$$
36		reltrclfv	$$⊢\left(F\in \mathrm{V}\wedge \mathrm{Rel}F\right)\to \mathrm{Rel}\mathrm{t+}\left(F\right)$$
37	1 35 36	syl2anc	$$⊢\phi \to \mathrm{Rel}\mathrm{t+}\left(F\right)$$
38		brrelex2	$$⊢\left(\mathrm{Rel}\mathrm{t+}\left(F\right)\wedge X\mathrm{t+}\left(F\right)B\right)\to B\in \mathrm{V}$$
39	37 4 38	syl2anc	$$⊢\phi \to B\in \mathrm{V}$$
40		brcog	$$⊢\left(X\in \mathrm{dom}F\wedge B\in \mathrm{V}\right)\to \left(X\left(\mathrm{t+}\left(F\right)\circ F\right)B\leftrightarrow \exists a\left(XFa\wedge a\mathrm{t+}\left(F\right)B\right)\right)$$
41	2 39 40	syl2anc	$$⊢\phi \to \left(X\left(\mathrm{t+}\left(F\right)\circ F\right)B\leftrightarrow \exists a\left(XFa\wedge a\mathrm{t+}\left(F\right)B\right)\right)$$
42	41	notbid	$$⊢\phi \to \left(\neg X\left(\mathrm{t+}\left(F\right)\circ F\right)B\leftrightarrow \neg \exists a\left(XFa\wedge a\mathrm{t+}\left(F\right)B\right)\right)$$
43	33 42	bitr4id	$$⊢\phi \to \left(\forall a\left(XFa\to \neg a\mathrm{t+}\left(F\right)B\right)\leftrightarrow \neg X\left(\mathrm{t+}\left(F\right)\circ F\right)B\right)$$
44	32 43	sylibd	$$⊢\phi \to \left(\neg A\mathrm{t+}\left(F\right)B\to \neg X\left(\mathrm{t+}\left(F\right)\circ F\right)B\right)$$
45		brdif	$$⊢X\left(\mathrm{t+}\left(F\right)\setminus \left(\mathrm{t+}\left(F\right)\circ F\right)\right)B\leftrightarrow \left(X\mathrm{t+}\left(F\right)B\wedge \neg X\left(\mathrm{t+}\left(F\right)\circ F\right)B\right)$$
46	45	simplbi2	$$⊢X\mathrm{t+}\left(F\right)B\to \left(\neg X\left(\mathrm{t+}\left(F\right)\circ F\right)B\to X\left(\mathrm{t+}\left(F\right)\setminus \left(\mathrm{t+}\left(F\right)\circ F\right)\right)B\right)$$
47	4 44 46	sylsyld	$$⊢\phi \to \left(\neg A\mathrm{t+}\left(F\right)B\to X\left(\mathrm{t+}\left(F\right)\setminus \left(\mathrm{t+}\left(F\right)\circ F\right)\right)B\right)$$
48		trclfvdecomr	$$⊢F\in \mathrm{V}\to \mathrm{t+}\left(F\right)=F\cup \left(\mathrm{t+}\left(F\right)\circ F\right)$$
49	1 48	syl	$$⊢\phi \to \mathrm{t+}\left(F\right)=F\cup \left(\mathrm{t+}\left(F\right)\circ F\right)$$
50		uncom	$$⊢F\cup \left(\mathrm{t+}\left(F\right)\circ F\right)=\left(\mathrm{t+}\left(F\right)\circ F\right)\cup F$$
51	49 50	eqtrdi	$$⊢\phi \to \mathrm{t+}\left(F\right)=\left(\mathrm{t+}\left(F\right)\circ F\right)\cup F$$
52		eqimss	$$⊢\mathrm{t+}\left(F\right)=\left(\mathrm{t+}\left(F\right)\circ F\right)\cup F\to \mathrm{t+}\left(F\right)\subseteq \left(\mathrm{t+}\left(F\right)\circ F\right)\cup F$$
53	51 52	syl	$$⊢\phi \to \mathrm{t+}\left(F\right)\subseteq \left(\mathrm{t+}\left(F\right)\circ F\right)\cup F$$
54		ssundif	$$⊢\mathrm{t+}\left(F\right)\subseteq \left(\mathrm{t+}\left(F\right)\circ F\right)\cup F\leftrightarrow \mathrm{t+}\left(F\right)\setminus \left(\mathrm{t+}\left(F\right)\circ F\right)\subseteq F$$
55	53 54	sylib	$$⊢\phi \to \mathrm{t+}\left(F\right)\setminus \left(\mathrm{t+}\left(F\right)\circ F\right)\subseteq F$$
56	55	ssbrd	$$⊢\phi \to \left(X\left(\mathrm{t+}\left(F\right)\setminus \left(\mathrm{t+}\left(F\right)\circ F\right)\right)B\to XFB\right)$$
57	47 56	syld	$$⊢\phi \to \left(\neg A\mathrm{t+}\left(F\right)B\to XFB\right)$$
58		funbrfv	$$⊢\mathrm{Fun}F\to \left(XFB\to F\left(X\right)=B\right)$$
59	5 57 58	sylsyld	$$⊢\phi \to \left(\neg A\mathrm{t+}\left(F\right)B\to F\left(X\right)=B\right)$$
60		eqcom	$$⊢F\left(X\right)=B\leftrightarrow B=F\left(X\right)$$
61	59 60	syl6ib	$$⊢\phi \to \left(\neg A\mathrm{t+}\left(F\right)B\to B=F\left(X\right)\right)$$
62		eqtr3	$$⊢\left(A=F\left(X\right)\wedge B=F\left(X\right)\right)\to A=B$$
63	3 61 62	syl6an	$$⊢\phi \to \left(\neg A\mathrm{t+}\left(F\right)B\to A=B\right)$$
64	63	orrd	$$⊢\phi \to \left(A\mathrm{t+}\left(F\right)B\vee A=B\right)$$