Metamath Proof Explorer

Theorem cantnfvalf

Description: Lemma for cantnf . The function appearing in cantnfval is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015)

Ref Expression
Hypothesis cantnfvalf.f 
|- F = seqom ( ( k e. A , z e. B |-> ( C +o D ) ) , (/) )
Assertion cantnfvalf 
|- F : _om --> On

Proof

Step Hyp Ref Expression
1 cantnfvalf.f 
 |-  F = seqom ( ( k e. A , z e. B |-> ( C +o D ) ) , (/) )
2 1 fnseqom 
 |-  F Fn _om
3 nn0suc 
 |-  ( x e. _om -> ( x = (/) \/ E. y e. _om x = suc y ) )
4 fveq2 
 |-  ( x = (/) -> ( F ` x ) = ( F ` (/) ) )
5 0ex 
 |-  (/) e. _V
6 1 seqom0g 
 |-  ( (/) e. _V -> ( F ` (/) ) = (/) )
7 5 6 ax-mp 
 |-  ( F ` (/) ) = (/)
8 4 7 eqtrdi 
 |-  ( x = (/) -> ( F ` x ) = (/) )
9 0elon 
 |-  (/) e. On
10 8 9 eqeltrdi 
 |-  ( x = (/) -> ( F ` x ) e. On )
11 1 seqomsuc 
 |-  ( y e. _om -> ( F ` suc y ) = ( y ( k e. A , z e. B |-> ( C +o D ) ) ( F ` y ) ) )
12 df-ov 
 |-  ( y ( k e. A , z e. B |-> ( C +o D ) ) ( F ` y ) ) = ( ( k e. A , z e. B |-> ( C +o D ) ) ` <. y , ( F ` y ) >. )
13 11 12 eqtrdi 
 |-  ( y e. _om -> ( F ` suc y ) = ( ( k e. A , z e. B |-> ( C +o D ) ) ` <. y , ( F ` y ) >. ) )
14 df-ov 
 |-  ( C +o D ) = ( +o ` <. C , D >. )
15 fnoa 
 |-  +o Fn ( On X. On )
16 oacl 
 |-  ( ( x e. On /\ y e. On ) -> ( x +o y ) e. On )
17 16 rgen2 
 |-  A. x e. On A. y e. On ( x +o y ) e. On
18 ffnov 
 |-  ( +o : ( On X. On ) --> On <-> ( +o Fn ( On X. On ) /\ A. x e. On A. y e. On ( x +o y ) e. On ) )
19 15 17 18 mpbir2an 
 |-  +o : ( On X. On ) --> On
20 19 9 f0cli 
 |-  ( +o ` <. C , D >. ) e. On
21 14 20 eqeltri 
 |-  ( C +o D ) e. On
22 21 rgen2w 
 |-  A. k e. A A. z e. B ( C +o D ) e. On
23 eqid 
 |-  ( k e. A , z e. B |-> ( C +o D ) ) = ( k e. A , z e. B |-> ( C +o D ) )
24 23 fmpo 
 |-  ( A. k e. A A. z e. B ( C +o D ) e. On <-> ( k e. A , z e. B |-> ( C +o D ) ) : ( A X. B ) --> On )
25 22 24 mpbi 
 |-  ( k e. A , z e. B |-> ( C +o D ) ) : ( A X. B ) --> On
26 25 9 f0cli 
 |-  ( ( k e. A , z e. B |-> ( C +o D ) ) ` <. y , ( F ` y ) >. ) e. On
27 13 26 eqeltrdi 
 |-  ( y e. _om -> ( F ` suc y ) e. On )
28 fveq2 
 |-  ( x = suc y -> ( F ` x ) = ( F ` suc y ) )
29 28 eleq1d 
 |-  ( x = suc y -> ( ( F ` x ) e. On <-> ( F ` suc y ) e. On ) )
30 27 29 syl5ibrcom 
 |-  ( y e. _om -> ( x = suc y -> ( F ` x ) e. On ) )
31 30 rexlimiv 
 |-  ( E. y e. _om x = suc y -> ( F ` x ) e. On )
32 10 31 jaoi 
 |-  ( ( x = (/) \/ E. y e. _om x = suc y ) -> ( F ` x ) e. On )
33 3 32 syl 
 |-  ( x e. _om -> ( F ` x ) e. On )
34 33 rgen 
 |-  A. x e. _om ( F ` x ) e. On
35 ffnfv 
 |-  ( F : _om --> On <-> ( F Fn _om /\ A. x e. _om ( F ` x ) e. On ) )
36 2 34 35 mpbir2an 
 |-  F : _om --> On