Metamath Proof Explorer

Theorem finxpreclem6

Description: Lemma for ^^ recursion theorems. (Contributed by ML, 24-Oct-2020)

Ref Expression
Hypothesis finxpreclem5.1 
|- F = ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
Assertion finxpreclem6 
|- ( ( N e. _om /\ 1o e. N ) -> ( U ^^ N ) C_ ( _V X. U ) )

Proof

Step Hyp Ref Expression
1 finxpreclem5.1 
 |-  F = ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
2 eleq1 
 |-  ( n = N -> ( n e. _om <-> N e. _om ) )
3 eleq2 
 |-  ( n = N -> ( 1o e. n <-> 1o e. N ) )
4 2 3 anbi12d 
 |-  ( n = N -> ( ( n e. _om /\ 1o e. n ) <-> ( N e. _om /\ 1o e. N ) ) )
5 anass 
 |-  ( ( ( n e. _om /\ 1o e. n ) /\ -. y e. ( _V X. U ) ) <-> ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) )
6 nfv 
 |-  F/ x ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) )
7 nfmpo2 
 |-  F/_ x ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
8 1 7 nfcxfr 
 |-  F/_ x F
9 nfcv 
 |-  F/_ x <. n , y >.
10 8 9 nfrdg 
 |-  F/_ x rec ( F , <. n , y >. )
11 nfcv 
 |-  F/_ x n
12 10 11 nffv 
 |-  F/_ x ( rec ( F , <. n , y >. ) ` n )
13 12 nfeq2 
 |-  F/ x (/) = ( rec ( F , <. n , y >. ) ` n )
14 13 nfn 
 |-  F/ x -. (/) = ( rec ( F , <. n , y >. ) ` n )
15 6 14 nfim 
 |-  F/ x ( ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) -> -. (/) = ( rec ( F , <. n , y >. ) ` n ) )
16 eleq1 
 |-  ( x = y -> ( x e. ( _V X. U ) <-> y e. ( _V X. U ) ) )
17 16 notbid 
 |-  ( x = y -> ( -. x e. ( _V X. U ) <-> -. y e. ( _V X. U ) ) )
18 17 anbi2d 
 |-  ( x = y -> ( ( 1o e. n /\ -. x e. ( _V X. U ) ) <-> ( 1o e. n /\ -. y e. ( _V X. U ) ) ) )
19 18 anbi2d 
 |-  ( x = y -> ( ( n e. _om /\ ( 1o e. n /\ -. x e. ( _V X. U ) ) ) <-> ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) ) )
20 opeq2 
 |-  ( x = y -> <. n , x >. = <. n , y >. )
21 rdgeq2 
 |-  ( <. n , x >. = <. n , y >. -> rec ( F , <. n , x >. ) = rec ( F , <. n , y >. ) )
22 20 21 syl 
 |-  ( x = y -> rec ( F , <. n , x >. ) = rec ( F , <. n , y >. ) )
23 22 fveq1d 
 |-  ( x = y -> ( rec ( F , <. n , x >. ) ` n ) = ( rec ( F , <. n , y >. ) ` n ) )
24 23 eqeq2d 
 |-  ( x = y -> ( (/) = ( rec ( F , <. n , x >. ) ` n ) <-> (/) = ( rec ( F , <. n , y >. ) ` n ) ) )
25 24 notbid 
 |-  ( x = y -> ( -. (/) = ( rec ( F , <. n , x >. ) ` n ) <-> -. (/) = ( rec ( F , <. n , y >. ) ` n ) ) )
26 19 25 imbi12d 
 |-  ( x = y -> ( ( ( n e. _om /\ ( 1o e. n /\ -. x e. ( _V X. U ) ) ) -> -. (/) = ( rec ( F , <. n , x >. ) ` n ) ) <-> ( ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) -> -. (/) = ( rec ( F , <. n , y >. ) ` n ) ) ) )
27 anass 
 |-  ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) <-> ( n e. _om /\ ( 1o e. n /\ -. x e. ( _V X. U ) ) ) )
28 vex 
 |-  n e. _V
29 fveqeq2 
 |-  ( m = (/) -> ( ( rec ( F , <. n , x >. ) ` m ) = <. n , x >. <-> ( rec ( F , <. n , x >. ) ` (/) ) = <. n , x >. ) )
30 fveqeq2 
 |-  ( m = o -> ( ( rec ( F , <. n , x >. ) ` m ) = <. n , x >. <-> ( rec ( F , <. n , x >. ) ` o ) = <. n , x >. ) )
31 fveqeq2 
 |-  ( m = suc o -> ( ( rec ( F , <. n , x >. ) ` m ) = <. n , x >. <-> ( rec ( F , <. n , x >. ) ` suc o ) = <. n , x >. ) )
32 opex 
 |-  <. n , x >. e. _V
33 32 rdg0 
 |-  ( rec ( F , <. n , x >. ) ` (/) ) = <. n , x >.
34 33 a1i 
 |-  ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( rec ( F , <. n , x >. ) ` (/) ) = <. n , x >. )
35 nnon 
 |-  ( o e. _om -> o e. On )
36 rdgsuc 
 |-  ( o e. On -> ( rec ( F , <. n , x >. ) ` suc o ) = ( F ` ( rec ( F , <. n , x >. ) ` o ) ) )
37 35 36 syl 
 |-  ( o e. _om -> ( rec ( F , <. n , x >. ) ` suc o ) = ( F ` ( rec ( F , <. n , x >. ) ` o ) ) )
38 fveq2 
 |-  ( ( rec ( F , <. n , x >. ) ` o ) = <. n , x >. -> ( F ` ( rec ( F , <. n , x >. ) ` o ) ) = ( F ` <. n , x >. ) )
39 37 38 sylan9eq 
 |-  ( ( o e. _om /\ ( rec ( F , <. n , x >. ) ` o ) = <. n , x >. ) -> ( rec ( F , <. n , x >. ) ` suc o ) = ( F ` <. n , x >. ) )
40 1 finxpreclem5 
 |-  ( ( n e. _om /\ 1o e. n ) -> ( -. x e. ( _V X. U ) -> ( F ` <. n , x >. ) = <. n , x >. ) )
41 40 imp 
 |-  ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( F ` <. n , x >. ) = <. n , x >. )
42 39 41 sylan9eq 
 |-  ( ( ( o e. _om /\ ( rec ( F , <. n , x >. ) ` o ) = <. n , x >. ) /\ ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) ) -> ( rec ( F , <. n , x >. ) ` suc o ) = <. n , x >. )
43 42 expl 
 |-  ( o e. _om -> ( ( ( rec ( F , <. n , x >. ) ` o ) = <. n , x >. /\ ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) ) -> ( rec ( F , <. n , x >. ) ` suc o ) = <. n , x >. ) )
44 43 expcomd 
 |-  ( o e. _om -> ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( ( rec ( F , <. n , x >. ) ` o ) = <. n , x >. -> ( rec ( F , <. n , x >. ) ` suc o ) = <. n , x >. ) ) )
45 29 30 31 34 44 finds2 
 |-  ( m e. _om -> ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( rec ( F , <. n , x >. ) ` m ) = <. n , x >. ) )
46 eleq1 
 |-  ( n = m -> ( n e. _om <-> m e. _om ) )
47 fveqeq2 
 |-  ( n = m -> ( ( rec ( F , <. n , x >. ) ` n ) = <. n , x >. <-> ( rec ( F , <. n , x >. ) ` m ) = <. n , x >. ) )
48 47 imbi2d 
 |-  ( n = m -> ( ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( rec ( F , <. n , x >. ) ` n ) = <. n , x >. ) <-> ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( rec ( F , <. n , x >. ) ` m ) = <. n , x >. ) ) )
49 46 48 imbi12d 
 |-  ( n = m -> ( ( n e. _om -> ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( rec ( F , <. n , x >. ) ` n ) = <. n , x >. ) ) <-> ( m e. _om -> ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( rec ( F , <. n , x >. ) ` m ) = <. n , x >. ) ) ) )
50 45 49 mpbiri 
 |-  ( n = m -> ( n e. _om -> ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( rec ( F , <. n , x >. ) ` n ) = <. n , x >. ) ) )
51 50 equcoms 
 |-  ( m = n -> ( n e. _om -> ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( rec ( F , <. n , x >. ) ` n ) = <. n , x >. ) ) )
52 28 51 vtocle 
 |-  ( n e. _om -> ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( rec ( F , <. n , x >. ) ` n ) = <. n , x >. ) )
53 27 52 syl5bir 
 |-  ( n e. _om -> ( ( n e. _om /\ ( 1o e. n /\ -. x e. ( _V X. U ) ) ) -> ( rec ( F , <. n , x >. ) ` n ) = <. n , x >. ) )
54 53 anabsi5 
 |-  ( ( n e. _om /\ ( 1o e. n /\ -. x e. ( _V X. U ) ) ) -> ( rec ( F , <. n , x >. ) ` n ) = <. n , x >. )
55 vex 
 |-  x e. _V
56 28 55 opnzi 
 |-  <. n , x >. =/= (/)
57 56 a1i 
 |-  ( ( n e. _om /\ ( 1o e. n /\ -. x e. ( _V X. U ) ) ) -> <. n , x >. =/= (/) )
58 54 57 eqnetrd 
 |-  ( ( n e. _om /\ ( 1o e. n /\ -. x e. ( _V X. U ) ) ) -> ( rec ( F , <. n , x >. ) ` n ) =/= (/) )
59 58 necomd 
 |-  ( ( n e. _om /\ ( 1o e. n /\ -. x e. ( _V X. U ) ) ) -> (/) =/= ( rec ( F , <. n , x >. ) ` n ) )
60 59 neneqd 
 |-  ( ( n e. _om /\ ( 1o e. n /\ -. x e. ( _V X. U ) ) ) -> -. (/) = ( rec ( F , <. n , x >. ) ` n ) )
61 15 26 60 chvarfv 
 |-  ( ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) -> -. (/) = ( rec ( F , <. n , y >. ) ` n ) )
62 61 intnand 
 |-  ( ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) -> -. ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) )
63 62 adantl 
 |-  ( ( n = N /\ ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) ) -> -. ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) )
64 opeq1 
 |-  ( n = N -> <. n , y >. = <. N , y >. )
65 rdgeq2 
 |-  ( <. n , y >. = <. N , y >. -> rec ( F , <. n , y >. ) = rec ( F , <. N , y >. ) )
66 64 65 syl 
 |-  ( n = N -> rec ( F , <. n , y >. ) = rec ( F , <. N , y >. ) )
67 id 
 |-  ( n = N -> n = N )
68 66 67 fveq12d 
 |-  ( n = N -> ( rec ( F , <. n , y >. ) ` n ) = ( rec ( F , <. N , y >. ) ` N ) )
69 68 eqeq2d 
 |-  ( n = N -> ( (/) = ( rec ( F , <. n , y >. ) ` n ) <-> (/) = ( rec ( F , <. N , y >. ) ` N ) ) )
70 2 69 anbi12d 
 |-  ( n = N -> ( ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) <-> ( N e. _om /\ (/) = ( rec ( F , <. N , y >. ) ` N ) ) ) )
71 70 abbidv 
 |-  ( n = N -> { y | ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) } = { y | ( N e. _om /\ (/) = ( rec ( F , <. N , y >. ) ` N ) ) } )
72 1 dffinxpf 
 |-  ( U ^^ N ) = { y | ( N e. _om /\ (/) = ( rec ( F , <. N , y >. ) ` N ) ) }
73 71 72 eqtr4di 
 |-  ( n = N -> { y | ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) } = ( U ^^ N ) )
74 73 eleq2d 
 |-  ( n = N -> ( y e. { y | ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) } <-> y e. ( U ^^ N ) ) )
75 abid 
 |-  ( y e. { y | ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) } <-> ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) )
76 74 75 bitr3di 
 |-  ( n = N -> ( y e. ( U ^^ N ) <-> ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) ) )
77 76 adantr 
 |-  ( ( n = N /\ ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) ) -> ( y e. ( U ^^ N ) <-> ( n e. _om /\ (/) = ( rec ( F , <. n , y >. ) ` n ) ) ) )
78 63 77 mtbird 
 |-  ( ( n = N /\ ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) ) -> -. y e. ( U ^^ N ) )
79 78 ex 
 |-  ( n = N -> ( ( n e. _om /\ ( 1o e. n /\ -. y e. ( _V X. U ) ) ) -> -. y e. ( U ^^ N ) ) )
80 5 79 syl5bi 
 |-  ( n = N -> ( ( ( n e. _om /\ 1o e. n ) /\ -. y e. ( _V X. U ) ) -> -. y e. ( U ^^ N ) ) )
81 80 expdimp 
 |-  ( ( n = N /\ ( n e. _om /\ 1o e. n ) ) -> ( -. y e. ( _V X. U ) -> -. y e. ( U ^^ N ) ) )
82 81 con4d 
 |-  ( ( n = N /\ ( n e. _om /\ 1o e. n ) ) -> ( y e. ( U ^^ N ) -> y e. ( _V X. U ) ) )
83 82 ssrdv 
 |-  ( ( n = N /\ ( n e. _om /\ 1o e. n ) ) -> ( U ^^ N ) C_ ( _V X. U ) )
84 83 ex 
 |-  ( n = N -> ( ( n e. _om /\ 1o e. n ) -> ( U ^^ N ) C_ ( _V X. U ) ) )
85 4 84 sylbird 
 |-  ( n = N -> ( ( N e. _om /\ 1o e. N ) -> ( U ^^ N ) C_ ( _V X. U ) ) )
86 85 vtocleg 
 |-  ( N e. _om -> ( ( N e. _om /\ 1o e. N ) -> ( U ^^ N ) C_ ( _V X. U ) ) )
87 86 anabsi5 
 |-  ( ( N e. _om /\ 1o e. N ) -> ( U ^^ N ) C_ ( _V X. U ) )