Theorem isf32lem5

Description: Lemma for isfin3-2 . There are infinite decrease points. (Contributed by Stefan O'Rear, 5-Nov-2014)

	Ref	Expression
Hypotheses	isf32lem.a	|- ( ph -> F : _om --> ~P G )
	isf32lem.b	|- ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
	isf32lem.c	|- ( ph -> -. |^| ran F e. ran F )
	isf32lem.d	|- S = { y e. _om | ( F ` suc y ) C. ( F ` y ) }
Assertion	isf32lem5	|- ( ph -> -. S e. Fin )

Proof

Step	Hyp	Ref	Expression
1		isf32lem.a	|- ( ph -> F : _om --> ~P G )
2		isf32lem.b	|- ( ph -> A. x e. _om ( F ` suc x ) C_ ( F ` x ) )
3		isf32lem.c	|- ( ph -> -. |^| ran F e. ran F )
4		isf32lem.d	|- S = { y e. _om | ( F ` suc y ) C. ( F ` y ) }
5	1 2 3	isf32lem2	|- ( ( ph /\ a e. _om ) -> E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
6	5	ralrimiva	|- ( ph -> A. a e. _om E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
7	4	ssrab3	|- S C_ _om
8		nnunifi	|- ( ( S C_ _om /\ S e. Fin ) -> U. S e. _om )
9	7 8	mpan	|- ( S e. Fin -> U. S e. _om )
10	9	adantl	|- ( ( ph /\ S e. Fin ) -> U. S e. _om )
11		elssuni	|- ( b e. S -> b C_ U. S )
12		nnon	|- ( b e. _om -> b e. On )
13		omsson	|- _om C_ On
14	13 10	sselid	|- ( ( ph /\ S e. Fin ) -> U. S e. On )
15		ontri1	|- ( ( b e. On /\ U. S e. On ) -> ( b C_ U. S <-> -. U. S e. b ) )
16	12 14 15	syl2anr	|- ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> ( b C_ U. S <-> -. U. S e. b ) )
17	11 16	imbitrid	|- ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> ( b e. S -> -. U. S e. b ) )
18	17	con2d	|- ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> ( U. S e. b -> -. b e. S ) )
19	18	impr	|- ( ( ( ph /\ S e. Fin ) /\ ( b e. _om /\ U. S e. b ) ) -> -. b e. S )
20	4	eleq2i	|- ( b e. S <-> b e. { y e. _om | ( F ` suc y ) C. ( F ` y ) } )
21	19 20	sylnib	|- ( ( ( ph /\ S e. Fin ) /\ ( b e. _om /\ U. S e. b ) ) -> -. b e. { y e. _om | ( F ` suc y ) C. ( F ` y ) } )
22		suceq	|- ( y = b -> suc y = suc b )
23	22	fveq2d	|- ( y = b -> ( F ` suc y ) = ( F ` suc b ) )
24		fveq2	|- ( y = b -> ( F ` y ) = ( F ` b ) )
25	23 24	psseq12d	|- ( y = b -> ( ( F ` suc y ) C. ( F ` y ) <-> ( F ` suc b ) C. ( F ` b ) ) )
26	25	elrab3	|- ( b e. _om -> ( b e. { y e. _om | ( F ` suc y ) C. ( F ` y ) } <-> ( F ` suc b ) C. ( F ` b ) ) )
27	26	ad2antrl	|- ( ( ( ph /\ S e. Fin ) /\ ( b e. _om /\ U. S e. b ) ) -> ( b e. { y e. _om | ( F ` suc y ) C. ( F ` y ) } <-> ( F ` suc b ) C. ( F ` b ) ) )
28	21 27	mtbid	|- ( ( ( ph /\ S e. Fin ) /\ ( b e. _om /\ U. S e. b ) ) -> -. ( F ` suc b ) C. ( F ` b ) )
29	28	expr	|- ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> ( U. S e. b -> -. ( F ` suc b ) C. ( F ` b ) ) )
30		imnan	|- ( ( U. S e. b -> -. ( F ` suc b ) C. ( F ` b ) ) <-> -. ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
31	29 30	sylib	|- ( ( ( ph /\ S e. Fin ) /\ b e. _om ) -> -. ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
32	31	nrexdv	|- ( ( ph /\ S e. Fin ) -> -. E. b e. _om ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
33		eleq1	|- ( a = U. S -> ( a e. b <-> U. S e. b ) )
34	33	anbi1d	|- ( a = U. S -> ( ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) <-> ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) )
35	34	rexbidv	|- ( a = U. S -> ( E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) <-> E. b e. _om ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) )
36	35	notbid	|- ( a = U. S -> ( -. E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) <-> -. E. b e. _om ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) )
37	36	rspcev	|- ( ( U. S e. _om /\ -. E. b e. _om ( U. S e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) -> E. a e. _om -. E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
38	10 32 37	syl2anc	|- ( ( ph /\ S e. Fin ) -> E. a e. _om -. E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
39		rexnal	|- ( E. a e. _om -. E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) <-> -. A. a e. _om E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
40	38 39	sylib	|- ( ( ph /\ S e. Fin ) -> -. A. a e. _om E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) )
41	40	ex	|- ( ph -> ( S e. Fin -> -. A. a e. _om E. b e. _om ( a e. b /\ ( F ` suc b ) C. ( F ` b ) ) ) )
42	6 41	mt2d	|- ( ph -> -. S e. Fin )