Metamath Proof Explorer

Theorem fseqen

Description: A set that is equinumerous to its Cartesian product is equinumerous to the set of finite sequences on it. (This can be proven more easily using some choice but this proof avoids it.) (Contributed by Mario Carneiro, 18-Nov-2014)

Ref Expression
Assertion fseqen 
|- ( ( ( A X. A ) ~~ A /\ A =/= (/) ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( ( A X. A ) ~~ A <-> E. f f : ( A X. A ) -1-1-onto-> A )
2 n0 
 |-  ( A =/= (/) <-> E. b b e. A )
3 exdistrv 
 |-  ( E. f E. b ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) <-> ( E. f f : ( A X. A ) -1-1-onto-> A /\ E. b b e. A ) )
4 omex 
 |-  _om e. _V
5 simpl 
 |-  ( ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> f : ( A X. A ) -1-1-onto-> A )
6 f1ofo 
 |-  ( f : ( A X. A ) -1-1-onto-> A -> f : ( A X. A ) -onto-> A )
7 forn 
 |-  ( f : ( A X. A ) -onto-> A -> ran f = A )
8 5 6 7 3syl 
 |-  ( ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> ran f = A )
9 vex 
 |-  f e. _V
10 9 rnex 
 |-  ran f e. _V
11 8 10 eqeltrrdi 
 |-  ( ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> A e. _V )
12 xpexg 
 |-  ( ( _om e. _V /\ A e. _V ) -> ( _om X. A ) e. _V )
13 4 11 12 sylancr 
 |-  ( ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> ( _om X. A ) e. _V )
14 simpr 
 |-  ( ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> b e. A )
15 eqid 
 |-  seqom ( ( k e. _V , g e. _V |-> ( y e. ( A ^m suc k ) |-> ( ( g ` ( y |` k ) ) f ( y ` k ) ) ) ) , { <. (/) , b >. } ) = seqom ( ( k e. _V , g e. _V |-> ( y e. ( A ^m suc k ) |-> ( ( g ` ( y |` k ) ) f ( y ` k ) ) ) ) , { <. (/) , b >. } )
16 eqid 
 |-  ( x e. U_ n e. _om ( A ^m n ) |-> <. dom x , ( ( seqom ( ( k e. _V , g e. _V |-> ( y e. ( A ^m suc k ) |-> ( ( g ` ( y |` k ) ) f ( y ` k ) ) ) ) , { <. (/) , b >. } ) ` dom x ) ` x ) >. ) = ( x e. U_ n e. _om ( A ^m n ) |-> <. dom x , ( ( seqom ( ( k e. _V , g e. _V |-> ( y e. ( A ^m suc k ) |-> ( ( g ` ( y |` k ) ) f ( y ` k ) ) ) ) , { <. (/) , b >. } ) ` dom x ) ` x ) >. )
17 11 14 5 15 16 fseqenlem2 
 |-  ( ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> ( x e. U_ n e. _om ( A ^m n ) |-> <. dom x , ( ( seqom ( ( k e. _V , g e. _V |-> ( y e. ( A ^m suc k ) |-> ( ( g ` ( y |` k ) ) f ( y ` k ) ) ) ) , { <. (/) , b >. } ) ` dom x ) ` x ) >. ) : U_ n e. _om ( A ^m n ) -1-1-> ( _om X. A ) )
18 f1domg 
 |-  ( ( _om X. A ) e. _V -> ( ( x e. U_ n e. _om ( A ^m n ) |-> <. dom x , ( ( seqom ( ( k e. _V , g e. _V |-> ( y e. ( A ^m suc k ) |-> ( ( g ` ( y |` k ) ) f ( y ` k ) ) ) ) , { <. (/) , b >. } ) ` dom x ) ` x ) >. ) : U_ n e. _om ( A ^m n ) -1-1-> ( _om X. A ) -> U_ n e. _om ( A ^m n ) ~<_ ( _om X. A ) ) )
19 13 17 18 sylc 
 |-  ( ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> U_ n e. _om ( A ^m n ) ~<_ ( _om X. A ) )
20 fseqdom 
 |-  ( A e. _V -> ( _om X. A ) ~<_ U_ n e. _om ( A ^m n ) )
21 11 20 syl 
 |-  ( ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> ( _om X. A ) ~<_ U_ n e. _om ( A ^m n ) )
22 sbth 
 |-  ( ( U_ n e. _om ( A ^m n ) ~<_ ( _om X. A ) /\ ( _om X. A ) ~<_ U_ n e. _om ( A ^m n ) ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) )
23 19 21 22 syl2anc 
 |-  ( ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) )
24 23 exlimivv 
 |-  ( E. f E. b ( f : ( A X. A ) -1-1-onto-> A /\ b e. A ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) )
25 3 24 sylbir 
 |-  ( ( E. f f : ( A X. A ) -1-1-onto-> A /\ E. b b e. A ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) )
26 1 2 25 syl2anb 
 |-  ( ( ( A X. A ) ~~ A /\ A =/= (/) ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) )