Metamath Proof Explorer

Theorem abrexdomjm

Description: An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypothesis abrexdomjm.1 
|- ( y e. A -> E* x ph )
Assertion abrexdomjm 
|- ( A e. V -> { x | E. y e. A ph } ~<_ A )

Proof

Step Hyp Ref Expression
1 abrexdomjm.1 
 |-  ( y e. A -> E* x ph )
2 df-rex 
 |-  ( E. y e. A ph <-> E. y ( y e. A /\ ph ) )
3 2 abbii 
 |-  { x | E. y e. A ph } = { x | E. y ( y e. A /\ ph ) }
4 rnopab 
 |-  ran { <. y , x >. | ( y e. A /\ ph ) } = { x | E. y ( y e. A /\ ph ) }
5 3 4 eqtr4i 
 |-  { x | E. y e. A ph } = ran { <. y , x >. | ( y e. A /\ ph ) }
6 dmopabss 
 |-  dom { <. y , x >. | ( y e. A /\ ph ) } C_ A
7 ssexg 
 |-  ( ( dom { <. y , x >. | ( y e. A /\ ph ) } C_ A /\ A e. V ) -> dom { <. y , x >. | ( y e. A /\ ph ) } e. _V )
8 6 7 mpan 
 |-  ( A e. V -> dom { <. y , x >. | ( y e. A /\ ph ) } e. _V )
9 funopab 
 |-  ( Fun { <. y , x >. | ( y e. A /\ ph ) } <-> A. y E* x ( y e. A /\ ph ) )
10 moanimv 
 |-  ( E* x ( y e. A /\ ph ) <-> ( y e. A -> E* x ph ) )
11 1 10 mpbir 
 |-  E* x ( y e. A /\ ph )
12 9 11 mpgbir 
 |-  Fun { <. y , x >. | ( y e. A /\ ph ) }
13 12 a1i 
 |-  ( A e. V -> Fun { <. y , x >. | ( y e. A /\ ph ) } )
14 funfn 
 |-  ( Fun { <. y , x >. | ( y e. A /\ ph ) } <-> { <. y , x >. | ( y e. A /\ ph ) } Fn dom { <. y , x >. | ( y e. A /\ ph ) } )
15 13 14 sylib 
 |-  ( A e. V -> { <. y , x >. | ( y e. A /\ ph ) } Fn dom { <. y , x >. | ( y e. A /\ ph ) } )
16 fnrndomg 
 |-  ( dom { <. y , x >. | ( y e. A /\ ph ) } e. _V -> ( { <. y , x >. | ( y e. A /\ ph ) } Fn dom { <. y , x >. | ( y e. A /\ ph ) } -> ran { <. y , x >. | ( y e. A /\ ph ) } ~<_ dom { <. y , x >. | ( y e. A /\ ph ) } ) )
17 8 15 16 sylc 
 |-  ( A e. V -> ran { <. y , x >. | ( y e. A /\ ph ) } ~<_ dom { <. y , x >. | ( y e. A /\ ph ) } )
18 ssdomg 
 |-  ( A e. V -> ( dom { <. y , x >. | ( y e. A /\ ph ) } C_ A -> dom { <. y , x >. | ( y e. A /\ ph ) } ~<_ A ) )
19 6 18 mpi 
 |-  ( A e. V -> dom { <. y , x >. | ( y e. A /\ ph ) } ~<_ A )
20 domtr 
 |-  ( ( ran { <. y , x >. | ( y e. A /\ ph ) } ~<_ dom { <. y , x >. | ( y e. A /\ ph ) } /\ dom { <. y , x >. | ( y e. A /\ ph ) } ~<_ A ) -> ran { <. y , x >. | ( y e. A /\ ph ) } ~<_ A )
21 17 19 20 syl2anc 
 |-  ( A e. V -> ran { <. y , x >. | ( y e. A /\ ph ) } ~<_ A )
22 5 21 eqbrtrid 
 |-  ( A e. V -> { x | E. y e. A ph } ~<_ A )