Metamath Proof Explorer

Theorem noinfepfnregs

Description: There are no infinite descending e. -chains, proven using ax-regs . (Contributed by BTernaryTau, 18-Feb-2026)

Ref Expression
Assertion noinfepfnregs 
|- ( F Fn _om -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) )

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 1 n0ii 
 |-  -. _om = (/)
3 ssid 
 |-  _om C_ _om
4 fnimaeq0 
 |-  ( ( F Fn _om /\ _om C_ _om ) -> ( ( F " _om ) = (/) <-> _om = (/) ) )
5 3 4 mpan2 
 |-  ( F Fn _om -> ( ( F " _om ) = (/) <-> _om = (/) ) )
6 2 5 mtbiri 
 |-  ( F Fn _om -> -. ( F " _om ) = (/) )
7 6 neqned 
 |-  ( F Fn _om -> ( F " _om ) =/= (/) )
8 axregszf 
 |-  ( ( F " _om ) =/= (/) -> E. y e. ( F " _om ) ( y i^i ( F " _om ) ) = (/) )
9 7 8 syl 
 |-  ( F Fn _om -> E. y e. ( F " _om ) ( y i^i ( F " _om ) ) = (/) )
10 fvelimab 
 |-  ( ( F Fn _om /\ _om C_ _om ) -> ( y e. ( F " _om ) <-> E. x e. _om ( F ` x ) = y ) )
11 3 10 mpan2 
 |-  ( F Fn _om -> ( y e. ( F " _om ) <-> E. x e. _om ( F ` x ) = y ) )
12 11 adantr 
 |-  ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) -> ( y e. ( F " _om ) <-> E. x e. _om ( F ` x ) = y ) )
13 simprl 
 |-  ( ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) /\ ( x e. _om /\ ( F ` x ) = y ) ) -> x e. _om )
14 peano2 
 |-  ( x e. _om -> suc x e. _om )
15 fnfvima 
 |-  ( ( F Fn _om /\ _om C_ _om /\ suc x e. _om ) -> ( F ` suc x ) e. ( F " _om ) )
16 3 15 mp3an2 
 |-  ( ( F Fn _om /\ suc x e. _om ) -> ( F ` suc x ) e. ( F " _om ) )
17 14 16 sylan2 
 |-  ( ( F Fn _om /\ x e. _om ) -> ( F ` suc x ) e. ( F " _om ) )
18 17 ad2ant2r 
 |-  ( ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) /\ ( x e. _om /\ ( F ` x ) = y ) ) -> ( F ` suc x ) e. ( F " _om ) )
19 ineq1 
 |-  ( ( F ` x ) = y -> ( ( F ` x ) i^i ( F " _om ) ) = ( y i^i ( F " _om ) ) )
20 19 eqeq1d 
 |-  ( ( F ` x ) = y -> ( ( ( F ` x ) i^i ( F " _om ) ) = (/) <-> ( y i^i ( F " _om ) ) = (/) ) )
21 20 biimparc 
 |-  ( ( ( y i^i ( F " _om ) ) = (/) /\ ( F ` x ) = y ) -> ( ( F ` x ) i^i ( F " _om ) ) = (/) )
22 21 ad2ant2l 
 |-  ( ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) /\ ( x e. _om /\ ( F ` x ) = y ) ) -> ( ( F ` x ) i^i ( F " _om ) ) = (/) )
23 minel 
 |-  ( ( ( F ` suc x ) e. ( F " _om ) /\ ( ( F ` x ) i^i ( F " _om ) ) = (/) ) -> -. ( F ` suc x ) e. ( F ` x ) )
24 18 22 23 syl2anc 
 |-  ( ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) /\ ( x e. _om /\ ( F ` x ) = y ) ) -> -. ( F ` suc x ) e. ( F ` x ) )
25 df-nel 
 |-  ( ( F ` suc x ) e/ ( F ` x ) <-> -. ( F ` suc x ) e. ( F ` x ) )
26 24 25 sylibr 
 |-  ( ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) /\ ( x e. _om /\ ( F ` x ) = y ) ) -> ( F ` suc x ) e/ ( F ` x ) )
27 13 26 jca 
 |-  ( ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) /\ ( x e. _om /\ ( F ` x ) = y ) ) -> ( x e. _om /\ ( F ` suc x ) e/ ( F ` x ) ) )
28 27 ex 
 |-  ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) -> ( ( x e. _om /\ ( F ` x ) = y ) -> ( x e. _om /\ ( F ` suc x ) e/ ( F ` x ) ) ) )
29 28 reximdv2 
 |-  ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) -> ( E. x e. _om ( F ` x ) = y -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) ) )
30 12 29 sylbid 
 |-  ( ( F Fn _om /\ ( y i^i ( F " _om ) ) = (/) ) -> ( y e. ( F " _om ) -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) ) )
31 30 expimpd 
 |-  ( F Fn _om -> ( ( ( y i^i ( F " _om ) ) = (/) /\ y e. ( F " _om ) ) -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) ) )
32 31 ancomsd 
 |-  ( F Fn _om -> ( ( y e. ( F " _om ) /\ ( y i^i ( F " _om ) ) = (/) ) -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) ) )
33 32 imp 
 |-  ( ( F Fn _om /\ ( y e. ( F " _om ) /\ ( y i^i ( F " _om ) ) = (/) ) ) -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) )
34 9 33 rexlimddv 
 |-  ( F Fn _om -> E. x e. _om ( F ` suc x ) e/ ( F ` x ) )