Metamath Proof Explorer

Theorem harwdom

Description: The value of the Hartogs function at a set X is weakly dominated by ~P ( X X. X ) . This follows from a more precise analysis of the bound used in hartogs to prove that ( harX ) is an ordinal. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion harwdom 
|- ( X e. V -> ( har ` X ) ~<_* ~P ( X X. X ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } = { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
2 eqid 
 |-  { <. s , t >. | E. w e. y E. z e. y ( ( s = ( f ` w ) /\ t = ( f ` z ) ) /\ w _E z ) } = { <. s , t >. | E. w e. y E. z e. y ( ( s = ( f ` w ) /\ t = ( f ` z ) ) /\ w _E z ) }
3 1 2 hartogslem1 
 |-  ( dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } C_ ~P ( X X. X ) /\ Fun { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } /\ ( X e. V -> ran { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } = { x e. On | x ~<_ X } ) )
4 3 simp2i 
 |-  Fun { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
5 3 simp1i 
 |-  dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } C_ ~P ( X X. X )
6 sqxpexg 
 |-  ( X e. V -> ( X X. X ) e. _V )
7 6 pwexd 
 |-  ( X e. V -> ~P ( X X. X ) e. _V )
8 ssexg 
 |-  ( ( dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } C_ ~P ( X X. X ) /\ ~P ( X X. X ) e. _V ) -> dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } e. _V )
9 5 7 8 sylancr 
 |-  ( X e. V -> dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } e. _V )
10 funex 
 |-  ( ( Fun { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } /\ dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } e. _V ) -> { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } e. _V )
11 4 9 10 sylancr 
 |-  ( X e. V -> { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } e. _V )
12 funfn 
 |-  ( Fun { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } <-> { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } Fn dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } )
13 4 12 mpbi 
 |-  { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } Fn dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) }
14 13 a1i 
 |-  ( X e. V -> { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } Fn dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } )
15 3 simp3i 
 |-  ( X e. V -> ran { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } = { x e. On | x ~<_ X } )
16 harval 
 |-  ( X e. V -> ( har ` X ) = { x e. On | x ~<_ X } )
17 15 16 eqtr4d 
 |-  ( X e. V -> ran { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } = ( har ` X ) )
18 df-fo 
 |-  ( { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } : dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } -onto-> ( har ` X ) <-> ( { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } Fn dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } /\ ran { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } = ( har ` X ) ) )
19 14 17 18 sylanbrc 
 |-  ( X e. V -> { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } : dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } -onto-> ( har ` X ) )
20 fowdom 
 |-  ( ( { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } e. _V /\ { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } : dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } -onto-> ( har ` X ) ) -> ( har ` X ) ~<_* dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } )
21 11 19 20 syl2anc 
 |-  ( X e. V -> ( har ` X ) ~<_* dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } )
22 ssdomg 
 |-  ( ~P ( X X. X ) e. _V -> ( dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } C_ ~P ( X X. X ) -> dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } ~<_ ~P ( X X. X ) ) )
23 7 5 22 mpisyl 
 |-  ( X e. V -> dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } ~<_ ~P ( X X. X ) )
24 domwdom 
 |-  ( dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } ~<_ ~P ( X X. X ) -> dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } ~<_* ~P ( X X. X ) )
25 23 24 syl 
 |-  ( X e. V -> dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } ~<_* ~P ( X X. X ) )
26 wdomtr 
 |-  ( ( ( har ` X ) ~<_* dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } /\ dom { <. r , y >. | ( ( ( dom r C_ X /\ ( _I |` dom r ) C_ r /\ r C_ ( dom r X. dom r ) ) /\ ( r \ _I ) We dom r ) /\ y = dom OrdIso ( ( r \ _I ) , dom r ) ) } ~<_* ~P ( X X. X ) ) -> ( har ` X ) ~<_* ~P ( X X. X ) )
27 21 25 26 syl2anc 
 |-  ( X e. V -> ( har ` X ) ~<_* ~P ( X X. X ) )