This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tz7.44-3

Description: The value of F at a limit ordinal. Part 3 of Theorem 7.44 of TakeutiZaring p. 49. (Contributed by NM, 23-Apr-1995) (Revised by David Abernethy, 19-Jun-2012)

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-3 
|- ( ( B e. X /\ Lim B ) -> ( F ` B ) = U. ( 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 = B -> ( F ` y ) = ( F ` B ) )
7 reseq2 
 |-  ( y = B -> ( F |` y ) = ( F |` B ) )
8 7 fveq2d 
 |-  ( y = B -> ( G ` ( F |` y ) ) = ( G ` ( F |` B ) ) )
9 6 8 eqeq12d 
 |-  ( y = B -> ( ( F ` y ) = ( G ` ( F |` y ) ) <-> ( F ` B ) = ( G ` ( F |` B ) ) ) )
10 9 2 vtoclga 
 |-  ( B e. X -> ( F ` B ) = ( G ` ( F |` B ) ) )
11 10 adantr 
 |-  ( ( B e. X /\ Lim B ) -> ( F ` B ) = ( G ` ( F |` B ) ) )
12 7 eleq1d 
 |-  ( y = B -> ( ( F |` y ) e. _V <-> ( F |` B ) e. _V ) )
13 12 3 vtoclga 
 |-  ( B e. X -> ( F |` B ) e. _V )
14 13 adantr 
 |-  ( ( B e. X /\ Lim B ) -> ( F |` B ) e. _V )
15 simpr 
 |-  ( ( B e. X /\ Lim B ) -> Lim B )
16 nlim0 
 |-  -. Lim (/)
17 dmres 
 |-  dom ( F |` B ) = ( B i^i dom F )
18 ordelss 
 |-  ( ( Ord X /\ B e. X ) -> B C_ X )
19 5 18 mpan 
 |-  ( B e. X -> B C_ X )
20 19 adantr 
 |-  ( ( B e. X /\ Lim B ) -> B C_ X )
21 fndm 
 |-  ( F Fn X -> dom F = X )
22 4 21 ax-mp 
 |-  dom F = X
23 20 22 sseqtrrdi 
 |-  ( ( B e. X /\ Lim B ) -> B C_ dom F )
24 dfss2 
 |-  ( B C_ dom F <-> ( B i^i dom F ) = B )
25 23 24 sylib 
 |-  ( ( B e. X /\ Lim B ) -> ( B i^i dom F ) = B )
26 17 25 eqtrid 
 |-  ( ( B e. X /\ Lim B ) -> dom ( F |` B ) = B )
27 dmeq 
 |-  ( ( F |` B ) = (/) -> dom ( F |` B ) = dom (/) )
28 dm0 
 |-  dom (/) = (/)
29 27 28 eqtrdi 
 |-  ( ( F |` B ) = (/) -> dom ( F |` B ) = (/) )
30 26 29 sylan9req 
 |-  ( ( ( B e. X /\ Lim B ) /\ ( F |` B ) = (/) ) -> B = (/) )
31 limeq 
 |-  ( B = (/) -> ( Lim B <-> Lim (/) ) )
32 30 31 syl 
 |-  ( ( ( B e. X /\ Lim B ) /\ ( F |` B ) = (/) ) -> ( Lim B <-> Lim (/) ) )
33 16 32 mtbiri 
 |-  ( ( ( B e. X /\ Lim B ) /\ ( F |` B ) = (/) ) -> -. Lim B )
34 33 ex 
 |-  ( ( B e. X /\ Lim B ) -> ( ( F |` B ) = (/) -> -. Lim B ) )
35 15 34 mt2d 
 |-  ( ( B e. X /\ Lim B ) -> -. ( F |` B ) = (/) )
36 35 iffalsed 
 |-  ( ( B e. X /\ Lim B ) -> if ( ( F |` B ) = (/) , A , if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) ) = if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) )
37 limeq 
 |-  ( dom ( F |` B ) = B -> ( Lim dom ( F |` B ) <-> Lim B ) )
38 26 37 syl 
 |-  ( ( B e. X /\ Lim B ) -> ( Lim dom ( F |` B ) <-> Lim B ) )
39 15 38 mpbird 
 |-  ( ( B e. X /\ Lim B ) -> Lim dom ( F |` B ) )
40 39 iftrued 
 |-  ( ( B e. X /\ Lim B ) -> if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) = U. ran ( F |` B ) )
41 36 40 eqtrd 
 |-  ( ( B e. X /\ Lim B ) -> if ( ( F |` B ) = (/) , A , if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) ) = U. ran ( F |` B ) )
42 rnexg 
 |-  ( ( F |` B ) e. _V -> ran ( F |` B ) e. _V )
43 uniexg 
 |-  ( ran ( F |` B ) e. _V -> U. ran ( F |` B ) e. _V )
44 14 42 43 3syl 
 |-  ( ( B e. X /\ Lim B ) -> U. ran ( F |` B ) e. _V )
45 41 44 eqeltrd 
 |-  ( ( B e. X /\ Lim B ) -> if ( ( F |` B ) = (/) , A , if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) ) e. _V )
46 eqeq1 
 |-  ( x = ( F |` B ) -> ( x = (/) <-> ( F |` B ) = (/) ) )
47 dmeq 
 |-  ( x = ( F |` B ) -> dom x = dom ( F |` B ) )
48 limeq 
 |-  ( dom x = dom ( F |` B ) -> ( Lim dom x <-> Lim dom ( F |` B ) ) )
49 47 48 syl 
 |-  ( x = ( F |` B ) -> ( Lim dom x <-> Lim dom ( F |` B ) ) )
50 rneq 
 |-  ( x = ( F |` B ) -> ran x = ran ( F |` B ) )
51 50 unieqd 
 |-  ( x = ( F |` B ) -> U. ran x = U. ran ( F |` B ) )
52 fveq1 
 |-  ( x = ( F |` B ) -> ( x ` U. dom x ) = ( ( F |` B ) ` U. dom x ) )
53 47 unieqd 
 |-  ( x = ( F |` B ) -> U. dom x = U. dom ( F |` B ) )
54 53 fveq2d 
 |-  ( x = ( F |` B ) -> ( ( F |` B ) ` U. dom x ) = ( ( F |` B ) ` U. dom ( F |` B ) ) )
55 52 54 eqtrd 
 |-  ( x = ( F |` B ) -> ( x ` U. dom x ) = ( ( F |` B ) ` U. dom ( F |` B ) ) )
56 55 fveq2d 
 |-  ( x = ( F |` B ) -> ( H ` ( x ` U. dom x ) ) = ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) )
57 49 51 56 ifbieq12d 
 |-  ( x = ( F |` B ) -> if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) = if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) )
58 46 57 ifbieq2d 
 |-  ( x = ( F |` B ) -> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) = if ( ( F |` B ) = (/) , A , if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) ) )
59 58 1 fvmptg 
 |-  ( ( ( F |` B ) e. _V /\ if ( ( F |` B ) = (/) , A , if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) ) e. _V ) -> ( G ` ( F |` B ) ) = if ( ( F |` B ) = (/) , A , if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) ) )
60 14 45 59 syl2anc 
 |-  ( ( B e. X /\ Lim B ) -> ( G ` ( F |` B ) ) = if ( ( F |` B ) = (/) , A , if ( Lim dom ( F |` B ) , U. ran ( F |` B ) , ( H ` ( ( F |` B ) ` U. dom ( F |` B ) ) ) ) ) )
61 60 41 eqtrd 
 |-  ( ( B e. X /\ Lim B ) -> ( G ` ( F |` B ) ) = U. ran ( F |` B ) )
62 11 61 eqtrd 
 |-  ( ( B e. X /\ Lim B ) -> ( F ` B ) = U. ran ( F |` B ) )
63 df-ima 
 |-  ( F " B ) = ran ( F |` B )
64 63 unieqi 
 |-  U. ( F " B ) = U. ran ( F |` B )
65 62 64 eqtr4di 
 |-  ( ( B e. X /\ Lim B ) -> ( F ` B ) = U. ( F " B ) )