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 ) )