Metamath Proof Explorer

Theorem hsmexlem6

Description: Lemma for hsmex . (Contributed by Stefan O'Rear, 14-Feb-2015)

Ref Expression
Hypotheses hsmexlem4.x 
|- X e. _V
hsmexlem4.h 
|- H = ( rec ( ( z e. _V |-> ( har ` ~P ( X X. z ) ) ) , ( har ` ~P X ) ) |` _om )
hsmexlem4.u 
|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
hsmexlem4.s 
|- S = { a e. U. ( R1 " On ) | A. b e. ( TC ` { a } ) b ~<_ X }
hsmexlem4.o 
|- O = OrdIso ( _E , ( rank " ( ( U ` d ) ` c ) ) )
Assertion hsmexlem6 
|- S e. _V

Proof

Step Hyp Ref Expression
1 hsmexlem4.x 
 |-  X e. _V
2 hsmexlem4.h 
 |-  H = ( rec ( ( z e. _V |-> ( har ` ~P ( X X. z ) ) ) , ( har ` ~P X ) ) |` _om )
3 hsmexlem4.u 
 |-  U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
4 hsmexlem4.s 
 |-  S = { a e. U. ( R1 " On ) | A. b e. ( TC ` { a } ) b ~<_ X }
5 hsmexlem4.o 
 |-  O = OrdIso ( _E , ( rank " ( ( U ` d ) ` c ) ) )
6 fvex 
 |-  ( R1 ` ( har ` ~P ( _om X. U. ran H ) ) ) e. _V
7 1 2 3 4 5 hsmexlem5 
 |-  ( d e. S -> ( rank ` d ) e. ( har ` ~P ( _om X. U. ran H ) ) )
8 4 ssrab3 
 |-  S C_ U. ( R1 " On )
9 8 sseli 
 |-  ( d e. S -> d e. U. ( R1 " On ) )
10 harcl 
 |-  ( har ` ~P ( _om X. U. ran H ) ) e. On
11 r1fnon 
 |-  R1 Fn On
12 11 fndmi 
 |-  dom R1 = On
13 10 12 eleqtrri 
 |-  ( har ` ~P ( _om X. U. ran H ) ) e. dom R1
14 rankr1ag 
 |-  ( ( d e. U. ( R1 " On ) /\ ( har ` ~P ( _om X. U. ran H ) ) e. dom R1 ) -> ( d e. ( R1 ` ( har ` ~P ( _om X. U. ran H ) ) ) <-> ( rank ` d ) e. ( har ` ~P ( _om X. U. ran H ) ) ) )
15 9 13 14 sylancl 
 |-  ( d e. S -> ( d e. ( R1 ` ( har ` ~P ( _om X. U. ran H ) ) ) <-> ( rank ` d ) e. ( har ` ~P ( _om X. U. ran H ) ) ) )
16 7 15 mpbird 
 |-  ( d e. S -> d e. ( R1 ` ( har ` ~P ( _om X. U. ran H ) ) ) )
17 16 ssriv 
 |-  S C_ ( R1 ` ( har ` ~P ( _om X. U. ran H ) ) )
18 6 17 ssexi 
 |-  S e. _V