Metamath Proof Explorer

Theorem finxpsuclem

Description: Lemma for finxpsuc . (Contributed by ML, 24-Oct-2020)

Ref Expression
Hypothesis finxpsuclem.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 finxpsuclem 
|- ( ( N e. _om /\ 1o C_ N ) -> ( U ^^ suc N ) = ( ( U ^^ N ) X. U ) )

Proof

Step Hyp Ref Expression
1 finxpsuclem.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 peano2 
 |-  ( N e. _om -> suc N e. _om )
3 2 adantr 
 |-  ( ( N e. _om /\ 1o C_ N ) -> suc N e. _om )
4 1on 
 |-  1o e. On
5 4 onordi 
 |-  Ord 1o
6 nnord 
 |-  ( N e. _om -> Ord N )
7 ordsseleq 
 |-  ( ( Ord 1o /\ Ord N ) -> ( 1o C_ N <-> ( 1o e. N \/ 1o = N ) ) )
8 5 6 7 sylancr 
 |-  ( N e. _om -> ( 1o C_ N <-> ( 1o e. N \/ 1o = N ) ) )
9 8 biimpa 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( 1o e. N \/ 1o = N ) )
10 elelsuc 
 |-  ( 1o e. N -> 1o e. suc N )
11 10 a1i 
 |-  ( N e. _om -> ( 1o e. N -> 1o e. suc N ) )
12 sucidg 
 |-  ( N e. _om -> N e. suc N )
13 eleq1 
 |-  ( 1o = N -> ( 1o e. suc N <-> N e. suc N ) )
14 12 13 syl5ibrcom 
 |-  ( N e. _om -> ( 1o = N -> 1o e. suc N ) )
15 11 14 jaod 
 |-  ( N e. _om -> ( ( 1o e. N \/ 1o = N ) -> 1o e. suc N ) )
16 15 adantr 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( ( 1o e. N \/ 1o = N ) -> 1o e. suc N ) )
17 9 16 mpd 
 |-  ( ( N e. _om /\ 1o C_ N ) -> 1o e. suc N )
18 1 finxpreclem6 
 |-  ( ( suc N e. _om /\ 1o e. suc N ) -> ( U ^^ suc N ) C_ ( _V X. U ) )
19 3 17 18 syl2anc 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( U ^^ suc N ) C_ ( _V X. U ) )
20 19 sselda 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( U ^^ suc N ) ) -> y e. ( _V X. U ) )
21 2 ad2antrr 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> suc N e. _om )
22 df-2o 
 |-  2o = suc 1o
23 ordsucsssuc 
 |-  ( ( Ord 1o /\ Ord N ) -> ( 1o C_ N <-> suc 1o C_ suc N ) )
24 5 6 23 sylancr 
 |-  ( N e. _om -> ( 1o C_ N <-> suc 1o C_ suc N ) )
25 24 biimpa 
 |-  ( ( N e. _om /\ 1o C_ N ) -> suc 1o C_ suc N )
26 22 25 eqsstrid 
 |-  ( ( N e. _om /\ 1o C_ N ) -> 2o C_ suc N )
27 26 adantr 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> 2o C_ suc N )
28 simpr 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> y e. ( _V X. U ) )
29 1 finxpreclem4 
 |-  ( ( ( suc N e. _om /\ 2o C_ suc N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. suc N , y >. ) ` suc N ) = ( rec ( F , <. U. suc N , ( 1st ` y ) >. ) ` U. suc N ) )
30 21 27 28 29 syl21anc 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. suc N , y >. ) ` suc N ) = ( rec ( F , <. U. suc N , ( 1st ` y ) >. ) ` U. suc N ) )
31 ordunisuc 
 |-  ( Ord N -> U. suc N = N )
32 6 31 syl 
 |-  ( N e. _om -> U. suc N = N )
33 opeq1 
 |-  ( U. suc N = N -> <. U. suc N , ( 1st ` y ) >. = <. N , ( 1st ` y ) >. )
34 rdgeq2 
 |-  ( <. U. suc N , ( 1st ` y ) >. = <. N , ( 1st ` y ) >. -> rec ( F , <. U. suc N , ( 1st ` y ) >. ) = rec ( F , <. N , ( 1st ` y ) >. ) )
35 33 34 syl 
 |-  ( U. suc N = N -> rec ( F , <. U. suc N , ( 1st ` y ) >. ) = rec ( F , <. N , ( 1st ` y ) >. ) )
36 32 35 syl 
 |-  ( N e. _om -> rec ( F , <. U. suc N , ( 1st ` y ) >. ) = rec ( F , <. N , ( 1st ` y ) >. ) )
37 36 32 fveq12d 
 |-  ( N e. _om -> ( rec ( F , <. U. suc N , ( 1st ` y ) >. ) ` U. suc N ) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) )
38 37 ad2antrr 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. U. suc N , ( 1st ` y ) >. ) ` U. suc N ) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) )
39 30 38 eqtrd 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. suc N , y >. ) ` suc N ) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) )
40 39 eqeq2d 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> ( (/) = ( rec ( F , <. suc N , y >. ) ` suc N ) <-> (/) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) ) )
41 1 dffinxpf 
 |-  ( U ^^ suc N ) = { y | ( suc N e. _om /\ (/) = ( rec ( F , <. suc N , y >. ) ` suc N ) ) }
42 41 eqabri 
 |-  ( y e. ( U ^^ suc N ) <-> ( suc N e. _om /\ (/) = ( rec ( F , <. suc N , y >. ) ` suc N ) ) )
43 2 biantrurd 
 |-  ( N e. _om -> ( (/) = ( rec ( F , <. suc N , y >. ) ` suc N ) <-> ( suc N e. _om /\ (/) = ( rec ( F , <. suc N , y >. ) ` suc N ) ) ) )
44 42 43 bitr4id 
 |-  ( N e. _om -> ( y e. ( U ^^ suc N ) <-> (/) = ( rec ( F , <. suc N , y >. ) ` suc N ) ) )
45 44 ad2antrr 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> ( y e. ( U ^^ suc N ) <-> (/) = ( rec ( F , <. suc N , y >. ) ` suc N ) ) )
46 fvex 
 |-  ( 1st ` y ) e. _V
47 opeq2 
 |-  ( z = ( 1st ` y ) -> <. N , z >. = <. N , ( 1st ` y ) >. )
48 rdgeq2 
 |-  ( <. N , z >. = <. N , ( 1st ` y ) >. -> rec ( F , <. N , z >. ) = rec ( F , <. N , ( 1st ` y ) >. ) )
49 47 48 syl 
 |-  ( z = ( 1st ` y ) -> rec ( F , <. N , z >. ) = rec ( F , <. N , ( 1st ` y ) >. ) )
50 49 fveq1d 
 |-  ( z = ( 1st ` y ) -> ( rec ( F , <. N , z >. ) ` N ) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) )
51 50 eqeq2d 
 |-  ( z = ( 1st ` y ) -> ( (/) = ( rec ( F , <. N , z >. ) ` N ) <-> (/) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) ) )
52 51 anbi2d 
 |-  ( z = ( 1st ` y ) -> ( ( N e. _om /\ (/) = ( rec ( F , <. N , z >. ) ` N ) ) <-> ( N e. _om /\ (/) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) ) ) )
53 1 dffinxpf 
 |-  ( U ^^ N ) = { z | ( N e. _om /\ (/) = ( rec ( F , <. N , z >. ) ` N ) ) }
54 46 52 53 elab2 
 |-  ( ( 1st ` y ) e. ( U ^^ N ) <-> ( N e. _om /\ (/) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) ) )
55 54 baib 
 |-  ( N e. _om -> ( ( 1st ` y ) e. ( U ^^ N ) <-> (/) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) ) )
56 55 ad2antrr 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> ( ( 1st ` y ) e. ( U ^^ N ) <-> (/) = ( rec ( F , <. N , ( 1st ` y ) >. ) ` N ) ) )
57 40 45 56 3bitr4d 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> ( y e. ( U ^^ suc N ) <-> ( 1st ` y ) e. ( U ^^ N ) ) )
58 57 biimpd 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( _V X. U ) ) -> ( y e. ( U ^^ suc N ) -> ( 1st ` y ) e. ( U ^^ N ) ) )
59 58 impancom 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( U ^^ suc N ) ) -> ( y e. ( _V X. U ) -> ( 1st ` y ) e. ( U ^^ N ) ) )
60 20 59 mpd 
 |-  ( ( ( N e. _om /\ 1o C_ N ) /\ y e. ( U ^^ suc N ) ) -> ( 1st ` y ) e. ( U ^^ N ) )
61 60 ex 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( y e. ( U ^^ suc N ) -> ( 1st ` y ) e. ( U ^^ N ) ) )
62 20 ex 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( y e. ( U ^^ suc N ) -> y e. ( _V X. U ) ) )
63 61 62 jcad 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( y e. ( U ^^ suc N ) -> ( ( 1st ` y ) e. ( U ^^ N ) /\ y e. ( _V X. U ) ) ) )
64 57 exbiri 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( y e. ( _V X. U ) -> ( ( 1st ` y ) e. ( U ^^ N ) -> y e. ( U ^^ suc N ) ) ) )
65 64 impd 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( ( y e. ( _V X. U ) /\ ( 1st ` y ) e. ( U ^^ N ) ) -> y e. ( U ^^ suc N ) ) )
66 65 ancomsd 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( ( ( 1st ` y ) e. ( U ^^ N ) /\ y e. ( _V X. U ) ) -> y e. ( U ^^ suc N ) ) )
67 63 66 impbid 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( y e. ( U ^^ suc N ) <-> ( ( 1st ` y ) e. ( U ^^ N ) /\ y e. ( _V X. U ) ) ) )
68 elxp8 
 |-  ( y e. ( ( U ^^ N ) X. U ) <-> ( ( 1st ` y ) e. ( U ^^ N ) /\ y e. ( _V X. U ) ) )
69 67 68 bitr4di 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( y e. ( U ^^ suc N ) <-> y e. ( ( U ^^ N ) X. U ) ) )
70 69 eqrdv 
 |-  ( ( N e. _om /\ 1o C_ N ) -> ( U ^^ suc N ) = ( ( U ^^ N ) X. U ) )