Theorem mirimanoffr

Description: Relative version of mirimanoff (which corresponds to the case V =V ).

Note that the definition of M presupposes that om is available as a set ( omex ), which is equivalent to assuming ax-inf2 . (Contributed by Adrian Ducourtial, 13-Oct-2026)

	Ref	Expression
Hypothesis	mirimanoffr.1	|- M = { x e. V | -. E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) }
Assertion	mirimanoffr	|- M e/ V

Proof

Step	Hyp	Ref	Expression
1		mirimanoffr.1	|- M = { x e. V | -. E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) }
2		omex	|- _om e. _V
3	2	mptex	|- ( m e. _om |-> ( f ` suc m ) ) e. _V
4	3	a1i	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> ( m e. _om |-> ( f ` suc m ) ) e. _V )
5		fvex	|- ( f ` suc m ) e. _V
6		eqid	|- ( m e. _om |-> ( f ` suc m ) ) = ( m e. _om |-> ( f ` suc m ) )
7	5 6	fnmpti	|- ( m e. _om |-> ( f ` suc m ) ) Fn _om
8	7	a1i	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> ( m e. _om |-> ( f ` suc m ) ) Fn _om )
9		peano1	|- (/) e. _om
10		suceq	|- ( m = (/) -> suc m = suc (/) )
11	10	fveq2d	|- ( m = (/) -> ( f ` suc m ) = ( f ` suc (/) ) )
12		fvex	|- ( f ` suc (/) ) e. _V
13	11 6 12	fvmpt	|- ( (/) e. _om -> ( ( m e. _om |-> ( f ` suc m ) ) ` (/) ) = ( f ` suc (/) ) )
14	9 13	ax-mp	|- ( ( m e. _om |-> ( f ` suc m ) ) ` (/) ) = ( f ` suc (/) )
15	14	a1i	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> ( ( m e. _om |-> ( f ` suc m ) ) ` (/) ) = ( f ` suc (/) ) )
16		suceq	|- ( n = m -> suc n = suc m )
17	16	fveq2d	|- ( n = m -> ( f ` suc n ) = ( f ` suc m ) )
18		fveq2	|- ( n = m -> ( f ` n ) = ( f ` m ) )
19	17 18	eleq12d	|- ( n = m -> ( ( f ` suc n ) e. ( f ` n ) <-> ( f ` suc m ) e. ( f ` m ) ) )
20	19	cbvralvw	|- ( A. n e. _om ( f ` suc n ) e. ( f ` n ) <-> A. m e. _om ( f ` suc m ) e. ( f ` m ) )
21		suceq	|- ( m = suc n -> suc m = suc suc n )
22	21	fveq2d	|- ( m = suc n -> ( f ` suc m ) = ( f ` suc suc n ) )
23		fveq2	|- ( m = suc n -> ( f ` m ) = ( f ` suc n ) )
24	22 23	eleq12d	|- ( m = suc n -> ( ( f ` suc m ) e. ( f ` m ) <-> ( f ` suc suc n ) e. ( f ` suc n ) ) )
25	24	rspcv	|- ( suc n e. _om -> ( A. m e. _om ( f ` suc m ) e. ( f ` m ) -> ( f ` suc suc n ) e. ( f ` suc n ) ) )
26		peano2	|- ( n e. _om -> suc n e. _om )
27	25 26	syl11	|- ( A. m e. _om ( f ` suc m ) e. ( f ` m ) -> ( n e. _om -> ( f ` suc suc n ) e. ( f ` suc n ) ) )
28	27	3ad2ant3	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. m e. _om ( f ` suc m ) e. ( f ` m ) ) -> ( n e. _om -> ( f ` suc suc n ) e. ( f ` suc n ) ) )
29	28	imp	|- ( ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. m e. _om ( f ` suc m ) e. ( f ` m ) ) /\ n e. _om ) -> ( f ` suc suc n ) e. ( f ` suc n ) )
30		eqidd	|- ( n e. _om -> ( m e. _om |-> ( f ` suc m ) ) = ( m e. _om |-> ( f ` suc m ) ) )
31		fvexd	|- ( n e. _om -> ( f ` suc suc n ) e. _V )
32	22 30 26 31	fvmptd4	|- ( n e. _om -> ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) = ( f ` suc suc n ) )
33		suceq	|- ( m = n -> suc m = suc n )
34	33	fveq2d	|- ( m = n -> ( f ` suc m ) = ( f ` suc n ) )
35		fvex	|- ( f ` suc n ) e. _V
36	34 6 35	fvmpt	|- ( n e. _om -> ( ( m e. _om |-> ( f ` suc m ) ) ` n ) = ( f ` suc n ) )
37	32 36	eleq12d	|- ( n e. _om -> ( ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) e. ( ( m e. _om |-> ( f ` suc m ) ) ` n ) <-> ( f ` suc suc n ) e. ( f ` suc n ) ) )
38	37	adantl	|- ( ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. m e. _om ( f ` suc m ) e. ( f ` m ) ) /\ n e. _om ) -> ( ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) e. ( ( m e. _om |-> ( f ` suc m ) ) ` n ) <-> ( f ` suc suc n ) e. ( f ` suc n ) ) )
39	29 38	mpbird	|- ( ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. m e. _om ( f ` suc m ) e. ( f ` m ) ) /\ n e. _om ) -> ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) e. ( ( m e. _om |-> ( f ` suc m ) ) ` n ) )
40	39	ralrimiva	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. m e. _om ( f ` suc m ) e. ( f ` m ) ) -> A. n e. _om ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) e. ( ( m e. _om |-> ( f ` suc m ) ) ` n ) )
41	20 40	syl3an3b	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> A. n e. _om ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) e. ( ( m e. _om |-> ( f ` suc m ) ) ` n ) )
42	8 15 41	3jca	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> ( ( m e. _om |-> ( f ` suc m ) ) Fn _om /\ ( ( m e. _om |-> ( f ` suc m ) ) ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) e. ( ( m e. _om |-> ( f ` suc m ) ) ` n ) ) )
43		fneq1	|- ( g = ( m e. _om |-> ( f ` suc m ) ) -> ( g Fn _om <-> ( m e. _om |-> ( f ` suc m ) ) Fn _om ) )
44		fveq1	|- ( g = ( m e. _om |-> ( f ` suc m ) ) -> ( g ` (/) ) = ( ( m e. _om |-> ( f ` suc m ) ) ` (/) ) )
45	44	eqeq1d	|- ( g = ( m e. _om |-> ( f ` suc m ) ) -> ( ( g ` (/) ) = ( f ` suc (/) ) <-> ( ( m e. _om |-> ( f ` suc m ) ) ` (/) ) = ( f ` suc (/) ) ) )
46		fveq1	|- ( g = ( m e. _om |-> ( f ` suc m ) ) -> ( g ` suc n ) = ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) )
47		fveq1	|- ( g = ( m e. _om |-> ( f ` suc m ) ) -> ( g ` n ) = ( ( m e. _om |-> ( f ` suc m ) ) ` n ) )
48	46 47	eleq12d	|- ( g = ( m e. _om |-> ( f ` suc m ) ) -> ( ( g ` suc n ) e. ( g ` n ) <-> ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) e. ( ( m e. _om |-> ( f ` suc m ) ) ` n ) ) )
49	48	ralbidv	|- ( g = ( m e. _om |-> ( f ` suc m ) ) -> ( A. n e. _om ( g ` suc n ) e. ( g ` n ) <-> A. n e. _om ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) e. ( ( m e. _om |-> ( f ` suc m ) ) ` n ) ) )
50	43 45 49	3anbi123d	|- ( g = ( m e. _om |-> ( f ` suc m ) ) -> ( ( g Fn _om /\ ( g ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) <-> ( ( m e. _om |-> ( f ` suc m ) ) Fn _om /\ ( ( m e. _om |-> ( f ` suc m ) ) ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( ( m e. _om |-> ( f ` suc m ) ) ` suc n ) e. ( ( m e. _om |-> ( f ` suc m ) ) ` n ) ) ) )
51	4 42 50	spcedv	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> E. g ( g Fn _om /\ ( g ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) )
52		suceq	|- ( n = (/) -> suc n = suc (/) )
53	52	fveq2d	|- ( n = (/) -> ( f ` suc n ) = ( f ` suc (/) ) )
54		fveq2	|- ( n = (/) -> ( f ` n ) = ( f ` (/) ) )
55	53 54	eleq12d	|- ( n = (/) -> ( ( f ` suc n ) e. ( f ` n ) <-> ( f ` suc (/) ) e. ( f ` (/) ) ) )
56	55	rspcv	|- ( (/) e. _om -> ( A. n e. _om ( f ` suc n ) e. ( f ` n ) -> ( f ` suc (/) ) e. ( f ` (/) ) ) )
57	9 56	ax-mp	|- ( A. n e. _om ( f ` suc n ) e. ( f ` n ) -> ( f ` suc (/) ) e. ( f ` (/) ) )
58	57	3ad2ant3	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> ( f ` suc (/) ) e. ( f ` (/) ) )
59		eleq2	|- ( ( f ` (/) ) = M -> ( ( f ` suc (/) ) e. ( f ` (/) ) <-> ( f ` suc (/) ) e. M ) )
60	59	3ad2ant2	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> ( ( f ` suc (/) ) e. ( f ` (/) ) <-> ( f ` suc (/) ) e. M ) )
61	58 60	mpbid	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> ( f ` suc (/) ) e. M )
62		eqeq2	|- ( x = ( f ` suc (/) ) -> ( ( g ` (/) ) = x <-> ( g ` (/) ) = ( f ` suc (/) ) ) )
63	62	3anbi2d	|- ( x = ( f ` suc (/) ) -> ( ( g Fn _om /\ ( g ` (/) ) = x /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) <-> ( g Fn _om /\ ( g ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) ) )
64	63	exbidv	|- ( x = ( f ` suc (/) ) -> ( E. g ( g Fn _om /\ ( g ` (/) ) = x /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) <-> E. g ( g Fn _om /\ ( g ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) ) )
65	64	notbid	|- ( x = ( f ` suc (/) ) -> ( -. E. g ( g Fn _om /\ ( g ` (/) ) = x /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) <-> -. E. g ( g Fn _om /\ ( g ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) ) )
66		fneq1	|- ( f = g -> ( f Fn _om <-> g Fn _om ) )
67		fveq1	|- ( f = g -> ( f ` (/) ) = ( g ` (/) ) )
68	67	eqeq1d	|- ( f = g -> ( ( f ` (/) ) = x <-> ( g ` (/) ) = x ) )
69		fveq1	|- ( f = g -> ( f ` suc n ) = ( g ` suc n ) )
70		fveq1	|- ( f = g -> ( f ` n ) = ( g ` n ) )
71	69 70	eleq12d	|- ( f = g -> ( ( f ` suc n ) e. ( f ` n ) <-> ( g ` suc n ) e. ( g ` n ) ) )
72	71	ralbidv	|- ( f = g -> ( A. n e. _om ( f ` suc n ) e. ( f ` n ) <-> A. n e. _om ( g ` suc n ) e. ( g ` n ) ) )
73	66 68 72	3anbi123d	|- ( f = g -> ( ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) <-> ( g Fn _om /\ ( g ` (/) ) = x /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) ) )
74	73	cbvexvw	|- ( E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) <-> E. g ( g Fn _om /\ ( g ` (/) ) = x /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) )
75	74	notbii	|- ( -. E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) <-> -. E. g ( g Fn _om /\ ( g ` (/) ) = x /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) )
76	1 75	rabbieq	|- M = { x e. V | -. E. g ( g Fn _om /\ ( g ` (/) ) = x /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) }
77	65 76	elrab2	|- ( ( f ` suc (/) ) e. M <-> ( ( f ` suc (/) ) e. V /\ -. E. g ( g Fn _om /\ ( g ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) ) )
78	61 77	sylib	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> ( ( f ` suc (/) ) e. V /\ -. E. g ( g Fn _om /\ ( g ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) ) )
79	78	simprd	|- ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> -. E. g ( g Fn _om /\ ( g ` (/) ) = ( f ` suc (/) ) /\ A. n e. _om ( g ` suc n ) e. ( g ` n ) ) )
80	51 79	pm2.65i	|- -. ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) )
81	80	a1i	|- ( M e. V -> -. ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) )
82	81	nexdv	|- ( M e. V -> -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) )
83		pm2.24	|- ( M e. V -> ( -. M e. V -> -. -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
84		idd	|- ( M e. V -> ( -. -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) -> -. -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
85	2	mptex	|- ( m e. _om |-> M ) e. _V
86	85	isseti	|- E. f f = ( m e. _om |-> M )
87		simpl	|- ( ( M e. V /\ M e. M ) -> M e. V )
88	87	ralrimivw	|- ( ( M e. V /\ M e. M ) -> A. m e. _om M e. V )
89		eqid	|- ( m e. _om |-> M ) = ( m e. _om |-> M )
90	89	fnmpt	|- ( A. m e. _om M e. V -> ( m e. _om |-> M ) Fn _om )
91	88 90	syl	|- ( ( M e. V /\ M e. M ) -> ( m e. _om |-> M ) Fn _om )
92		eqidd	|- ( m = (/) -> M = M )
93	92 89	fvmptg	|- ( ( (/) e. _om /\ M e. V ) -> ( ( m e. _om |-> M ) ` (/) ) = M )
94	9 87 93	sylancr	|- ( ( M e. V /\ M e. M ) -> ( ( m e. _om |-> M ) ` (/) ) = M )
95		eqidd	|- ( m = suc n -> M = M )
96	95 89	fvmptg	|- ( ( suc n e. _om /\ M e. V ) -> ( ( m e. _om |-> M ) ` suc n ) = M )
97	26 96	sylan	|- ( ( n e. _om /\ M e. V ) -> ( ( m e. _om |-> M ) ` suc n ) = M )
98		eqidd	|- ( m = n -> M = M )
99	98 89	fvmptg	|- ( ( n e. _om /\ M e. V ) -> ( ( m e. _om |-> M ) ` n ) = M )
100	97 99	eleq12d	|- ( ( n e. _om /\ M e. V ) -> ( ( ( m e. _om |-> M ) ` suc n ) e. ( ( m e. _om |-> M ) ` n ) <-> M e. M ) )
101	100	biimprd	|- ( ( n e. _om /\ M e. V ) -> ( M e. M -> ( ( m e. _om |-> M ) ` suc n ) e. ( ( m e. _om |-> M ) ` n ) ) )
102	101	ancoms	|- ( ( M e. V /\ n e. _om ) -> ( M e. M -> ( ( m e. _om |-> M ) ` suc n ) e. ( ( m e. _om |-> M ) ` n ) ) )
103	102	impancom	|- ( ( M e. V /\ M e. M ) -> ( n e. _om -> ( ( m e. _om |-> M ) ` suc n ) e. ( ( m e. _om |-> M ) ` n ) ) )
104	103	ralrimiv	|- ( ( M e. V /\ M e. M ) -> A. n e. _om ( ( m e. _om |-> M ) ` suc n ) e. ( ( m e. _om |-> M ) ` n ) )
105	91 94 104	3jca	|- ( ( M e. V /\ M e. M ) -> ( ( m e. _om |-> M ) Fn _om /\ ( ( m e. _om |-> M ) ` (/) ) = M /\ A. n e. _om ( ( m e. _om |-> M ) ` suc n ) e. ( ( m e. _om |-> M ) ` n ) ) )
106		fneq1	|- ( f = ( m e. _om |-> M ) -> ( f Fn _om <-> ( m e. _om |-> M ) Fn _om ) )
107		fveq1	|- ( f = ( m e. _om |-> M ) -> ( f ` (/) ) = ( ( m e. _om |-> M ) ` (/) ) )
108	107	eqeq1d	|- ( f = ( m e. _om |-> M ) -> ( ( f ` (/) ) = M <-> ( ( m e. _om |-> M ) ` (/) ) = M ) )
109		fveq1	|- ( f = ( m e. _om |-> M ) -> ( f ` suc n ) = ( ( m e. _om |-> M ) ` suc n ) )
110		fveq1	|- ( f = ( m e. _om |-> M ) -> ( f ` n ) = ( ( m e. _om |-> M ) ` n ) )
111	109 110	eleq12d	|- ( f = ( m e. _om |-> M ) -> ( ( f ` suc n ) e. ( f ` n ) <-> ( ( m e. _om |-> M ) ` suc n ) e. ( ( m e. _om |-> M ) ` n ) ) )
112	111	ralbidv	|- ( f = ( m e. _om |-> M ) -> ( A. n e. _om ( f ` suc n ) e. ( f ` n ) <-> A. n e. _om ( ( m e. _om |-> M ) ` suc n ) e. ( ( m e. _om |-> M ) ` n ) ) )
113	106 108 112	3anbi123d	|- ( f = ( m e. _om |-> M ) -> ( ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) <-> ( ( m e. _om |-> M ) Fn _om /\ ( ( m e. _om |-> M ) ` (/) ) = M /\ A. n e. _om ( ( m e. _om |-> M ) ` suc n ) e. ( ( m e. _om |-> M ) ` n ) ) ) )
114	105 113	syl5ibrcom	|- ( ( M e. V /\ M e. M ) -> ( f = ( m e. _om |-> M ) -> ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
115	114	eximdv	|- ( ( M e. V /\ M e. M ) -> ( E. f f = ( m e. _om |-> M ) -> E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
116	115	ex	|- ( M e. V -> ( M e. M -> ( E. f f = ( m e. _om |-> M ) -> E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) ) )
117	86 116	mpii	|- ( M e. V -> ( M e. M -> E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
118	82 117	mtod	|- ( M e. V -> -. M e. M )
119		eqeq2	|- ( x = M -> ( ( f ` (/) ) = x <-> ( f ` (/) ) = M ) )
120	119	3anbi2d	|- ( x = M -> ( ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) <-> ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
121	120	exbidv	|- ( x = M -> ( E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) <-> E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
122	121	notbid	|- ( x = M -> ( -. E. f ( f Fn _om /\ ( f ` (/) ) = x /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) <-> -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
123	122 1	elrab2	|- ( M e. M <-> ( M e. V /\ -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
124	118 123	sylnib	|- ( M e. V -> -. ( M e. V /\ -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
125		ianor	|- ( -. ( M e. V /\ -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) <-> ( -. M e. V \/ -. -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
126	124 125	sylib	|- ( M e. V -> ( -. M e. V \/ -. -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) ) )
127	83 84 126	mpjaod	|- ( M e. V -> -. -. E. f ( f Fn _om /\ ( f ` (/) ) = M /\ A. n e. _om ( f ` suc n ) e. ( f ` n ) ) )
128	82 127	pm2.65i	|- -. M e. V
129	128	nelir	|- M e/ V