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

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 ) )