Metamath Proof Explorer

Theorem aomclem5

Description: Lemma for dfac11 . Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 aomclem5.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 aomclem5.c 
 |-  C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
3 aomclem5.d 
 |-  D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )
4 aomclem5.e 
 |-  E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }
5 aomclem5.f 
 |-  F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }
6 aomclem5.g 
 |-  G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )
7 aomclem5.on 
 |-  ( ph -> dom z e. On )
8 aomclem5.we 
 |-  ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
9 aomclem5.a 
 |-  ( ph -> A e. On )
10 aomclem5.za 
 |-  ( ph -> dom z C_ A )
11 aomclem5.y 
 |-  ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
12 7 adantr 
 |-  ( ( ph /\ dom z = U. dom z ) -> dom z e. On )
13 simpr 
 |-  ( ( ph /\ dom z = U. dom z ) -> dom z = U. dom z )
14 8 adantr 
 |-  ( ( ph /\ dom z = U. dom z ) -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
15 5 12 13 14 aomclem4 
 |-  ( ( ph /\ dom z = U. dom z ) -> F We ( R1 ` dom z ) )
16 iftrue 
 |-  ( dom z = U. dom z -> if ( dom z = U. dom z , F , E ) = F )
17 16 adantl 
 |-  ( ( ph /\ dom z = U. dom z ) -> if ( dom z = U. dom z , F , E ) = F )
18 eqidd 
 |-  ( ( ph /\ dom z = U. dom z ) -> ( R1 ` dom z ) = ( R1 ` dom z ) )
19 17 18 weeq12d 
 |-  ( ( ph /\ dom z = U. dom z ) -> ( if ( dom z = U. dom z , F , E ) We ( R1 ` dom z ) <-> F We ( R1 ` dom z ) ) )
20 15 19 mpbird 
 |-  ( ( ph /\ dom z = U. dom z ) -> if ( dom z = U. dom z , F , E ) We ( R1 ` dom z ) )
21 7 adantr 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> dom z e. On )
22 eloni 
 |-  ( dom z e. On -> Ord dom z )
23 orduniorsuc 
 |-  ( Ord dom z -> ( dom z = U. dom z \/ dom z = suc U. dom z ) )
24 7 22 23 3syl 
 |-  ( ph -> ( dom z = U. dom z \/ dom z = suc U. dom z ) )
25 24 orcanai 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> dom z = suc U. dom z )
26 8 adantr 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
27 9 adantr 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> A e. On )
28 10 adantr 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> dom z C_ A )
29 11 adantr 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
30 1 2 3 4 21 25 26 27 28 29 aomclem3 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> E We ( R1 ` dom z ) )
31 iffalse 
 |-  ( -. dom z = U. dom z -> if ( dom z = U. dom z , F , E ) = E )
32 31 adantl 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> if ( dom z = U. dom z , F , E ) = E )
33 eqidd 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> ( R1 ` dom z ) = ( R1 ` dom z ) )
34 32 33 weeq12d 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> ( if ( dom z = U. dom z , F , E ) We ( R1 ` dom z ) <-> E We ( R1 ` dom z ) ) )
35 30 34 mpbird 
 |-  ( ( ph /\ -. dom z = U. dom z ) -> if ( dom z = U. dom z , F , E ) We ( R1 ` dom z ) )
36 20 35 pm2.61dan 
 |-  ( ph -> if ( dom z = U. dom z , F , E ) We ( R1 ` dom z ) )
37 weinxp 
 |-  ( if ( dom z = U. dom z , F , E ) We ( R1 ` dom z ) <-> ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) ) We ( R1 ` dom z ) )
38 36 37 sylib 
 |-  ( ph -> ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) ) We ( R1 ` dom z ) )
39 weeq1 
 |-  ( G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) ) -> ( G We ( R1 ` dom z ) <-> ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) ) We ( R1 ` dom z ) ) )
40 6 39 ax-mp 
 |-  ( G We ( R1 ` dom z ) <-> ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) ) We ( R1 ` dom z ) )
41 38 40 sylibr 
 |-  ( ph -> G We ( R1 ` dom z ) )