Theorem abianfp 4020

Description: "A most fundamental fixed point theorem" of Alexander Abian (1923-1999), apparently proved in 1998. Let G` 0 = x, G` 1 = F` x, G` 2 = F` (F` x),... be the iterates of F. The theorem reads (using our variable names): "Let F be a mapping from a set A into itself. Then F has a fixed point if and only if: There exists an element x of A such that for every ordinal v , G` v is an element of A, and if G` v is not a fixed point of F then the G` u 's are all distinct for every ordinal u e. v." See df-rdg 3990 for the rec operation. The proof's key idea is to assume that F does not have a fixed point, then use the Axiom of Replacement in the form of f1dmex 3767 to derive that the class of all ordinal numbers exists, contradicting onprc 3046. Our version of this theorem does not require the hypothesis that F be a mapping. Reference: http://www.math.ucdavis.edu/~suh/abian/abian-themostfixed.html. For an application of this theorem, see http://groups.google.com/group/sci.stat.math/msg/1737ee1133c24aeb for its use in a proof of Tarski's fixed point theorem.

Hypotheses

Ref	Expression
abianfp.1	|- A e. V
abianfp.2	|- G = rec({<.z, w>. | w = (F` z)}, x)

Assertion

Ref	Expression
abianfp	|- (E.x e. A (F` x) = x <-> E.x e. A A.v e. On ((G` v) e. A /\ (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u))))

Distinct variable groups:   x,v,A   x,z,w,u,F,v   v,G,u

Proof of Theorem abianfp

Step	Hyp	Ref	Expression
1		abianfp.1	. . . . . . . . . . 11 |- A e. V
2		abianfp.2	. . . . . . . . . . 11 |- G = rec({<.z, w>. | w = (F` z)}, x)
3	1, 2	abianfplem 4019	. . . . . . . . . 10 |- (v e. On -> ((F` x) = x -> (G` v) = x))
4	3	imp 357	. . . . . . . . 9 |- ((v e. On /\ (F` x) = x) -> (G` v) = x)
5	4	eleq1d 1587	. . . . . . . 8 |- ((v e. On /\ (F` x) = x) -> ((G` v) e. A <-> x e. A))
6	5	biimprd 161	. . . . . . 7 |- ((v e. On /\ (F` x) = x) -> (x e. A -> (G` v) e. A))
7		fveq2 3781	. . . . . . . . . . . 12 |- ((G` v) = x -> (F` (G` v)) = (F` x))
8		id 59	. . . . . . . . . . . 12 |- ((G` v) = x -> (G` v) = x)
9	7, 8	eqeq12d 1536	. . . . . . . . . . 11 |- ((G` v) = x -> ((F` (G` v)) = (G` v) <-> (F` x) = x))
10	9	biimprcd 163	. . . . . . . . . 10 |- ((F` x) = x -> ((G` v) = x -> (F` (G` v)) = (G` v)))
11	3, 10	sylcom 51	. . . . . . . . 9 |- (v e. On -> ((F` x) = x -> (F` (G` v)) = (G` v)))
12	11	imp 357	. . . . . . . 8 |- ((v e. On /\ (F` x) = x) -> (F` (G` v)) = (G` v))
13	12	pm2.24d 111	. . . . . . 7 |- ((v e. On /\ (F` x) = x) -> (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u)))
14	6, 13	jctird 613	. . . . . 6 |- ((v e. On /\ (F` x) = x) -> (x e. A -> ((G` v) e. A /\ (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u)))))
15	14	ex 380	. . . . 5 |- (v e. On -> ((F` x) = x -> (x e. A -> ((G` v) e. A /\ (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u))))))
16	15	com13 33	. . . 4 |- (x e. A -> ((F` x) = x -> (v e. On -> ((G` v) e. A /\ (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u))))))
17	16	r19.21adv 1765	. . 3 |- (x e. A -> ((F` x) = x -> A.v e. On ((G` v) e. A /\ (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u)))))
18	17	r19.22i 1779	. 2 |- (E.x e. A (F` x) = x -> E.x e. A A.v e. On ((G` v) e. A /\ (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u))))
19		onprc 3046	. . . . . 6 |- -. On e. V
20		r19.26 1797	. . . . . . 7 |- (A.v e. On ((G` v) e. A /\ (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u))) <-> (A.v e. On (G` v) e. A /\ A.v e. On (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u))))
21		fveq2 3781	. . . . . . . . . . . . . . . . . . 19 |- (y = (G` v) -> (F` y) = (F` (G` v)))
22		id 59	. . . . . . . . . . . . . . . . . . 19 |- (y = (G` v) -> y = (G` v))
23	21, 22	eqeq12d 1536	. . . . . . . . . . . . . . . . . 18 |- (y = (G` v) -> ((F` y) = y <-> (F` (G` v)) = (G` v)))
24	23	notbid 622	. . . . . . . . . . . . . . . . 17 |- (y = (G` v) -> (-. (F` y) = y <-> -. (F` (G` v)) = (G` v)))
25	24	rcla4cv 1921	. . . . . . . . . . . . . . . 16 |- (A.y e. A -. (F` y) = y -> ((G` v) e. A -> -. (F` (G` v)) = (G` v)))
26	25	imim1d 28	. . . . . . . . . . . . . . 15 |- (A.y e. A -. (F` y) = y -> ((-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u)) -> ((G` v) e. A -> A.u e. v -. (G` v) = (G` u))))
27	26	r19.20sdv 1757	. . . . . . . . . . . . . 14 |- (A.y e. A -. (F` y) = y -> (A.v e. On (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u)) -> A.v e. On ((G` v) e. A -> A.u e. v -. (G` v) = (G` u))))
28		r19.20 1749	. . . . . . . . . . . . . 14 |- (A.v e. On ((G` v) e. A -> A.u e. v -. (G` v) = (G` u)) -> (A.v e. On (G` v) e. A -> A.v e. On A.u e. v -. (G` v) = (G` u)))
29	27, 28	syl6 22	. . . . . . . . . . . . 13 |- (A.y e. A -. (F` y) = y -> (A.v e. On (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u)) -> (A.v e. On (G` v) e. A -> A.v e. On A.u e. v -. (G` v) = (G` u))))
30	29	imp 357	. . . . . . . . . . . 12 |- ((A.y e. A -. (F` y) = y /\ A.v e. On (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u))) -> (A.v e. On (G` v) e. A -> A.v e. On A.u e. v -. (G` v) = (G` u)))
31	30	com12 11	. . . . . . . . . . 11 |- (A.v e. On (G` v) e. A -> ((A.y e. A -. (F` y) = y /\ A.v e. On (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u))) -> A.v e. On A.u e. v -. (G` v) = (G` u)))
32		rdgfnon 3997	. . . . . . . . . . . . . . . . 17 |- rec({<.z, w>. | w = (F` z)}, x) Fn On
33		fneq1 3639	. . . . . . . . . . . . . . . . . 18 |- (G = rec({<.z, w>. | w = (F` z)}, x) -> (G Fn On <-> rec({<.z, w>. | w = (F` z)}, x) Fn On))
34	2, 33	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (G Fn On <-> rec({<.z, w>. | w = (F` z)}, x) Fn On)
35	32, 34	mpbir 197	. . . . . . . . . . . . . . . 16 |- G Fn On
36		ffnfv 3885	. . . . . . . . . . . . . . . . 17 |- (G:On-->A <-> (G Fn On /\ A.v e. On (G` v) e. A))
37	36	biimpri 159	. . . . . . . . . . . . . . . 16 |- ((G Fn On /\ A.v e. On (G` v) e. A) -> G:On-->A)
38	35, 37	mpan 707	. . . . . . . . . . . . . . 15 |- (A.v e. On (G` v) e. A -> G:On-->A)
39		ssid 2131	. . . . . . . . . . . . . . . . 17 |- On (_ On
40	35	tz7.48lem 4013	. . . . . . . . . . . . . . . . 17 |- ((On (_ On /\ A.v e. On A.u e. v -. (G` v) = (G` u)) -> Fun `'(G |` On))
41	39, 40	mpan 707	. . . . . . . . . . . . . . . 16 |- (A.v e. On A.u e. v -. (G` v) = (G` u) -> Fun `'(G |` On))
42		fnresdm 3653	. . . . . . . . . . . . . . . . . . 19 |- (G Fn On -> (G |` On) = G)
43	35, 42	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- (G |` On) = G
44		cnveq 3349	. . . . . . . . . . . . . . . . . 18 |- ((G |` On) = G -> `'(G |` On) = `'G)
45	43, 44	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- `'(G |` On) = `'G
46		funeq 3592	. . . . . . . . . . . . . . . . 17 |- (`'(G |` On) = `'G -> (Fun `'(G |` On) <-> Fun `'G))
47	45, 46	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (Fun `'(G |` On) <-> Fun `'G)
48	41, 47	sylib 205	. . . . . . . . . . . . . . 15 |- (A.v e. On A.u e. v -. (G` v) = (G` u) -> Fun `'G)
49	38, 48	anim12i <