Metamath Proof Explorer

Theorem aomclem7

Description: Lemma for dfac11 . ( R1A ) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem6.b 
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }
aomclem6.c 
|- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
aomclem6.d 
|- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )
aomclem6.e 
|- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }
aomclem6.f 
|- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }
aomclem6.g 
|- G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )
aomclem6.h 
|- H = recs ( ( z e. _V |-> G ) )
aomclem6.a 
|- ( ph -> A e. On )
aomclem6.y 
|- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
Assertion aomclem7 
|- ( ph -> E. b b We ( R1 ` A ) )

Proof

Step Hyp Ref Expression
1 aomclem6.b 
 |-  B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }
2 aomclem6.c 
 |-  C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
3 aomclem6.d 
 |-  D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )
4 aomclem6.e 
 |-  E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }
5 aomclem6.f 
 |-  F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }
6 aomclem6.g 
 |-  G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )
7 aomclem6.h 
 |-  H = recs ( ( z e. _V |-> G ) )
8 aomclem6.a 
 |-  ( ph -> A e. On )
9 aomclem6.y 
 |-  ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
10 1 2 3 4 5 6 7 8 9 aomclem6 
 |-  ( ph -> ( H ` A ) We ( R1 ` A ) )
11 fvex 
 |-  ( H ` A ) e. _V
12 weeq1 
 |-  ( b = ( H ` A ) -> ( b We ( R1 ` A ) <-> ( H ` A ) We ( R1 ` A ) ) )
13 11 12 spcev 
 |-  ( ( H ` A ) We ( R1 ` A ) -> E. b b We ( R1 ` A ) )
14 10 13 syl 
 |-  ( ph -> E. b b We ( R1 ` A ) )