Metamath Proof Explorer

Theorem fineqvinfep

Description: A counterexample demonstrating that tz9.1 does not hold when all sets are finite and an infinite descending e. -chain exists. (Contributed by BTernaryTau, 18-Feb-2026)

Ref Expression
Hypothesis fineqvinfep.1 
|- A = { ( F ` (/) ) }
Assertion fineqvinfep 
|- ( ( Fin = _V /\ F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> -. E. y ( A C_ y /\ Tr y ) )

Proof

Step Hyp Ref Expression
1 fineqvinfep.1 
 |-  A = { ( F ` (/) ) }
2 vex 
 |-  y e. _V
3 eleq2 
 |-  ( Fin = _V -> ( y e. Fin <-> y e. _V ) )
4 2 3 mpbiri 
 |-  ( Fin = _V -> y e. Fin )
5 4 3ad2ant1 
 |-  ( ( Fin = _V /\ F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> y e. Fin )
6 fveq2 
 |-  ( w = (/) -> ( F ` w ) = ( F ` (/) ) )
7 6 eleq1d 
 |-  ( w = (/) -> ( ( F ` w ) e. y <-> ( F ` (/) ) e. y ) )
8 fveq2 
 |-  ( w = z -> ( F ` w ) = ( F ` z ) )
9 8 eleq1d 
 |-  ( w = z -> ( ( F ` w ) e. y <-> ( F ` z ) e. y ) )
10 fveq2 
 |-  ( w = suc z -> ( F ` w ) = ( F ` suc z ) )
11 10 eleq1d 
 |-  ( w = suc z -> ( ( F ` w ) e. y <-> ( F ` suc z ) e. y ) )
12 simp2 
 |-  ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ A C_ y /\ Tr y ) -> A C_ y )
13 fvex 
 |-  ( F ` (/) ) e. _V
14 13 snid 
 |-  ( F ` (/) ) e. { ( F ` (/) ) }
15 14 1 eleqtrri 
 |-  ( F ` (/) ) e. A
16 15 a1i 
 |-  ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ A C_ y /\ Tr y ) -> ( F ` (/) ) e. A )
17 12 16 sseldd 
 |-  ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ A C_ y /\ Tr y ) -> ( F ` (/) ) e. y )
18 3simpb 
 |-  ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ A C_ y /\ Tr y ) -> ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ Tr y ) )
19 suceq 
 |-  ( x = z -> suc x = suc z )
20 19 fveq2d 
 |-  ( x = z -> ( F ` suc x ) = ( F ` suc z ) )
21 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
22 20 21 eleq12d 
 |-  ( x = z -> ( ( F ` suc x ) e. ( F ` x ) <-> ( F ` suc z ) e. ( F ` z ) ) )
23 22 rspcv 
 |-  ( z e. _om -> ( A. x e. _om ( F ` suc x ) e. ( F ` x ) -> ( F ` suc z ) e. ( F ` z ) ) )
24 trel 
 |-  ( Tr y -> ( ( ( F ` suc z ) e. ( F ` z ) /\ ( F ` z ) e. y ) -> ( F ` suc z ) e. y ) )
25 24 expd 
 |-  ( Tr y -> ( ( F ` suc z ) e. ( F ` z ) -> ( ( F ` z ) e. y -> ( F ` suc z ) e. y ) ) )
26 25 com12 
 |-  ( ( F ` suc z ) e. ( F ` z ) -> ( Tr y -> ( ( F ` z ) e. y -> ( F ` suc z ) e. y ) ) )
27 23 26 syl6 
 |-  ( z e. _om -> ( A. x e. _om ( F ` suc x ) e. ( F ` x ) -> ( Tr y -> ( ( F ` z ) e. y -> ( F ` suc z ) e. y ) ) ) )
28 27 impd 
 |-  ( z e. _om -> ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ Tr y ) -> ( ( F ` z ) e. y -> ( F ` suc z ) e. y ) ) )
29 18 28 syl5 
 |-  ( z e. _om -> ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ A C_ y /\ Tr y ) -> ( ( F ` z ) e. y -> ( F ` suc z ) e. y ) ) )
30 7 9 11 17 29 finds2 
 |-  ( w e. _om -> ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ A C_ y /\ Tr y ) -> ( F ` w ) e. y ) )
31 30 com12 
 |-  ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ A C_ y /\ Tr y ) -> ( w e. _om -> ( F ` w ) e. y ) )
32 31 ralrimiv 
 |-  ( ( A. x e. _om ( F ` suc x ) e. ( F ` x ) /\ A C_ y /\ Tr y ) -> A. w e. _om ( F ` w ) e. y )
33 32 3expib 
 |-  ( A. x e. _om ( F ` suc x ) e. ( F ` x ) -> ( ( A C_ y /\ Tr y ) -> A. w e. _om ( F ` w ) e. y ) )
34 33 adantl 
 |-  ( ( F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( ( A C_ y /\ Tr y ) -> A. w e. _om ( F ` w ) e. y ) )
35 f1fun 
 |-  ( F : _om -1-1-> _V -> Fun F )
36 f1dm 
 |-  ( F : _om -1-1-> _V -> dom F = _om )
37 36 eqimsscd 
 |-  ( F : _om -1-1-> _V -> _om C_ dom F )
38 funimass4 
 |-  ( ( Fun F /\ _om C_ dom F ) -> ( ( F " _om ) C_ y <-> A. w e. _om ( F ` w ) e. y ) )
39 35 37 38 syl2anc 
 |-  ( F : _om -1-1-> _V -> ( ( F " _om ) C_ y <-> A. w e. _om ( F ` w ) e. y ) )
40 39 adantr 
 |-  ( ( F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( ( F " _om ) C_ y <-> A. w e. _om ( F ` w ) e. y ) )
41 34 40 sylibrd 
 |-  ( ( F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( ( A C_ y /\ Tr y ) -> ( F " _om ) C_ y ) )
42 ominf 
 |-  -. _om e. Fin
43 f1fn 
 |-  ( F : _om -1-1-> _V -> F Fn _om )
44 fnima 
 |-  ( F Fn _om -> ( F " _om ) = ran F )
45 43 44 syl 
 |-  ( F : _om -1-1-> _V -> ( F " _om ) = ran F )
46 45 eqimsscd 
 |-  ( F : _om -1-1-> _V -> ran F C_ ( F " _om ) )
47 f1ssr 
 |-  ( ( F : _om -1-1-> _V /\ ran F C_ ( F " _om ) ) -> F : _om -1-1-> ( F " _om ) )
48 46 47 mpdan 
 |-  ( F : _om -1-1-> _V -> F : _om -1-1-> ( F " _om ) )
49 f1fi 
 |-  ( ( ( F " _om ) e. Fin /\ F : _om -1-1-> ( F " _om ) ) -> _om e. Fin )
50 48 49 sylan2 
 |-  ( ( ( F " _om ) e. Fin /\ F : _om -1-1-> _V ) -> _om e. Fin )
51 50 ancoms 
 |-  ( ( F : _om -1-1-> _V /\ ( F " _om ) e. Fin ) -> _om e. Fin )
52 42 51 mto 
 |-  -. ( F : _om -1-1-> _V /\ ( F " _om ) e. Fin )
53 52 imnani 
 |-  ( F : _om -1-1-> _V -> -. ( F " _om ) e. Fin )
54 ssfi 
 |-  ( ( y e. Fin /\ ( F " _om ) C_ y ) -> ( F " _om ) e. Fin )
55 54 ancoms 
 |-  ( ( ( F " _om ) C_ y /\ y e. Fin ) -> ( F " _om ) e. Fin )
56 55 con3i 
 |-  ( -. ( F " _om ) e. Fin -> -. ( ( F " _om ) C_ y /\ y e. Fin ) )
57 imnan 
 |-  ( ( ( F " _om ) C_ y -> -. y e. Fin ) <-> -. ( ( F " _om ) C_ y /\ y e. Fin ) )
58 56 57 sylibr 
 |-  ( -. ( F " _om ) e. Fin -> ( ( F " _om ) C_ y -> -. y e. Fin ) )
59 53 58 syl 
 |-  ( F : _om -1-1-> _V -> ( ( F " _om ) C_ y -> -. y e. Fin ) )
60 59 adantr 
 |-  ( ( F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( ( F " _om ) C_ y -> -. y e. Fin ) )
61 41 60 syld 
 |-  ( ( F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( ( A C_ y /\ Tr y ) -> -. y e. Fin ) )
62 61 3adant1 
 |-  ( ( Fin = _V /\ F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> ( ( A C_ y /\ Tr y ) -> -. y e. Fin ) )
63 5 62 mt2d 
 |-  ( ( Fin = _V /\ F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> -. ( A C_ y /\ Tr y ) )
64 63 nexdv 
 |-  ( ( Fin = _V /\ F : _om -1-1-> _V /\ A. x e. _om ( F ` suc x ) e. ( F ` x ) ) -> -. E. y ( A C_ y /\ Tr y ) )