Metamath Proof Explorer

Theorem fineqvnttrclselem3

Description: Lemma for fineqvnttrclse . (Contributed by BTernaryTau, 12-Jan-2026)

Ref Expression
Hypotheses fineqvnttrclselem3.1 
|- R = { <. x , y >. | ( x e. A /\ x = suc y ) }
fineqvnttrclselem3.2 
|- A = _om
fineqvnttrclselem3.3 
|- F = ( v e. suc suc N |-> U. { d e. On | ( v +o d ) = B } )
Assertion fineqvnttrclselem3 
|- ( ( B e. ( _om \ 1o ) /\ N e. B ) -> A. a e. suc N ( F ` a ) R ( F ` suc a ) )

Proof

Step Hyp Ref Expression
1 fineqvnttrclselem3.1 
 |-  R = { <. x , y >. | ( x e. A /\ x = suc y ) }
2 fineqvnttrclselem3.2 
 |-  A = _om
3 fineqvnttrclselem3.3 
 |-  F = ( v e. suc suc N |-> U. { d e. On | ( v +o d ) = B } )
4 oveq1 
 |-  ( v = a -> ( v +o d ) = ( a +o d ) )
5 4 eqeq1d 
 |-  ( v = a -> ( ( v +o d ) = B <-> ( a +o d ) = B ) )
6 5 rabbidv 
 |-  ( v = a -> { d e. On | ( v +o d ) = B } = { d e. On | ( a +o d ) = B } )
7 6 unieqd 
 |-  ( v = a -> U. { d e. On | ( v +o d ) = B } = U. { d e. On | ( a +o d ) = B } )
8 elelsuc 
 |-  ( a e. suc N -> a e. suc suc N )
9 8 adantl 
 |-  ( ( B e. ( _om \ 1o ) /\ a e. suc N ) -> a e. suc suc N )
10 fineqvnttrclselem1 
 |-  ( B e. ( _om \ 1o ) -> U. { d e. On | ( a +o d ) = B } e. _om )
11 10 adantr 
 |-  ( ( B e. ( _om \ 1o ) /\ a e. suc N ) -> U. { d e. On | ( a +o d ) = B } e. _om )
12 3 7 9 11 fvmptd3 
 |-  ( ( B e. ( _om \ 1o ) /\ a e. suc N ) -> ( F ` a ) = U. { d e. On | ( a +o d ) = B } )
13 12 11 eqeltrd 
 |-  ( ( B e. ( _om \ 1o ) /\ a e. suc N ) -> ( F ` a ) e. _om )
14 13 3adant2 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> ( F ` a ) e. _om )
15 14 2 eleqtrrdi 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> ( F ` a ) e. A )
16 3 fineqvnttrclselem2 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc suc N ) -> ( a +o ( F ` a ) ) = B )
17 8 16 syl3an3 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> ( a +o ( F ` a ) ) = B )
18 eldifi 
 |-  ( B e. ( _om \ 1o ) -> B e. _om )
19 elnn 
 |-  ( ( N e. B /\ B e. _om ) -> N e. _om )
20 19 ancoms 
 |-  ( ( B e. _om /\ N e. B ) -> N e. _om )
21 18 20 sylan 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B ) -> N e. _om )
22 peano2 
 |-  ( N e. _om -> suc N e. _om )
23 nnord 
 |-  ( suc N e. _om -> Ord suc N )
24 ordsucelsuc 
 |-  ( Ord suc N -> ( a e. suc N <-> suc a e. suc suc N ) )
25 22 23 24 3syl 
 |-  ( N e. _om -> ( a e. suc N <-> suc a e. suc suc N ) )
26 25 biimpa 
 |-  ( ( N e. _om /\ a e. suc N ) -> suc a e. suc suc N )
27 21 26 stoic3 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> suc a e. suc suc N )
28 3 fineqvnttrclselem2 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ suc a e. suc suc N ) -> ( suc a +o ( F ` suc a ) ) = B )
29 27 28 syld3an3 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> ( suc a +o ( F ` suc a ) ) = B )
30 17 29 eqtr4d 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> ( a +o ( F ` a ) ) = ( suc a +o ( F ` suc a ) ) )
31 21 22 syl 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B ) -> suc N e. _om )
32 elnn 
 |-  ( ( a e. suc N /\ suc N e. _om ) -> a e. _om )
33 32 ancoms 
 |-  ( ( suc N e. _om /\ a e. suc N ) -> a e. _om )
34 31 33 stoic3 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> a e. _om )
35 21 3adant3 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> N e. _om )
36 oveq1 
 |-  ( v = suc a -> ( v +o d ) = ( suc a +o d ) )
37 36 eqeq1d 
 |-  ( v = suc a -> ( ( v +o d ) = B <-> ( suc a +o d ) = B ) )
38 37 rabbidv 
 |-  ( v = suc a -> { d e. On | ( v +o d ) = B } = { d e. On | ( suc a +o d ) = B } )
39 38 unieqd 
 |-  ( v = suc a -> U. { d e. On | ( v +o d ) = B } = U. { d e. On | ( suc a +o d ) = B } )
40 26 3adant1 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. _om /\ a e. suc N ) -> suc a e. suc suc N )
41 fineqvnttrclselem1 
 |-  ( B e. ( _om \ 1o ) -> U. { d e. On | ( suc a +o d ) = B } e. _om )
42 41 3ad2ant1 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. _om /\ a e. suc N ) -> U. { d e. On | ( suc a +o d ) = B } e. _om )
43 3 39 40 42 fvmptd3 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. _om /\ a e. suc N ) -> ( F ` suc a ) = U. { d e. On | ( suc a +o d ) = B } )
44 43 42 eqeltrd 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. _om /\ a e. suc N ) -> ( F ` suc a ) e. _om )
45 35 44 syld3an2 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> ( F ` suc a ) e. _om )
46 nnacom 
 |-  ( ( a e. _om /\ ( F ` suc a ) e. _om ) -> ( a +o ( F ` suc a ) ) = ( ( F ` suc a ) +o a ) )
47 46 suceqd 
 |-  ( ( a e. _om /\ ( F ` suc a ) e. _om ) -> suc ( a +o ( F ` suc a ) ) = suc ( ( F ` suc a ) +o a ) )
48 nnasuc 
 |-  ( ( a e. _om /\ ( F ` suc a ) e. _om ) -> ( a +o suc ( F ` suc a ) ) = suc ( a +o ( F ` suc a ) ) )
49 nnasuc 
 |-  ( ( ( F ` suc a ) e. _om /\ a e. _om ) -> ( ( F ` suc a ) +o suc a ) = suc ( ( F ` suc a ) +o a ) )
50 49 ancoms 
 |-  ( ( a e. _om /\ ( F ` suc a ) e. _om ) -> ( ( F ` suc a ) +o suc a ) = suc ( ( F ` suc a ) +o a ) )
51 47 48 50 3eqtr4d 
 |-  ( ( a e. _om /\ ( F ` suc a ) e. _om ) -> ( a +o suc ( F ` suc a ) ) = ( ( F ` suc a ) +o suc a ) )
52 peano2 
 |-  ( a e. _om -> suc a e. _om )
53 nnacom 
 |-  ( ( suc a e. _om /\ ( F ` suc a ) e. _om ) -> ( suc a +o ( F ` suc a ) ) = ( ( F ` suc a ) +o suc a ) )
54 52 53 sylan 
 |-  ( ( a e. _om /\ ( F ` suc a ) e. _om ) -> ( suc a +o ( F ` suc a ) ) = ( ( F ` suc a ) +o suc a ) )
55 51 54 eqtr4d 
 |-  ( ( a e. _om /\ ( F ` suc a ) e. _om ) -> ( a +o suc ( F ` suc a ) ) = ( suc a +o ( F ` suc a ) ) )
56 55 3adant2 
 |-  ( ( a e. _om /\ ( F ` a ) e. _om /\ ( F ` suc a ) e. _om ) -> ( a +o suc ( F ` suc a ) ) = ( suc a +o ( F ` suc a ) ) )
57 56 eqeq2d 
 |-  ( ( a e. _om /\ ( F ` a ) e. _om /\ ( F ` suc a ) e. _om ) -> ( ( a +o ( F ` a ) ) = ( a +o suc ( F ` suc a ) ) <-> ( a +o ( F ` a ) ) = ( suc a +o ( F ` suc a ) ) ) )
58 peano2 
 |-  ( ( F ` suc a ) e. _om -> suc ( F ` suc a ) e. _om )
59 nnacan 
 |-  ( ( a e. _om /\ ( F ` a ) e. _om /\ suc ( F ` suc a ) e. _om ) -> ( ( a +o ( F ` a ) ) = ( a +o suc ( F ` suc a ) ) <-> ( F ` a ) = suc ( F ` suc a ) ) )
60 58 59 syl3an3 
 |-  ( ( a e. _om /\ ( F ` a ) e. _om /\ ( F ` suc a ) e. _om ) -> ( ( a +o ( F ` a ) ) = ( a +o suc ( F ` suc a ) ) <-> ( F ` a ) = suc ( F ` suc a ) ) )
61 57 60 bitr3d 
 |-  ( ( a e. _om /\ ( F ` a ) e. _om /\ ( F ` suc a ) e. _om ) -> ( ( a +o ( F ` a ) ) = ( suc a +o ( F ` suc a ) ) <-> ( F ` a ) = suc ( F ` suc a ) ) )
62 34 14 45 61 syl3anc 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> ( ( a +o ( F ` a ) ) = ( suc a +o ( F ` suc a ) ) <-> ( F ` a ) = suc ( F ` suc a ) ) )
63 30 62 mpbid 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> ( F ` a ) = suc ( F ` suc a ) )
64 fvex 
 |-  ( F ` a ) e. _V
65 fvex 
 |-  ( F ` suc a ) e. _V
66 eleq1 
 |-  ( x = ( F ` a ) -> ( x e. A <-> ( F ` a ) e. A ) )
67 eqeq1 
 |-  ( x = ( F ` a ) -> ( x = suc y <-> ( F ` a ) = suc y ) )
68 66 67 anbi12d 
 |-  ( x = ( F ` a ) -> ( ( x e. A /\ x = suc y ) <-> ( ( F ` a ) e. A /\ ( F ` a ) = suc y ) ) )
69 suceq 
 |-  ( y = ( F ` suc a ) -> suc y = suc ( F ` suc a ) )
70 69 eqeq2d 
 |-  ( y = ( F ` suc a ) -> ( ( F ` a ) = suc y <-> ( F ` a ) = suc ( F ` suc a ) ) )
71 70 anbi2d 
 |-  ( y = ( F ` suc a ) -> ( ( ( F ` a ) e. A /\ ( F ` a ) = suc y ) <-> ( ( F ` a ) e. A /\ ( F ` a ) = suc ( F ` suc a ) ) ) )
72 64 65 68 71 1 brab 
 |-  ( ( F ` a ) R ( F ` suc a ) <-> ( ( F ` a ) e. A /\ ( F ` a ) = suc ( F ` suc a ) ) )
73 15 63 72 sylanbrc 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B /\ a e. suc N ) -> ( F ` a ) R ( F ` suc a ) )
74 73 3expia 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B ) -> ( a e. suc N -> ( F ` a ) R ( F ` suc a ) ) )
75 74 ralrimiv 
 |-  ( ( B e. ( _om \ 1o ) /\ N e. B ) -> A. a e. suc N ( F ` a ) R ( F ` suc a ) )