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 \in V \| \neg \exists f (f Fn ω \land f (\emptyset) = x \land \forall n \in ω f (suc n) \in f (n))\}$
	Assertion	mirimanoffr	$⊢ M \notin V$

Proof

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

Metamath Proof Explorer

Theorem mirimanoffr

Proof