Theorem abianfp 3947

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 3917 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 3695 to derive that the class of all ordinal numbers exists, contradicting onprc 2979. 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 3946	. . . . . . . . . 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 1532	. . . . . . . 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 3709	. . . . . . . . . . . 12 |- ((G` v) = x -> (F` (G` v)) = (F` x))
8		id 59	. . . . . . . . . . . 12 |- ((G` v) = x -> (G` v) = x)
9	7, 8	eqeq12d 1481	. . . . . . . . . . 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 600	. . . . . 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 1710	. . 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 1724	. 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 2979	. . . . . 6 |- -. On e. V
20		r19.26 1742	. . . . . . 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 3709	. . . . . . . . . . . . . . . . . . 19 |- (y = (G` v) -> (F` y) = (F` (G` v)))
22		id 59	. . . . . . . . . . . . . . . . . . 19 |- (y = (G` v) -> y = (G` v))
23	21, 22	eqeq12d 1481	. . . . . . . . . . . . . . . . . 18 |- (y = (G` v) -> ((F` y) = y <-> (F` (G` v)) = (G` v)))
24	23	negbid 609	. . . . . . . . . . . . . . . . 17 |- (y = (G` v) -> (-. (F` y) = y <-> -. (F` (G` v)) = (G` v)))
25	24	rcla4cv 1865	. . . . . . . . . . . . . . . 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 1702	. . . . . . . . . . . . . 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 1694	. . . . . . . . . . . . . 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 3924	. . . . . . . . . . . . . . . . 17 |- rec({<.z, w>. | w = (F` z)}, x) Fn On
33		fneq1 3568	. . . . . . . . . . . . . . . . . 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 3813	. . . . . . . . . . . . . . . . 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 693	. . . . . . . . . . . . . . 15 |- (A.v e. On (G` v) e. A -> G:On-->A)
39		ssid 2070	. . . . . . . . . . . . . . . . 17 |- On (_ On
40	35	tz7.48lem 3940	. . . . . . . . . . . . . . . . 17 |- ((On (_ On /\ A.v e. On A.u e. v -. (G` v) = (G` u)) -> Fun `'(G |` On))
41	39, 40	mpan 693	. . . . . . . . . . . . . . . 16 |- (A.v e. On A.u e. v -. (G` v) = (G` u) -> Fun `'(G |` On))
42		fnresdm 3582	. . . . . . . . . . . . . . . . . . 19 |- (G Fn On -> (G |` On) = G)
43	35, 42	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- (G |` On) = G
44		cnveq 3281	. . . . . . . . . . . . . . . . . 18 |- ((G |` On) = G -> `'(G |` On) = `'G)
45	43, 44	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- `'(G |` On) = `'G
46		funeq 3521	. . . . . . . . . . . . . . . . 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 333