Theorem abianfp 3962

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 3932 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 3710 to derive that the class of all ordinal numbers exists, contradicting onprc 2989. 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 3961	. . . . . . . . . 10 |- (v e. On -> ((F` x) = x -> (G` v) = x))
4	3	imp 350	. . . . . . . . 9 |- ((v e. On /\ (F` x) = x) -> (G` v) = x)
5	4	eleq1d 1540	. . . . . . . 8 |- ((v e. On /\ (F` x) = x) -> ((G` v) e. A <-> x e. A))
6	5	biimprd 154	. . . . . . 7 |- ((v e. On /\ (F` x) = x) -> (x e. A -> (G` v) e. A))
7		fveq2 3724	. . . . . . . . . . . 12 |- ((G` v) = x -> (F` (G` v)) = (F` x))
8		id 59	. . . . . . . . . . . 12 |- ((G` v) = x -> (G` v) = x)
9	7, 8	eqeq12d 1489	. . . . . . . . . . 11 |- ((G` v) = x -> ((F` (G` v)) = (G` v) <-> (F` x) = x))
10	9	biimprcd 156	. . . . . . . . . 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 350	. . . . . . . 8 |- ((v e. On /\ (F` x) = x) -> (F` (G` v)) = (G` v))
13	12	pm2.24d 105	. . . . . . 7 |- ((v e. On /\ (F` x) = x) -> (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u)))
14	6, 13	jctird 602	. . . . . 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 373	. . . . 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 1718	. . 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 1732	. 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 2989	. . . . . 6 |- -. On e. V
20		r19.26 1750	. . . . . . 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 3724	. . . . . . . . . . . . . . . . . . 19 |- (y = (G` v) -> (F` y) = (F` (G` v)))
22		id 59	. . . . . . . . . . . . . . . . . . 19 |- (y = (G` v) -> y = (G` v))
23	21, 22	eqeq12d 1489	. . . . . . . . . . . . . . . . . 18 |- (y = (G` v) -> ((F` y) = y <-> (F` (G` v)) = (G` v)))
24	23	negbid 611	. . . . . . . . . . . . . . . . 17 |- (y = (G` v) -> (-. (F` y) = y <-> -. (F` (G` v)) = (G` v)))
25	24	rcla4cv 1874	. . . . . . . . . . . . . . . 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 1710	. . . . . . . . . . . . . 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 1702	. . . . . . . . . . . . . 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 350	. . . . . . . . . . . 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 3939	. . . . . . . . . . . . . . . . 17 |- rec({<.z, w>. | w = (F` z)}, x) Fn On
33		fneq1 3582	. . . . . . . . . . . . . . . . . 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 190	. . . . . . . . . . . . . . . 16 |- G Fn On
36		ffnfv 3828	. . . . . . . . . . . . . . . . 17 |- (G:On-->A <-> (G Fn On /\ A.v e. On (G` v) e. A))
37	36	biimpr 152	. . . . . . . . . . . . . . . 16 |- ((G Fn On /\ A.v e. On (G` v) e. A) -> G:On-->A)
38	35, 37	mpan 695	. . . . . . . . . . . . . . 15 |- (A.v e. On (G` v) e. A -> G:On-->A)
39		ssid 2080	. . . . . . . . . . . . . . . . 17 |- On (_ On
40	35	tz7.48lem 3955	. . . . . . . . . . . . . . . . 17 |- ((On (_ On /\ A.v e. On A.u e. v -. (G` v) = (G` u)) -> Fun `'(G |` On))
41	39, 40	mpan 695	. . . . . . . . . . . . . . . 16 |- (A.v e. On A.u e. v -. (G` v) = (G` u) -> Fun `'(G |` On))
42		fnresdm 3596	. . . . . . . . . . . . . . . . . . 19 |- (G Fn On -> (G |` On) = G)
43	35, 42	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- (G |` On) = G
44		cnveq 3292	. . . . . . . . . . . . . . . . . 18 |- ((G |` On) = G -> `'(G |` On) = `'G)
45	43, 44	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- `'(G |` On) = `'G
46		funeq 3535	. . . . . . . . . . . . . . . . 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 198	. . . . . . . . . . . . . . 15 |- (A.v e. On A.u e. v -. (G` v) = (G` u) -> Fun `'G)
49	38, 48	anim12i