Theorem abianfp 3000

Description: "A most fundamental fixed point theorem" of Alexander Abian (1923-1999), apparently proved in 1998. "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." Note that G` 0 = x, G` 1 = F` x, G` 2 = F` (F` x),... are the iterates of F. See df-rdg 2970 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 2819 to derive that the class of all ordinals exists, contradicting onprc 2240. 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.

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 group(s):   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 2999	. . . . . . . . . 10 |- (v e. On -> ((F` x) = x -> (G` v) = x))
4	3	imp 277	. . . . . . . . 9 |- ((v e. On /\ (F` x) = x) -> (G` v) = x)
5	4	eleq1d 1155	. . . . . . . 8 |- ((v e. On /\ (F` x) = x) -> ((G` v) e. A <-> x e. A))
6	5	biimprd 136	. . . . . . 7 |- ((v e. On /\ (F` x) = x) -> (x e. A -> (G` v) e. A))
7		fveq2 2832	. . . . . . . . . . . . . 14 |- ((G` v) = x -> (F` (G` v)) = (F` x))
8		id 9	. . . . . . . . . . . . . 14 |- ((G` v) = x -> (G` v) = x)
9	7, 8	cleq12d 1115	. . . . . . . . . . . . 13 |- ((G` v) = x -> ((F` (G` v)) = (G` v) <-> (F` x) = x))
10	9	biimprcd 138	. . . . . . . . . . . 12 |- ((F` x) = x -> ((G` v) = x -> (F` (G` v)) = (G` v)))
11	3, 10	sylcom 51	. . . . . . . . . . 11 |- (v e. On -> ((F` x) = x -> (F` (G` v)) = (G` v)))
12	11	imp 277	. . . . . . . . . 10 |- ((v e. On /\ (F` x) = x) -> (F` (G` v)) = (G` v))
13		negb 79	. . . . . . . . . 10 |- ((F` (G` v)) = (G` v) -> -. -. (F` (G` v)) = (G` v))
14	12, 13	syl 12	. . . . . . . . 9 |- ((v e. On /\ (F` x) = x) -> -. -. (F` (G` v)) = (G` v))
15	14	pm2.21d 74	. . . . . . . 8 |- ((v e. On /\ (F` x) = x) -> (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u)))
16	15	a1d 14	. . . . . . 7 |- ((v e. On /\ (F` x) = x) -> (x e. A -> (-. (F` (G` v)) = (G` v) -> A.u e. v -. (G` v) = (G` u))))
17	6, 16	jcad 455	. . . . . 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)))))
18	17	exp 291	. . . . 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))))))
19	18	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))))))
20	19	r19.21adv 1262	. . 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)))))
21	20	r19.22i 1273	. 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))))
22		onprc 2240	. . . . . 6 |- -. On e. V
23		r19.26 1289	. . . . . . 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))))
24		fveq2 2832	. . . . . . . . . . . . . . . . . . 19 |- (y = (G` v) -> (F` y) = (F` (G` v)))
25		id 9	. . . . . . . . . . . . . . . . . . 19 |- (y = (G` v) -> y = (G` v))
26	24, 25	cleq12d 1115	. . . . . . . . . . . . . . . . . 18 |- (y = (G` v) -> ((F` y) = y <-> (F` (G` v)) = (G` v)))
27	26	negbid 463	. . . . . . . . . . . . . . . . 17 |- (y = (G` v) -> (-. (F` y) = y <-> -. (F` (G` v)) = (G` v)))
28	27	rcla4v 1402	. . . . . . . . . . . . . . . 16 |- (A.y e. A -. (F` y) = y -> ((G` v) e. A -> -. (F` (G` v)) = (G` v)))
29	28	syl4d 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))))
30	29	r19.20sdv 1257	. . . . . . . . . . . . . 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))))
31		r19.20 1251	. . . . . . . . . . . . . 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)))
32	30, 31	syl6 23	. . . . . . . . . . . . 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))))
33	32	imp 277	. . . . . . . . . . . 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)))
34	33	com12 13	. . . . . . . . . . 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)))
35		rdgfnon 2977	. . . . . . . . . . . . . . . . 17 |- rec({<.z, w>. | w = (F` z)}, x) Fn On
36		fneq1 2718	. . . . . . . . . . . . . . . . . 18 |- (G = rec({<.z, w>. | w = (F` z)}, x) -> (G Fn On <-> rec({<.z, w>. | w = (F` z)}, x) Fn On))
37	2, 36	ax-mp 6	. . . . . . . . . . . . . . . . 17 |- (G Fn On <-> rec({<.z, w>. | w = (F` z)}, x) Fn On)
38	35, 37	mpbir 165	. . . . . . . . . . . . . . . 16 |- G Fn On
39		ffnfv 2892	. . . . . . . . . . . . . . . . 17 |- (G:On-->A <-> (G Fn On /\ A.v e. On (G` v) e. A))
40	39	biimpr 134	. . . . . . . . . . . . . . . 16 |- ((G Fn On /\ A.v e. On (G` v) e. A) -> G:On-->A)
41	38, 40	mpan 518	. . . . . . . . . . . . . . 15 |- (A.v e. On (G` v) e. A -> G:On-->A)
42		ssid 1519	. . . . . . . . . . . . . . . . 17 |- On (_ On
43	38	tz7.48lem 2993	. . . . . . . . . . . . . . . . 17 |- ((On (_ On /\ A.v e. On A.u e. v -. (G` v) = (G` u)) -> Fun `'(G |` On))
44	42, 43	mpan 518	. . . . . . . . . . . . . . . 16 |- (A.v e. On A.u e. v -. (G` v) = (G` u) -> Fun `'(G |` On))
45		fnresdm 2731	. . . . . . . . . . . . . . . . . . 19 |- (G Fn On -> (G |` On) = G)
46	38, 45	ax-mp 6	. . . . . . . . . . . . . . . . . 18 |- (G |` On) = G
47		cnveq 2513	. . . . . . . . . . . . . . . . . 18 |- ((G |` On) = G -> `'(G |` On) = `'G)
48	46, 47	ax-mp 6	. . . . . . . . . . . . . . . . 17 |- `'(G |` On) = `'G
49		funeq 2683	. . . . . . . . . . . . . . . . 17 |- (`'(G |`