Metamath Proof Explorer

Theorem fseqdom

Description: One half of fseqen . (Contributed by Mario Carneiro, 18-Nov-2014)

Ref Expression
Assertion fseqdom 
|- ( A e. V -> ( _om X. A ) ~<_ U_ n e. _om ( A ^m n ) )

Proof

Step Hyp Ref Expression
1 omex 
 |-  _om e. _V
2 ovex 
 |-  ( A ^m n ) e. _V
3 1 2 iunex 
 |-  U_ n e. _om ( A ^m n ) e. _V
4 xp1st 
 |-  ( x e. ( _om X. A ) -> ( 1st ` x ) e. _om )
5 peano2 
 |-  ( ( 1st ` x ) e. _om -> suc ( 1st ` x ) e. _om )
6 4 5 syl 
 |-  ( x e. ( _om X. A ) -> suc ( 1st ` x ) e. _om )
7 xp2nd 
 |-  ( x e. ( _om X. A ) -> ( 2nd ` x ) e. A )
8 fconst6g 
 |-  ( ( 2nd ` x ) e. A -> ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) : suc ( 1st ` x ) --> A )
9 7 8 syl 
 |-  ( x e. ( _om X. A ) -> ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) : suc ( 1st ` x ) --> A )
10 9 adantl 
 |-  ( ( A e. V /\ x e. ( _om X. A ) ) -> ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) : suc ( 1st ` x ) --> A )
11 elmapg 
 |-  ( ( A e. V /\ suc ( 1st ` x ) e. _om ) -> ( ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) e. ( A ^m suc ( 1st ` x ) ) <-> ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) : suc ( 1st ` x ) --> A ) )
12 6 11 sylan2 
 |-  ( ( A e. V /\ x e. ( _om X. A ) ) -> ( ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) e. ( A ^m suc ( 1st ` x ) ) <-> ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) : suc ( 1st ` x ) --> A ) )
13 10 12 mpbird 
 |-  ( ( A e. V /\ x e. ( _om X. A ) ) -> ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) e. ( A ^m suc ( 1st ` x ) ) )
14 oveq2 
 |-  ( n = suc ( 1st ` x ) -> ( A ^m n ) = ( A ^m suc ( 1st ` x ) ) )
15 14 eliuni 
 |-  ( ( suc ( 1st ` x ) e. _om /\ ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) e. ( A ^m suc ( 1st ` x ) ) ) -> ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) e. U_ n e. _om ( A ^m n ) )
16 6 13 15 syl2an2 
 |-  ( ( A e. V /\ x e. ( _om X. A ) ) -> ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) e. U_ n e. _om ( A ^m n ) )
17 16 ex 
 |-  ( A e. V -> ( x e. ( _om X. A ) -> ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) e. U_ n e. _om ( A ^m n ) ) )
18 nsuceq0 
 |-  suc ( 1st ` x ) =/= (/)
19 fvex 
 |-  ( 2nd ` x ) e. _V
20 19 snnz 
 |-  { ( 2nd ` x ) } =/= (/)
21 xp11 
 |-  ( ( suc ( 1st ` x ) =/= (/) /\ { ( 2nd ` x ) } =/= (/) ) -> ( ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) = ( suc ( 1st ` y ) X. { ( 2nd ` y ) } ) <-> ( suc ( 1st ` x ) = suc ( 1st ` y ) /\ { ( 2nd ` x ) } = { ( 2nd ` y ) } ) ) )
22 18 20 21 mp2an 
 |-  ( ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) = ( suc ( 1st ` y ) X. { ( 2nd ` y ) } ) <-> ( suc ( 1st ` x ) = suc ( 1st ` y ) /\ { ( 2nd ` x ) } = { ( 2nd ` y ) } ) )
23 xp1st 
 |-  ( y e. ( _om X. A ) -> ( 1st ` y ) e. _om )
24 peano4 
 |-  ( ( ( 1st ` x ) e. _om /\ ( 1st ` y ) e. _om ) -> ( suc ( 1st ` x ) = suc ( 1st ` y ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
25 4 23 24 syl2an 
 |-  ( ( x e. ( _om X. A ) /\ y e. ( _om X. A ) ) -> ( suc ( 1st ` x ) = suc ( 1st ` y ) <-> ( 1st ` x ) = ( 1st ` y ) ) )
26 sneqbg 
 |-  ( ( 2nd ` x ) e. _V -> ( { ( 2nd ` x ) } = { ( 2nd ` y ) } <-> ( 2nd ` x ) = ( 2nd ` y ) ) )
27 19 26 mp1i 
 |-  ( ( x e. ( _om X. A ) /\ y e. ( _om X. A ) ) -> ( { ( 2nd ` x ) } = { ( 2nd ` y ) } <-> ( 2nd ` x ) = ( 2nd ` y ) ) )
28 25 27 anbi12d 
 |-  ( ( x e. ( _om X. A ) /\ y e. ( _om X. A ) ) -> ( ( suc ( 1st ` x ) = suc ( 1st ` y ) /\ { ( 2nd ` x ) } = { ( 2nd ` y ) } ) <-> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) ) )
29 22 28 syl5bb 
 |-  ( ( x e. ( _om X. A ) /\ y e. ( _om X. A ) ) -> ( ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) = ( suc ( 1st ` y ) X. { ( 2nd ` y ) } ) <-> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) ) )
30 xpopth 
 |-  ( ( x e. ( _om X. A ) /\ y e. ( _om X. A ) ) -> ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) <-> x = y ) )
31 29 30 bitrd 
 |-  ( ( x e. ( _om X. A ) /\ y e. ( _om X. A ) ) -> ( ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) = ( suc ( 1st ` y ) X. { ( 2nd ` y ) } ) <-> x = y ) )
32 31 a1i 
 |-  ( A e. V -> ( ( x e. ( _om X. A ) /\ y e. ( _om X. A ) ) -> ( ( suc ( 1st ` x ) X. { ( 2nd ` x ) } ) = ( suc ( 1st ` y ) X. { ( 2nd ` y ) } ) <-> x = y ) ) )
33 17 32 dom2d 
 |-  ( A e. V -> ( U_ n e. _om ( A ^m n ) e. _V -> ( _om X. A ) ~<_ U_ n e. _om ( A ^m n ) ) )
34 3 33 mpi 
 |-  ( A e. V -> ( _om X. A ) ~<_ U_ n e. _om ( A ^m n ) )