Metamath Proof Explorer

Theorem aomclem3

Description: Lemma for dfac11 . Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 aomclem3.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 aomclem3.c 
 |-  C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )
3 aomclem3.d 
 |-  D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )
4 aomclem3.e 
 |-  E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }
5 aomclem3.on 
 |-  ( ph -> dom z e. On )
6 aomclem3.su 
 |-  ( ph -> dom z = suc U. dom z )
7 aomclem3.we 
 |-  ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )
8 aomclem3.a 
 |-  ( ph -> A e. On )
9 aomclem3.za 
 |-  ( ph -> dom z C_ A )
10 aomclem3.y 
 |-  ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )
11 rneq 
 |-  ( a = c -> ran a = ran c )
12 11 difeq2d 
 |-  ( a = c -> ( ( R1 ` dom z ) \ ran a ) = ( ( R1 ` dom z ) \ ran c ) )
13 12 fveq2d 
 |-  ( a = c -> ( C ` ( ( R1 ` dom z ) \ ran a ) ) = ( C ` ( ( R1 ` dom z ) \ ran c ) ) )
14 13 cbvmptv 
 |-  ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) = ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) )
15 recseq 
 |-  ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) = ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) -> recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) ) = recs ( ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) ) )
16 14 15 ax-mp 
 |-  recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) ) = recs ( ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) )
17 3 16 eqtri 
 |-  D = recs ( ( c e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran c ) ) ) )
18 fvexd 
 |-  ( ph -> ( R1 ` dom z ) e. _V )
19 1 2 5 6 7 8 9 10 aomclem2 
 |-  ( ph -> A. a e. ~P ( R1 ` dom z ) ( a =/= (/) -> ( C ` a ) e. a ) )
20 neeq1 
 |-  ( a = d -> ( a =/= (/) <-> d =/= (/) ) )
21 fveq2 
 |-  ( a = d -> ( C ` a ) = ( C ` d ) )
22 id 
 |-  ( a = d -> a = d )
23 21 22 eleq12d 
 |-  ( a = d -> ( ( C ` a ) e. a <-> ( C ` d ) e. d ) )
24 20 23 imbi12d 
 |-  ( a = d -> ( ( a =/= (/) -> ( C ` a ) e. a ) <-> ( d =/= (/) -> ( C ` d ) e. d ) ) )
25 24 cbvralvw 
 |-  ( A. a e. ~P ( R1 ` dom z ) ( a =/= (/) -> ( C ` a ) e. a ) <-> A. d e. ~P ( R1 ` dom z ) ( d =/= (/) -> ( C ` d ) e. d ) )
26 19 25 sylib 
 |-  ( ph -> A. d e. ~P ( R1 ` dom z ) ( d =/= (/) -> ( C ` d ) e. d ) )
27 17 18 26 4 dnwech 
 |-  ( ph -> E We ( R1 ` dom z ) )