Metamath Proof Explorer

Theorem tz7.44-2

Description: The value of F at a successor ordinal. Part 2 of Theorem 7.44 of TakeutiZaring p. 49. (Contributed by NM, 23-Apr-1995) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Hypotheses tz7.44.1 
|- G = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) )
tz7.44.2 
|- ( y e. X -> ( F ` y ) = ( G ` ( F |` y ) ) )
tz7.44.3 
|- ( y e. X -> ( F |` y ) e. _V )
tz7.44.4 
|- F Fn X
tz7.44.5 
|- Ord X
Assertion tz7.44-2 
|- ( suc B e. X -> ( F ` suc B ) = ( H ` ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 tz7.44.1 
 |-  G = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) )
2 tz7.44.2 
 |-  ( y e. X -> ( F ` y ) = ( G ` ( F |` y ) ) )
3 tz7.44.3 
 |-  ( y e. X -> ( F |` y ) e. _V )
4 tz7.44.4 
 |-  F Fn X
5 tz7.44.5 
 |-  Ord X
6 fveq2 
 |-  ( y = suc B -> ( F ` y ) = ( F ` suc B ) )
7 reseq2 
 |-  ( y = suc B -> ( F |` y ) = ( F |` suc B ) )
8 7 fveq2d 
 |-  ( y = suc B -> ( G ` ( F |` y ) ) = ( G ` ( F |` suc B ) ) )
9 6 8 eqeq12d 
 |-  ( y = suc B -> ( ( F ` y ) = ( G ` ( F |` y ) ) <-> ( F ` suc B ) = ( G ` ( F |` suc B ) ) ) )
10 9 2 vtoclga 
 |-  ( suc B e. X -> ( F ` suc B ) = ( G ` ( F |` suc B ) ) )
11 eqeq1 
 |-  ( x = ( F |` suc B ) -> ( x = (/) <-> ( F |` suc B ) = (/) ) )
12 dmeq 
 |-  ( x = ( F |` suc B ) -> dom x = dom ( F |` suc B ) )
13 limeq 
 |-  ( dom x = dom ( F |` suc B ) -> ( Lim dom x <-> Lim dom ( F |` suc B ) ) )
14 12 13 syl 
 |-  ( x = ( F |` suc B ) -> ( Lim dom x <-> Lim dom ( F |` suc B ) ) )
15 rneq 
 |-  ( x = ( F |` suc B ) -> ran x = ran ( F |` suc B ) )
16 15 unieqd 
 |-  ( x = ( F |` suc B ) -> U. ran x = U. ran ( F |` suc B ) )
17 fveq1 
 |-  ( x = ( F |` suc B ) -> ( x ` U. dom x ) = ( ( F |` suc B ) ` U. dom x ) )
18 12 unieqd 
 |-  ( x = ( F |` suc B ) -> U. dom x = U. dom ( F |` suc B ) )
19 18 fveq2d 
 |-  ( x = ( F |` suc B ) -> ( ( F |` suc B ) ` U. dom x ) = ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) )
20 17 19 eqtrd 
 |-  ( x = ( F |` suc B ) -> ( x ` U. dom x ) = ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) )
21 20 fveq2d 
 |-  ( x = ( F |` suc B ) -> ( H ` ( x ` U. dom x ) ) = ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) )
22 14 16 21 ifbieq12d 
 |-  ( x = ( F |` suc B ) -> if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) = if ( Lim dom ( F |` suc B ) , U. ran ( F |` suc B ) , ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) ) )
23 11 22 ifbieq2d 
 |-  ( x = ( F |` suc B ) -> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) = if ( ( F |` suc B ) = (/) , A , if ( Lim dom ( F |` suc B ) , U. ran ( F |` suc B ) , ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) ) ) )
24 7 eleq1d 
 |-  ( y = suc B -> ( ( F |` y ) e. _V <-> ( F |` suc B ) e. _V ) )
25 24 3 vtoclga 
 |-  ( suc B e. X -> ( F |` suc B ) e. _V )
26 noel 
 |-  -. B e. (/)
27 dmeq 
 |-  ( ( F |` suc B ) = (/) -> dom ( F |` suc B ) = dom (/) )
28 dm0 
 |-  dom (/) = (/)
29 27 28 eqtrdi 
 |-  ( ( F |` suc B ) = (/) -> dom ( F |` suc B ) = (/) )
30 ordsson 
 |-  ( Ord X -> X C_ On )
31 5 30 ax-mp 
 |-  X C_ On
32 ordtr 
 |-  ( Ord X -> Tr X )
33 5 32 ax-mp 
 |-  Tr X
34 trsuc 
 |-  ( ( Tr X /\ suc B e. X ) -> B e. X )
35 33 34 mpan 
 |-  ( suc B e. X -> B e. X )
36 31 35 sselid 
 |-  ( suc B e. X -> B e. On )
37 sucidg 
 |-  ( B e. On -> B e. suc B )
38 36 37 syl 
 |-  ( suc B e. X -> B e. suc B )
39 dmres 
 |-  dom ( F |` suc B ) = ( suc B i^i dom F )
40 ordelss 
 |-  ( ( Ord X /\ suc B e. X ) -> suc B C_ X )
41 5 40 mpan 
 |-  ( suc B e. X -> suc B C_ X )
42 4 fndmi 
 |-  dom F = X
43 41 42 sseqtrrdi 
 |-  ( suc B e. X -> suc B C_ dom F )
44 df-ss 
 |-  ( suc B C_ dom F <-> ( suc B i^i dom F ) = suc B )
45 43 44 sylib 
 |-  ( suc B e. X -> ( suc B i^i dom F ) = suc B )
46 39 45 eqtrid 
 |-  ( suc B e. X -> dom ( F |` suc B ) = suc B )
47 38 46 eleqtrrd 
 |-  ( suc B e. X -> B e. dom ( F |` suc B ) )
48 eleq2 
 |-  ( dom ( F |` suc B ) = (/) -> ( B e. dom ( F |` suc B ) <-> B e. (/) ) )
49 47 48 syl5ibcom 
 |-  ( suc B e. X -> ( dom ( F |` suc B ) = (/) -> B e. (/) ) )
50 29 49 syl5 
 |-  ( suc B e. X -> ( ( F |` suc B ) = (/) -> B e. (/) ) )
51 26 50 mtoi 
 |-  ( suc B e. X -> -. ( F |` suc B ) = (/) )
52 51 iffalsed 
 |-  ( suc B e. X -> if ( ( F |` suc B ) = (/) , A , if ( Lim dom ( F |` suc B ) , U. ran ( F |` suc B ) , ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) ) ) = if ( Lim dom ( F |` suc B ) , U. ran ( F |` suc B ) , ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) ) )
53 nlimsucg 
 |-  ( B e. On -> -. Lim suc B )
54 36 53 syl 
 |-  ( suc B e. X -> -. Lim suc B )
55 limeq 
 |-  ( dom ( F |` suc B ) = suc B -> ( Lim dom ( F |` suc B ) <-> Lim suc B ) )
56 46 55 syl 
 |-  ( suc B e. X -> ( Lim dom ( F |` suc B ) <-> Lim suc B ) )
57 54 56 mtbird 
 |-  ( suc B e. X -> -. Lim dom ( F |` suc B ) )
58 57 iffalsed 
 |-  ( suc B e. X -> if ( Lim dom ( F |` suc B ) , U. ran ( F |` suc B ) , ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) ) = ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) )
59 46 unieqd 
 |-  ( suc B e. X -> U. dom ( F |` suc B ) = U. suc B )
60 eloni 
 |-  ( B e. On -> Ord B )
61 ordunisuc 
 |-  ( Ord B -> U. suc B = B )
62 36 60 61 3syl 
 |-  ( suc B e. X -> U. suc B = B )
63 59 62 eqtrd 
 |-  ( suc B e. X -> U. dom ( F |` suc B ) = B )
64 63 fveq2d 
 |-  ( suc B e. X -> ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) = ( ( F |` suc B ) ` B ) )
65 38 fvresd 
 |-  ( suc B e. X -> ( ( F |` suc B ) ` B ) = ( F ` B ) )
66 64 65 eqtrd 
 |-  ( suc B e. X -> ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) = ( F ` B ) )
67 66 fveq2d 
 |-  ( suc B e. X -> ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) = ( H ` ( F ` B ) ) )
68 52 58 67 3eqtrd 
 |-  ( suc B e. X -> if ( ( F |` suc B ) = (/) , A , if ( Lim dom ( F |` suc B ) , U. ran ( F |` suc B ) , ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) ) ) = ( H ` ( F ` B ) ) )
69 fvex 
 |-  ( H ` ( F ` B ) ) e. _V
70 68 69 eqeltrdi 
 |-  ( suc B e. X -> if ( ( F |` suc B ) = (/) , A , if ( Lim dom ( F |` suc B ) , U. ran ( F |` suc B ) , ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) ) ) e. _V )
71 1 23 25 70 fvmptd3 
 |-  ( suc B e. X -> ( G ` ( F |` suc B ) ) = if ( ( F |` suc B ) = (/) , A , if ( Lim dom ( F |` suc B ) , U. ran ( F |` suc B ) , ( H ` ( ( F |` suc B ) ` U. dom ( F |` suc B ) ) ) ) ) )
72 10 71 68 3eqtrd 
 |-  ( suc B e. X -> ( F ` suc B ) = ( H ` ( F ` B ) ) )