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

Metamath Proof Explorer

Theorem aomclem3

Proof