Metamath Proof Explorer

Theorem onvf1odlem3

Description: Lemma for onvf1od . The value of F at an ordinal A . (Contributed by BTernaryTau, 2-Dec-2025)

Ref Expression
Hypotheses onvf1odlem3.1 
|- M = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. ran w }
onvf1odlem3.2 
|- N = ( G ` ( ( R1 ` M ) \ ran w ) )
onvf1odlem3.3 
|- F = recs ( ( w e. _V |-> N ) )
onvf1odlem3.4 
|- B = |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " A ) }
onvf1odlem3.5 
|- C = ( G ` ( ( R1 ` B ) \ ( F " A ) ) )
Assertion onvf1odlem3 
|- ( A e. On -> ( F ` A ) = C )

Proof

Step Hyp Ref Expression
1 onvf1odlem3.1 
 |-  M = |^| { x e. On | E. y e. ( R1 ` x ) -. y e. ran w }
2 onvf1odlem3.2 
 |-  N = ( G ` ( ( R1 ` M ) \ ran w ) )
3 onvf1odlem3.3 
 |-  F = recs ( ( w e. _V |-> N ) )
4 onvf1odlem3.4 
 |-  B = |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " A ) }
5 onvf1odlem3.5 
 |-  C = ( G ` ( ( R1 ` B ) \ ( F " A ) ) )
6 3 tfr2 
 |-  ( A e. On -> ( F ` A ) = ( ( w e. _V |-> N ) ` ( F |` A ) ) )
7 3 tfr1 
 |-  F Fn On
8 fnfun 
 |-  ( F Fn On -> Fun F )
9 7 8 ax-mp 
 |-  Fun F
10 resfunexg 
 |-  ( ( Fun F /\ A e. On ) -> ( F |` A ) e. _V )
11 9 10 mpan 
 |-  ( A e. On -> ( F |` A ) e. _V )
12 eleq1w 
 |-  ( t = v -> ( t e. ran r <-> v e. ran r ) )
13 12 notbid 
 |-  ( t = v -> ( -. t e. ran r <-> -. v e. ran r ) )
14 13 adantl 
 |-  ( ( s = u /\ t = v ) -> ( -. t e. ran r <-> -. v e. ran r ) )
15 fveq2 
 |-  ( s = u -> ( R1 ` s ) = ( R1 ` u ) )
16 15 adantr 
 |-  ( ( s = u /\ t = v ) -> ( R1 ` s ) = ( R1 ` u ) )
17 14 16 cbvrexdva2 
 |-  ( s = u -> ( E. t e. ( R1 ` s ) -. t e. ran r <-> E. v e. ( R1 ` u ) -. v e. ran r ) )
18 17 cbvrabv 
 |-  { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } = { u e. On | E. v e. ( R1 ` u ) -. v e. ran r }
19 rneq 
 |-  ( r = ( F |` A ) -> ran r = ran ( F |` A ) )
20 df-ima 
 |-  ( F " A ) = ran ( F |` A )
21 19 20 eqtr4di 
 |-  ( r = ( F |` A ) -> ran r = ( F " A ) )
22 21 eleq2d 
 |-  ( r = ( F |` A ) -> ( v e. ran r <-> v e. ( F " A ) ) )
23 22 notbid 
 |-  ( r = ( F |` A ) -> ( -. v e. ran r <-> -. v e. ( F " A ) ) )
24 23 rexbidv 
 |-  ( r = ( F |` A ) -> ( E. v e. ( R1 ` u ) -. v e. ran r <-> E. v e. ( R1 ` u ) -. v e. ( F " A ) ) )
25 24 rabbidv 
 |-  ( r = ( F |` A ) -> { u e. On | E. v e. ( R1 ` u ) -. v e. ran r } = { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " A ) } )
26 18 25 eqtrid 
 |-  ( r = ( F |` A ) -> { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } = { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " A ) } )
27 26 inteqd 
 |-  ( r = ( F |` A ) -> |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } = |^| { u e. On | E. v e. ( R1 ` u ) -. v e. ( F " A ) } )
28 27 4 eqtr4di 
 |-  ( r = ( F |` A ) -> |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } = B )
29 28 fveq2d 
 |-  ( r = ( F |` A ) -> ( R1 ` |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } ) = ( R1 ` B ) )
30 29 21 difeq12d 
 |-  ( r = ( F |` A ) -> ( ( R1 ` |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } ) \ ran r ) = ( ( R1 ` B ) \ ( F " A ) ) )
31 30 fveq2d 
 |-  ( r = ( F |` A ) -> ( G ` ( ( R1 ` |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } ) \ ran r ) ) = ( G ` ( ( R1 ` B ) \ ( F " A ) ) ) )
32 31 5 eqtr4di 
 |-  ( r = ( F |` A ) -> ( G ` ( ( R1 ` |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } ) \ ran r ) ) = C )
33 eleq1w 
 |-  ( y = t -> ( y e. ran w <-> t e. ran w ) )
34 33 notbid 
 |-  ( y = t -> ( -. y e. ran w <-> -. t e. ran w ) )
35 34 adantl 
 |-  ( ( x = s /\ y = t ) -> ( -. y e. ran w <-> -. t e. ran w ) )
36 fveq2 
 |-  ( x = s -> ( R1 ` x ) = ( R1 ` s ) )
37 36 adantr 
 |-  ( ( x = s /\ y = t ) -> ( R1 ` x ) = ( R1 ` s ) )
38 35 37 cbvrexdva2 
 |-  ( x = s -> ( E. y e. ( R1 ` x ) -. y e. ran w <-> E. t e. ( R1 ` s ) -. t e. ran w ) )
39 38 cbvrabv 
 |-  { x e. On | E. y e. ( R1 ` x ) -. y e. ran w } = { s e. On | E. t e. ( R1 ` s ) -. t e. ran w }
40 rneq 
 |-  ( w = r -> ran w = ran r )
41 40 eleq2d 
 |-  ( w = r -> ( t e. ran w <-> t e. ran r ) )
42 41 notbid 
 |-  ( w = r -> ( -. t e. ran w <-> -. t e. ran r ) )
43 42 rexbidv 
 |-  ( w = r -> ( E. t e. ( R1 ` s ) -. t e. ran w <-> E. t e. ( R1 ` s ) -. t e. ran r ) )
44 43 rabbidv 
 |-  ( w = r -> { s e. On | E. t e. ( R1 ` s ) -. t e. ran w } = { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } )
45 39 44 eqtrid 
 |-  ( w = r -> { x e. On | E. y e. ( R1 ` x ) -. y e. ran w } = { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } )
46 45 inteqd 
 |-  ( w = r -> |^| { x e. On | E. y e. ( R1 ` x ) -. y e. ran w } = |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } )
47 1 46 eqtrid 
 |-  ( w = r -> M = |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } )
48 47 fveq2d 
 |-  ( w = r -> ( R1 ` M ) = ( R1 ` |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } ) )
49 48 40 difeq12d 
 |-  ( w = r -> ( ( R1 ` M ) \ ran w ) = ( ( R1 ` |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } ) \ ran r ) )
50 49 fveq2d 
 |-  ( w = r -> ( G ` ( ( R1 ` M ) \ ran w ) ) = ( G ` ( ( R1 ` |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } ) \ ran r ) ) )
51 2 50 eqtrid 
 |-  ( w = r -> N = ( G ` ( ( R1 ` |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } ) \ ran r ) ) )
52 51 cbvmptv 
 |-  ( w e. _V |-> N ) = ( r e. _V |-> ( G ` ( ( R1 ` |^| { s e. On | E. t e. ( R1 ` s ) -. t e. ran r } ) \ ran r ) ) )
53 5 fvexi 
 |-  C e. _V
54 32 52 53 fvmpt 
 |-  ( ( F |` A ) e. _V -> ( ( w e. _V |-> N ) ` ( F |` A ) ) = C )
55 11 54 syl 
 |-  ( A e. On -> ( ( w e. _V |-> N ) ` ( F |` A ) ) = C )
56 6 55 eqtrd 
 |-  ( A e. On -> ( F ` A ) = C )