Metamath Proof Explorer

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 ⊢ 𝑀 = { 𝑥 ∈ 𝑉 ∣ ¬ ∃ 𝑓 ( 𝑓 Fn ω ∧ ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ∀ 𝑛 ∈ ω ( 𝑓 ‘ suc 𝑛 ) ∈ ( 𝑓 ‘ 𝑛 ) ) }
Assertion mirimanoffr 𝑀 ∉ 𝑉

Proof

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