Theorem noinfep 5747

Description: Using the Axiom of Regularity in the form zfregfr 5706, show that there are no infinite descending e.-chains. Proposition 7.34 of [TakeutiZaring] p. 44.

Assertion

Ref	Expression
noinfep	|- (F Fn om -> E.x e. om -. (F` suc x) e. (F` x))

Distinct variable group:   x,F

Proof of Theorem noinfep

Step	Hyp	Ref	Expression
1		fndm 4512	. . . . 5 |- (F Fn om -> dom F = om)
2		omex 5733	. . . . 5 |- om e. _V
3	1, 2	syl6eqel 1979	. . . 4 |- (F Fn om -> dom F e. _V)
4		fnfun 4510	. . . 4 |- (F Fn om -> Fun F)
5		funrnex 4544	. . . 4 |- (dom F e. _V -> (Fun F -> ran F e. _V))
6	3, 4, 5	sylc 83	. . 3 |- (F Fn om -> ran F e. _V)
7		peano1 3971	. . . . . . 7 |- (/) e. om
8		eleq2 1958	. . . . . . 7 |- (dom F = om -> ((/) e. dom F <-> (/) e. om))
9	7, 8	mpbiri 211	. . . . . 6 |- (dom F = om -> (/) e. dom F)
10		ne0i 2881	. . . . . 6 |- ((/) e. dom F -> dom F =/= (/))
11	9, 10	syl 12	. . . . 5 |- (dom F = om -> dom F =/= (/))
12		dm0rn0 4175	. . . . . 6 |- (dom F = (/) <-> ran F = (/))
13	12	necon3bii 2032	. . . . 5 |- (dom F =/= (/) <-> ran F =/= (/))
14	11, 13	sylib 215	. . . 4 |- (dom F = om -> ran F =/= (/))
15	1, 14	syl 12	. . 3 |- (F Fn om -> ran F =/= (/))
16		zfregfr 5706	. . . 4 |- _E Fr ran F
17		ssid 2634	. . . . 5 |- ran F C_ ran F
18		fri 3626	. . . . 5 |- (((ran F e. _V /\ _E Fr ran F) /\ (ran F C_ ran F /\ ran F =/= (/))) -> E.y e. ran FA.z e. ran F -. z _E y)
19	17, 18	mpanr1 774	. . . 4 |- (((ran F e. _V /\ _E Fr ran F) /\ ran F =/= (/)) -> E.y e. ran FA.z e. ran F -. z _E y)
20	16, 19	mpanl2 771	. . 3 |- ((ran F e. _V /\ ran F =/= (/)) -> E.y e. ran FA.z e. ran F -. z _E y)
21	6, 15, 20	syl11anc 524	. 2 |- (F Fn om -> E.y e. ran FA.z e. ran F -. z _E y)
22		fvelrnb 4719	. . . . . . 7 |- (F Fn om -> (y e. ran F <-> E.x e. om (F` x) = y))
23	22	adantr 425	. . . . . 6 |- ((F Fn om /\ A.z e. ran F -. z _E y) -> (y e. ran F <-> E.x e. om (F` x) = y))
24		eleq2 1958	. . . . . . . . . . . 12 |- ((F` x) = y -> ((F` suc x) e. (F` x) <-> (F` suc x) e. y))
25	24	notbid 673	. . . . . . . . . . 11 |- ((F` x) = y -> (-. (F` suc x) e. (F` x) <-> -. (F` suc x) e. y))
26		eleq1 1957	. . . . . . . . . . . . . 14 |- (z = (F` suc x) -> (z e. y <-> (F` suc x) e. y))
27		epel 3585	. . . . . . . . . . . . . 14 |- (z _E y <-> z e. y)
28	26, 27	syl5bb 591	. . . . . . . . . . . . 13 |- (z = (F` suc x) -> (z _E y <-> (F` suc x) e. y))
29	28	notbid 673	. . . . . . . . . . . 12 |- (z = (F` suc x) -> (-. z _E y <-> -. (F` suc x) e. y))
30	29	rcla4va 2378	. . . . . . . . . . 11 |- (((F` suc x) e. ran F /\ A.z e. ran F -. z _E y) -> -. (F` suc x) e. y)
31	25, 30	syl5bir 227	. . . . . . . . . 10 |- ((F` x) = y -> (((F` suc x) e. ran F /\ A.z e. ran F -. z _E y) -> -. (F` suc x) e. (F` x)))
32		fnfvelrn 4786	. . . . . . . . . . . 12 |- ((F Fn om /\ suc x e. om) -> (F` suc x) e. ran F)
33	32	adantlr 429	. . . . . . . . . . 11 |- (((F Fn om /\ A.z e. ran F -. z _E y) /\ suc x e. om) -> (F` suc x) e. ran F)
34		simplr 449	. . . . . . . . . . 11 |- (((F Fn om /\ A.z e. ran F -. z _E y) /\ suc x e. om) -> A.z e. ran F -. z _E y)
35	33, 34	jca 310	. . . . . . . . . 10 |- (((F Fn om /\ A.z e. ran F -. z _E y) /\ suc x e. om) -> ((F` suc x) e. ran F /\ A.z e. ran F -. z _E y))
36	31, 35	syl5 20	. . . . . . . . 9 |- ((F` x) = y -> (((F Fn om /\ A.z e. ran F -. z _E y) /\ suc x e. om) -> -. (F` suc x) e. (F` x)))
37		peano2 3972	. . . . . . . . 9 |- (x e. om -> suc x e. om)
38	36, 37	sylan2i 514	. . . . . . . 8 |- ((F` x) = y -> (((F Fn om /\ A.z e. ran F -. z _E y) /\ x e. om) -> -. (F` suc x) e. (F` x)))
39	38	com12 14	. . . . . . 7 |- (((F Fn om /\ A.z e. ran F -. z _E y) /\ x e. om) -> ((F` x) = y -> -. (F` suc x) e. (F` x)))
40	39	reximdva 2203	. . . . . 6 |- ((F Fn om /\ A.z e. ran F -. z _E y) -> (E.x e. om (F` x) = y -> E.x e. om -. (F` suc x) e. (F` x)))
41	23, 40	sylbid 220	. . . . 5 |- ((F Fn om /\ A.z e. ran F -. z _E y) -> (y e. ran F -> E.x e. om -. (F` suc x) e. (F` x)))
42	41	ex 402	. . . 4 |- (F Fn om -> (A.z e. ran F -. z _E y -> (y e. ran F -> E.x e. om -. (F` suc x) e. (F` x))))
43	42	com23 36	. . 3 |- (F Fn om -> (y e. ran F -> (A.z e. ran F -. z _E y -> E.x e. om -. (F` suc x) e. (F` x))))
44	43	r19.23adv 2215	. 2 |- (F Fn om -> (E.y e. ran FA.z e. ran F -. z _E y -> E.x e. om -. (F` suc x) e. (F` x)))
45	21, 44	mpd 29	1 |- (F Fn om -> E.x e. om -. (F` suc x) e. (F` x))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  (/)c0 2875   class class class wbr 3338   _E cep 3581   Fr wfr 3623  suc csuc 3659  omcom 3949  dom cdm 3986  ran crn 3987  Fun wfun 3992   Fn wfn 3993  ` cfv 3998

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014

Copyright terms: Public domain