Metamath Proof Explorer

Theorem ramub1lem2

Description: Lemma for ramub1 . (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ramub1.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
ramub1.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
ramub1.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ )
ramub1.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑅 ↦ ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝐹 ‘ 𝑥 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) )
ramub1.1 ⊢ ( 𝜑 → 𝐺 : 𝑅 ⟶ ℕ0 )
ramub1.2 ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 )
ramub1.3 ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
ramub1.4 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
ramub1.5 ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )
ramub1.6 ⊢ ( 𝜑 → 𝐾 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 )
ramub1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
ramub1.h ⊢ 𝐻 = ( 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ↦ ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) )
Assertion ramub1lem2 ( 𝜑 → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) )

Proof

Step Hyp Ref Expression
1 ramub1.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 ramub1.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
3 ramub1.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ )
4 ramub1.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑅 ↦ ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝐹 ‘ 𝑥 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) )
5 ramub1.1 ⊢ ( 𝜑 → 𝐺 : 𝑅 ⟶ ℕ0 )
6 ramub1.2 ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 )
7 ramub1.3 ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
8 ramub1.4 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
9 ramub1.5 ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )
10 ramub1.6 ⊢ ( 𝜑 → 𝐾 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 )
11 ramub1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
12 ramub1.h ⊢ 𝐻 = ( 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ↦ ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) )
13 nnm1nn0 ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ0 )
14 1 13 syl ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℕ0 )
15 diffi ⊢ ( 𝑆 ∈ Fin → ( 𝑆 ∖ { 𝑋 } ) ∈ Fin )
16 8 15 syl ⊢ ( 𝜑 → ( 𝑆 ∖ { 𝑋 } ) ∈ Fin )
17 6 nn0red ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℝ )
18 17 leidd ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ≤ ( ( 𝑀 − 1 ) Ramsey 𝐺 ) )
19 hashcl ⊢ ( ( 𝑆 ∖ { 𝑋 } ) ∈ Fin → ( ♯ ‘ ( 𝑆 ∖ { 𝑋 } ) ) ∈ ℕ0 )
20 16 19 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ∖ { 𝑋 } ) ) ∈ ℕ0 )
21 20 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ∖ { 𝑋 } ) ) ∈ ℂ )
22 6 nn0cnd ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℂ )
23 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
24 undif1 ⊢ ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = ( 𝑆 ∪ { 𝑋 } )
25 11 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑆 )
26 ssequn2 ⊢ ( { 𝑋 } ⊆ 𝑆 ↔ ( 𝑆 ∪ { 𝑋 } ) = 𝑆 )
27 25 26 sylib ⊢ ( 𝜑 → ( 𝑆 ∪ { 𝑋 } ) = 𝑆 )
28 24 27 syl5eq ⊢ ( 𝜑 → ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = 𝑆 )
29 28 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = ( ♯ ‘ 𝑆 ) )
30 neldifsnd ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑆 ∖ { 𝑋 } ) )
31 hashunsng ⊢ ( 𝑋 ∈ 𝑆 → ( ( ( 𝑆 ∖ { 𝑋 } ) ∈ Fin ∧ ¬ 𝑋 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ♯ ‘ ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = ( ( ♯ ‘ ( 𝑆 ∖ { 𝑋 } ) ) + 1 ) ) )
32 11 31 syl ⊢ ( 𝜑 → ( ( ( 𝑆 ∖ { 𝑋 } ) ∈ Fin ∧ ¬ 𝑋 ∈ ( 𝑆 ∖ { 𝑋 } ) ) → ( ♯ ‘ ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = ( ( ♯ ‘ ( 𝑆 ∖ { 𝑋 } ) ) + 1 ) ) )
33 16 30 32 mp2and ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑆 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = ( ( ♯ ‘ ( 𝑆 ∖ { 𝑋 } ) ) + 1 ) )
34 29 33 9 3eqtr3d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑆 ∖ { 𝑋 } ) ) + 1 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )
35 21 22 23 34 addcan2ad ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 ∖ { 𝑋 } ) ) = ( ( 𝑀 − 1 ) Ramsey 𝐺 ) )
36 18 35 breqtrrd ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ≤ ( ♯ ‘ ( 𝑆 ∖ { 𝑋 } ) ) )
37 10 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → 𝐾 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 )
38 fveqeq2 ⊢ ( 𝑥 = ( 𝑢 ∪ { 𝑋 } ) → ( ( ♯ ‘ 𝑥 ) = 𝑀 ↔ ( ♯ ‘ ( 𝑢 ∪ { 𝑋 } ) ) = 𝑀 ) )
39 7 hashbcval ⊢ ( ( ( 𝑆 ∖ { 𝑋 } ) ∈ Fin ∧ ( 𝑀 − 1 ) ∈ ℕ0 ) → ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) = { 𝑥 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ∣ ( ♯ ‘ 𝑥 ) = ( 𝑀 − 1 ) } )
40 16 14 39 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) = { 𝑥 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ∣ ( ♯ ‘ 𝑥 ) = ( 𝑀 − 1 ) } )
41 40 eleq2d ⊢ ( 𝜑 → ( 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ↔ 𝑢 ∈ { 𝑥 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ∣ ( ♯ ‘ 𝑥 ) = ( 𝑀 − 1 ) } ) )
42 fveqeq2 ⊢ ( 𝑥 = 𝑢 → ( ( ♯ ‘ 𝑥 ) = ( 𝑀 − 1 ) ↔ ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) ) )
43 42 elrab ⊢ ( 𝑢 ∈ { 𝑥 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ∣ ( ♯ ‘ 𝑥 ) = ( 𝑀 − 1 ) } ↔ ( 𝑢 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ∧ ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) ) )
44 41 43 bitrdi ⊢ ( 𝜑 → ( 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ↔ ( 𝑢 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ∧ ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) ) ) )
45 44 simprbda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → 𝑢 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) )
46 45 elpwid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → 𝑢 ⊆ ( 𝑆 ∖ { 𝑋 } ) )
47 46 difss2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → 𝑢 ⊆ 𝑆 )
48 25 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → { 𝑋 } ⊆ 𝑆 )
49 47 48 unssd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( 𝑢 ∪ { 𝑋 } ) ⊆ 𝑆 )
50 vex ⊢ 𝑢 ∈ V
51 snex ⊢ { 𝑋 } ∈ V
52 50 51 unex ⊢ ( 𝑢 ∪ { 𝑋 } ) ∈ V
53 52 elpw ⊢ ( ( 𝑢 ∪ { 𝑋 } ) ∈ 𝒫 𝑆 ↔ ( 𝑢 ∪ { 𝑋 } ) ⊆ 𝑆 )
54 49 53 sylibr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( 𝑢 ∪ { 𝑋 } ) ∈ 𝒫 𝑆 )
55 16 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( 𝑆 ∖ { 𝑋 } ) ∈ Fin )
56 55 46 ssfid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → 𝑢 ∈ Fin )
57 neldifsnd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ¬ 𝑋 ∈ ( 𝑆 ∖ { 𝑋 } ) )
58 46 57 ssneldd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ¬ 𝑋 ∈ 𝑢 )
59 11 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → 𝑋 ∈ 𝑆 )
60 hashunsng ⊢ ( 𝑋 ∈ 𝑆 → ( ( 𝑢 ∈ Fin ∧ ¬ 𝑋 ∈ 𝑢 ) → ( ♯ ‘ ( 𝑢 ∪ { 𝑋 } ) ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) )
61 59 60 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( ( 𝑢 ∈ Fin ∧ ¬ 𝑋 ∈ 𝑢 ) → ( ♯ ‘ ( 𝑢 ∪ { 𝑋 } ) ) = ( ( ♯ ‘ 𝑢 ) + 1 ) ) )
62 56 58 61 mp2and ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( ♯ ‘ ( 𝑢 ∪ { 𝑋 } ) ) = ( ( ♯ ‘ 𝑢 ) + 1 ) )
63 44 simplbda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) )
64 63 oveq1d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( ( ♯ ‘ 𝑢 ) + 1 ) = ( ( 𝑀 − 1 ) + 1 ) )
65 1 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
66 ax-1cn ⊢ 1 ∈ ℂ
67 npcan ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
68 65 66 67 sylancl ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
70 62 64 69 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( ♯ ‘ ( 𝑢 ∪ { 𝑋 } ) ) = 𝑀 )
71 38 54 70 elrabd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( 𝑢 ∪ { 𝑋 } ) ∈ { 𝑥 ∈ 𝒫 𝑆 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
72 1 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
73 7 hashbcval ⊢ ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ ℕ0 ) → ( 𝑆 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 𝑆 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
74 8 72 73 syl2anc ⊢ ( 𝜑 → ( 𝑆 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 𝑆 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( 𝑆 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 𝑆 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
76 71 75 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( 𝑢 ∪ { 𝑋 } ) ∈ ( 𝑆 𝐶 𝑀 ) )
77 37 76 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ) → ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) ∈ 𝑅 )
78 77 12 fmptd ⊢ ( 𝜑 → 𝐻 : ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ⟶ 𝑅 )
79 7 14 2 5 6 16 36 78 rami ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑅 ∃ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) )
80 72 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝑀 ∈ ℕ0 )
81 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝑅 ∈ Fin )
82 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝐹 : 𝑅 ⟶ ℕ )
83 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝑑 ∈ 𝑅 )
84 82 83 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝐹 ‘ 𝑑 ) ∈ ℕ )
85 nnm1nn0 ⊢ ( ( 𝐹 ‘ 𝑑 ) ∈ ℕ → ( ( 𝐹 ‘ 𝑑 ) − 1 ) ∈ ℕ0 )
86 84 85 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( ( 𝐹 ‘ 𝑑 ) − 1 ) ∈ ℕ0 )
87 86 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ 𝑦 ∈ 𝑅 ) → ( ( 𝐹 ‘ 𝑑 ) − 1 ) ∈ ℕ0 )
88 82 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ 𝑦 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ )
89 88 nnnn0d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ 𝑦 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
90 87 89 ifcld ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ 𝑦 ∈ 𝑅 ) → if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ∈ ℕ0 )
91 eqid ⊢ ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) )
92 90 91 fmptd ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) : 𝑅 ⟶ ℕ0 )
93 equequ2 ⊢ ( 𝑥 = 𝑑 → ( 𝑦 = 𝑥 ↔ 𝑦 = 𝑑 ) )
94 fveq2 ⊢ ( 𝑥 = 𝑑 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑑 ) )
95 94 oveq1d ⊢ ( 𝑥 = 𝑑 → ( ( 𝐹 ‘ 𝑥 ) − 1 ) = ( ( 𝐹 ‘ 𝑑 ) − 1 ) )
96 93 95 ifbieq1d ⊢ ( 𝑥 = 𝑑 → if ( 𝑦 = 𝑥 , ( ( 𝐹 ‘ 𝑥 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) = if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) )
97 96 mpteq2dv ⊢ ( 𝑥 = 𝑑 → ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝐹 ‘ 𝑥 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) )
98 97 oveq2d ⊢ ( 𝑥 = 𝑑 → ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝐹 ‘ 𝑥 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) = ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) )
99 ovex ⊢ ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) ∈ V
100 98 4 99 fvmpt ⊢ ( 𝑑 ∈ 𝑅 → ( 𝐺 ‘ 𝑑 ) = ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) )
101 83 100 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝐺 ‘ 𝑑 ) = ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) )
102 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝐺 : 𝑅 ⟶ ℕ0 )
103 102 83 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝐺 ‘ 𝑑 ) ∈ ℕ0 )
104 101 103 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) ∈ ℕ0 )
105 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) )
106 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) )
107 101 106 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) ≤ ( ♯ ‘ 𝑤 ) )
108 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝐾 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 )
109 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝑆 ∈ Fin )
110 105 elpwid ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝑤 ⊆ ( 𝑆 ∖ { 𝑋 } ) )
111 110 difss2d ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → 𝑤 ⊆ 𝑆 )
112 7 hashbcss ⊢ ( ( 𝑆 ∈ Fin ∧ 𝑤 ⊆ 𝑆 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑤 𝐶 𝑀 ) ⊆ ( 𝑆 𝐶 𝑀 ) )
113 109 111 80 112 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝑤 𝐶 𝑀 ) ⊆ ( 𝑆 𝐶 𝑀 ) )
114 108 113 fssresd ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) : ( 𝑤 𝐶 𝑀 ) ⟶ 𝑅 )
115 7 80 81 92 104 105 107 114 rami ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑣 ∈ 𝒫 𝑤 ( ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) )
116 equequ1 ⊢ ( 𝑦 = 𝑐 → ( 𝑦 = 𝑑 ↔ 𝑐 = 𝑑 ) )
117 fveq2 ⊢ ( 𝑦 = 𝑐 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑐 ) )
118 116 117 ifbieq2d ⊢ ( 𝑦 = 𝑐 → if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) = if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) )
119 ovex ⊢ ( ( 𝐹 ‘ 𝑑 ) − 1 ) ∈ V
120 fvex ⊢ ( 𝐹 ‘ 𝑐 ) ∈ V
121 119 120 ifex ⊢ if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ∈ V
122 118 91 121 fvmpt ⊢ ( 𝑐 ∈ 𝑅 → ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑐 ) = if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) )
123 122 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ) → ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑐 ) = if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) )
124 123 breq1d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ) → ( ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑣 ) ↔ if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ) )
125 124 anbi1d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ) → ( ( ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ↔ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) )
126 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝑀 ∈ ℕ )
127 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝑅 ∈ Fin )
128 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝐹 : 𝑅 ⟶ ℕ )
129 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝐺 : 𝑅 ⟶ ℕ0 )
130 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 )
131 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝑆 ∈ Fin )
132 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → ( ♯ ‘ 𝑆 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )
133 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝐾 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 )
134 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝑋 ∈ 𝑆 )
135 83 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝑑 ∈ 𝑅 )
136 110 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝑤 ⊆ ( 𝑆 ∖ { 𝑋 } ) )
137 106 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) )
138 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) )
139 138 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) )
140 simprll ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝑐 ∈ 𝑅 )
141 simprlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝑣 ∈ 𝒫 𝑤 )
142 141 elpwid ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → 𝑣 ⊆ 𝑤 )
143 simprrl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) )
144 simprrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) )
145 cnvresima ⊢ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) = ( ( ◡ 𝐾 “ { 𝑐 } ) ∩ ( 𝑤 𝐶 𝑀 ) )
146 inss1 ⊢ ( ( ◡ 𝐾 “ { 𝑐 } ) ∩ ( 𝑤 𝐶 𝑀 ) ) ⊆ ( ◡ 𝐾 “ { 𝑐 } )
147 145 146 eqsstri ⊢ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ⊆ ( ◡ 𝐾 “ { 𝑐 } )
148 144 147 sstrdi ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) )
149 126 127 128 4 129 130 7 131 132 133 134 12 135 136 137 139 140 142 143 148 ramub1lem1 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ∧ ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) ) ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) )
150 149 expr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ) → ( ( if ( 𝑐 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑐 ) ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) ) )
151 125 150 sylbid ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ ( 𝑐 ∈ 𝑅 ∧ 𝑣 ∈ 𝒫 𝑤 ) ) → ( ( ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) ) )
152 151 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ 𝑐 ∈ 𝑅 ) ∧ 𝑣 ∈ 𝒫 𝑤 ) → ( ( ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) ) )
153 152 rexlimdva ⊢ ( ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) ∧ 𝑐 ∈ 𝑅 ) → ( ∃ 𝑣 ∈ 𝒫 𝑤 ( ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) ) )
154 153 reximdva ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑣 ∈ 𝒫 𝑤 ( ( ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑑 , ( ( 𝐹 ‘ 𝑑 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑣 ) ∧ ( 𝑣 𝐶 𝑀 ) ⊆ ( ◡ ( 𝐾 ↾ ( 𝑤 𝐶 𝑀 ) ) “ { 𝑐 } ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) ) )
155 115 154 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ∧ ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) )
156 155 expr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ) ) → ( ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) ) )
157 156 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑑 ∈ 𝑅 ∃ 𝑤 ∈ 𝒫 ( 𝑆 ∖ { 𝑋 } ) ( ( 𝐺 ‘ 𝑑 ) ≤ ( ♯ ‘ 𝑤 ) ∧ ( 𝑤 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝑑 } ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) ) )
158 79 157 mpd ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝑐 } ) ) )