Metamath Proof Explorer

Theorem 0ram

Description: The Ramsey number when M = 0 . (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion 0ram ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ( 0 Ramsey 𝐹 ) = sup ( ran 𝐹 , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2 0nn0 ⊢ 0 ∈ ℕ0
3 2 a1i ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → 0 ∈ ℕ0 )
4 simpl1 ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → 𝑅 ∈ 𝑉 )
5 simpl3 ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → 𝐹 : 𝑅 ⟶ ℕ0 )
6 5 frnd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ran 𝐹 ⊆ ℕ0 )
7 nn0ssz ⊢ ℕ0 ⊆ ℤ
8 6 7 sstrdi ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ran 𝐹 ⊆ ℤ )
9 5 fdmd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → dom 𝐹 = 𝑅 )
10 simpl2 ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → 𝑅 ≠ ∅ )
11 9 10 eqnetrd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → dom 𝐹 ≠ ∅ )
12 dm0rn0 ⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
13 12 necon3bii ⊢ ( dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅ )
14 11 13 sylib ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ran 𝐹 ≠ ∅ )
15 simpr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
16 suprzcl2 ⊢ ( ( ran 𝐹 ⊆ ℤ ∧ ran 𝐹 ≠ ∅ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
17 8 14 15 16 syl3anc ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 )
18 6 17 sseldd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℕ0 )
19 1 hashbc0 ⊢ ( 𝑠 ∈ V → ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) = { ∅ } )
20 19 elv ⊢ ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) = { ∅ }
21 20 feq2i ⊢ ( 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⟶ 𝑅 ↔ 𝑓 : { ∅ } ⟶ 𝑅 )
22 21 biimpi ⊢ ( 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⟶ 𝑅 → 𝑓 : { ∅ } ⟶ 𝑅 )
23 simprr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → 𝑓 : { ∅ } ⟶ 𝑅 )
24 0ex ⊢ ∅ ∈ V
25 24 snid ⊢ ∅ ∈ { ∅ }
26 ffvelrn ⊢ ( ( 𝑓 : { ∅ } ⟶ 𝑅 ∧ ∅ ∈ { ∅ } ) → ( 𝑓 ‘ ∅ ) ∈ 𝑅 )
27 23 25 26 sylancl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( 𝑓 ‘ ∅ ) ∈ 𝑅 )
28 vex ⊢ 𝑠 ∈ V
29 28 pwid ⊢ 𝑠 ∈ 𝒫 𝑠
30 29 a1i ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → 𝑠 ∈ 𝒫 𝑠 )
31 5 adantr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → 𝐹 : 𝑅 ⟶ ℕ0 )
32 31 27 ffvelrnd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ∈ ℕ0 )
33 32 nn0red ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ∈ ℝ )
34 33 rexrd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ∈ ℝ* )
35 18 nn0red ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ )
36 35 rexrd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ* )
37 36 adantr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → sup ( ran 𝐹 , ℝ , < ) ∈ ℝ* )
38 hashxrcl ⊢ ( 𝑠 ∈ V → ( ♯ ‘ 𝑠 ) ∈ ℝ* )
39 28 38 mp1i ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( ♯ ‘ 𝑠 ) ∈ ℝ* )
40 8 adantr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ran 𝐹 ⊆ ℤ )
41 15 adantr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 )
42 31 ffnd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → 𝐹 Fn 𝑅 )
43 fnfvelrn ⊢ ( ( 𝐹 Fn 𝑅 ∧ ( 𝑓 ‘ ∅ ) ∈ 𝑅 ) → ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ∈ ran 𝐹 )
44 42 27 43 syl2anc ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ∈ ran 𝐹 )
45 suprzub ⊢ ( ( ran 𝐹 ⊆ ℤ ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ∧ ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ∈ ran 𝐹 ) → ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ sup ( ran 𝐹 , ℝ , < ) )
46 40 41 44 45 syl3anc ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ sup ( ran 𝐹 , ℝ , < ) )
47 simprl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) )
48 34 37 39 46 47 xrletrd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ ( ♯ ‘ 𝑠 ) )
49 25 a1i ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ∅ ∈ { ∅ } )
50 fvex ⊢ ( 𝑓 ‘ ∅ ) ∈ V
51 50 snid ⊢ ( 𝑓 ‘ ∅ ) ∈ { ( 𝑓 ‘ ∅ ) }
52 51 a1i ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( 𝑓 ‘ ∅ ) ∈ { ( 𝑓 ‘ ∅ ) } )
53 ffn ⊢ ( 𝑓 : { ∅ } ⟶ 𝑅 → 𝑓 Fn { ∅ } )
54 elpreima ⊢ ( 𝑓 Fn { ∅ } → ( ∅ ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) ↔ ( ∅ ∈ { ∅ } ∧ ( 𝑓 ‘ ∅ ) ∈ { ( 𝑓 ‘ ∅ ) } ) ) )
55 23 53 54 3syl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ( ∅ ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) ↔ ( ∅ ∈ { ∅ } ∧ ( 𝑓 ‘ ∅ ) ∈ { ( 𝑓 ‘ ∅ ) } ) ) )
56 49 52 55 mpbir2and ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ∅ ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) )
57 fveq2 ⊢ ( 𝑐 = ( 𝑓 ‘ ∅ ) → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) )
58 57 breq1d ⊢ ( 𝑐 = ( 𝑓 ‘ ∅ ) → ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ↔ ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
59 1 hashbc0 ⊢ ( 𝑧 ∈ V → ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) = { ∅ } )
60 59 elv ⊢ ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) = { ∅ }
61 60 sseq1i ⊢ ( ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ { ∅ } ⊆ ( ◡ 𝑓 “ { 𝑐 } ) )
62 24 snss ⊢ ( ∅ ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ { ∅ } ⊆ ( ◡ 𝑓 “ { 𝑐 } ) )
63 61 62 bitr4i ⊢ ( ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ∅ ∈ ( ◡ 𝑓 “ { 𝑐 } ) )
64 sneq ⊢ ( 𝑐 = ( 𝑓 ‘ ∅ ) → { 𝑐 } = { ( 𝑓 ‘ ∅ ) } )
65 64 imaeq2d ⊢ ( 𝑐 = ( 𝑓 ‘ ∅ ) → ( ◡ 𝑓 “ { 𝑐 } ) = ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) )
66 65 eleq2d ⊢ ( 𝑐 = ( 𝑓 ‘ ∅ ) → ( ∅ ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ∅ ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) ) )
67 63 66 syl5bb ⊢ ( 𝑐 = ( 𝑓 ‘ ∅ ) → ( ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ∅ ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) ) )
68 58 67 anbi12d ⊢ ( 𝑐 = ( 𝑓 ‘ ∅ ) → ( ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ( ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ ( ♯ ‘ 𝑧 ) ∧ ∅ ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) ) ) )
69 fveq2 ⊢ ( 𝑧 = 𝑠 → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ 𝑠 ) )
70 69 breq2d ⊢ ( 𝑧 = 𝑠 → ( ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ ( ♯ ‘ 𝑧 ) ↔ ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ ( ♯ ‘ 𝑠 ) ) )
71 70 anbi1d ⊢ ( 𝑧 = 𝑠 → ( ( ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ ( ♯ ‘ 𝑧 ) ∧ ∅ ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) ) ↔ ( ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ ( ♯ ‘ 𝑠 ) ∧ ∅ ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) ) ) )
72 68 71 rspc2ev ⊢ ( ( ( 𝑓 ‘ ∅ ) ∈ 𝑅 ∧ 𝑠 ∈ 𝒫 𝑠 ∧ ( ( 𝐹 ‘ ( 𝑓 ‘ ∅ ) ) ≤ ( ♯ ‘ 𝑠 ) ∧ ∅ ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ ∅ ) } ) ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
73 27 30 48 56 72 syl112anc ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : { ∅ } ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
74 22 73 sylanr2 ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ≤ ( ♯ ‘ 𝑠 ) ∧ 𝑓 : ( 𝑠 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⟶ 𝑅 ) ) → ∃ 𝑐 ∈ 𝑅 ∃ 𝑧 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
75 1 3 4 5 18 74 ramub ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ( 0 Ramsey 𝐹 ) ≤ sup ( ran 𝐹 , ℝ , < ) )
76 ffn ⊢ ( 𝐹 : 𝑅 ⟶ ℕ0 → 𝐹 Fn 𝑅 )
77 fvelrnb ⊢ ( 𝐹 Fn 𝑅 → ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ 𝑅 ( 𝐹 ‘ 𝑐 ) = sup ( ran 𝐹 , ℝ , < ) ) )
78 5 76 77 3syl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ( sup ( ran 𝐹 , ℝ , < ) ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ 𝑅 ( 𝐹 ‘ 𝑐 ) = sup ( ran 𝐹 , ℝ , < ) ) )
79 17 78 mpbid ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ∃ 𝑐 ∈ 𝑅 ( 𝐹 ‘ 𝑐 ) = sup ( ran 𝐹 , ℝ , < ) )
80 2 a1i ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → 0 ∈ ℕ0 )
81 simpll1 ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → 𝑅 ∈ 𝑉 )
82 simpll3 ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → 𝐹 : 𝑅 ⟶ ℕ0 )
83 nnm1nn0 ⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ℕ → ( ( 𝐹 ‘ 𝑐 ) − 1 ) ∈ ℕ0 )
84 83 ad2antll ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑐 ) − 1 ) ∈ ℕ0 )
85 vex ⊢ 𝑐 ∈ V
86 24 85 f1osn ⊢ { ⟨ ∅ , 𝑐 ⟩ } : { ∅ } –1-1-onto→ { 𝑐 }
87 f1of ⊢ ( { ⟨ ∅ , 𝑐 ⟩ } : { ∅ } –1-1-onto→ { 𝑐 } → { ⟨ ∅ , 𝑐 ⟩ } : { ∅ } ⟶ { 𝑐 } )
88 86 87 ax-mp ⊢ { ⟨ ∅ , 𝑐 ⟩ } : { ∅ } ⟶ { 𝑐 }
89 simprl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → 𝑐 ∈ 𝑅 )
90 89 snssd ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → { 𝑐 } ⊆ 𝑅 )
91 fss ⊢ ( ( { ⟨ ∅ , 𝑐 ⟩ } : { ∅ } ⟶ { 𝑐 } ∧ { 𝑐 } ⊆ 𝑅 ) → { ⟨ ∅ , 𝑐 ⟩ } : { ∅ } ⟶ 𝑅 )
92 88 90 91 sylancr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → { ⟨ ∅ , 𝑐 ⟩ } : { ∅ } ⟶ 𝑅 )
93 ovex ⊢ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ∈ V
94 1 hashbc0 ⊢ ( ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ∈ V → ( ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) = { ∅ } )
95 93 94 ax-mp ⊢ ( ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) = { ∅ }
96 95 feq2i ⊢ ( { ⟨ ∅ , 𝑐 ⟩ } : ( ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⟶ 𝑅 ↔ { ⟨ ∅ , 𝑐 ⟩ } : { ∅ } ⟶ 𝑅 )
97 92 96 sylibr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → { ⟨ ∅ , 𝑐 ⟩ } : ( ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⟶ 𝑅 )
98 60 sseq1i ⊢ ( ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) ↔ { ∅ } ⊆ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) )
99 24 snss ⊢ ( ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) ↔ { ∅ } ⊆ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) )
100 98 99 bitr4i ⊢ ( ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) ↔ ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) )
101 fzfid ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ∈ Fin )
102 simprr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) )
103 ssdomg ⊢ ( ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ∈ Fin → ( 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) → 𝑧 ≼ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) )
104 101 102 103 sylc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → 𝑧 ≼ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) )
105 101 102 ssfid ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → 𝑧 ∈ Fin )
106 hashdom ⊢ ( ( 𝑧 ∈ Fin ∧ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ∈ Fin ) → ( ( ♯ ‘ 𝑧 ) ≤ ( ♯ ‘ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ↔ 𝑧 ≼ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) )
107 105 101 106 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ( ♯ ‘ 𝑧 ) ≤ ( ♯ ‘ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ↔ 𝑧 ≼ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) )
108 104 107 mpbird ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ♯ ‘ 𝑧 ) ≤ ( ♯ ‘ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) )
109 84 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑐 ) − 1 ) ∈ ℕ0 )
110 hashfz1 ⊢ ( ( ( 𝐹 ‘ 𝑐 ) − 1 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) = ( ( 𝐹 ‘ 𝑐 ) − 1 ) )
111 109 110 syl ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ♯ ‘ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) = ( ( 𝐹 ‘ 𝑐 ) − 1 ) )
112 108 111 breqtrd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ♯ ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑐 ) − 1 ) )
113 hashcl ⊢ ( 𝑧 ∈ Fin → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
114 105 113 syl ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
115 5 ffvelrnda ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ 𝑐 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑐 ) ∈ ℕ0 )
116 115 adantrr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℕ0 )
117 116 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℕ0 )
118 nn0ltlem1 ⊢ ( ( ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑧 ) < ( 𝐹 ‘ 𝑐 ) ↔ ( ♯ ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) )
119 114 117 118 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ( ♯ ‘ 𝑧 ) < ( 𝐹 ‘ 𝑐 ) ↔ ( ♯ ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) )
120 112 119 mpbird ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ♯ ‘ 𝑧 ) < ( 𝐹 ‘ 𝑐 ) )
121 24 85 fvsn ⊢ ( { ⟨ ∅ , 𝑐 ⟩ } ‘ ∅ ) = 𝑐
122 f1ofn ⊢ ( { ⟨ ∅ , 𝑐 ⟩ } : { ∅ } –1-1-onto→ { 𝑐 } → { ⟨ ∅ , 𝑐 ⟩ } Fn { ∅ } )
123 elpreima ⊢ ( { ⟨ ∅ , 𝑐 ⟩ } Fn { ∅ } → ( ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) ↔ ( ∅ ∈ { ∅ } ∧ ( { ⟨ ∅ , 𝑐 ⟩ } ‘ ∅ ) ∈ { 𝑑 } ) ) )
124 86 122 123 mp2b ⊢ ( ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) ↔ ( ∅ ∈ { ∅ } ∧ ( { ⟨ ∅ , 𝑐 ⟩ } ‘ ∅ ) ∈ { 𝑑 } ) )
125 124 simprbi ⊢ ( ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) → ( { ⟨ ∅ , 𝑐 ⟩ } ‘ ∅ ) ∈ { 𝑑 } )
126 121 125 eqeltrrid ⊢ ( ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) → 𝑐 ∈ { 𝑑 } )
127 elsni ⊢ ( 𝑐 ∈ { 𝑑 } → 𝑐 = 𝑑 )
128 126 127 syl ⊢ ( ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) → 𝑐 = 𝑑 )
129 128 fveq2d ⊢ ( ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑑 ) )
130 129 breq2d ⊢ ( ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) → ( ( ♯ ‘ 𝑧 ) < ( 𝐹 ‘ 𝑐 ) ↔ ( ♯ ‘ 𝑧 ) < ( 𝐹 ‘ 𝑑 ) ) )
131 120 130 syl5ibcom ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ∅ ∈ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) → ( ♯ ‘ 𝑧 ) < ( 𝐹 ‘ 𝑑 ) ) )
132 100 131 syl5bi ⊢ ( ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) ∧ ( 𝑑 ∈ 𝑅 ∧ 𝑧 ⊆ ( 1 ... ( ( 𝐹 ‘ 𝑐 ) − 1 ) ) ) ) → ( ( 𝑧 ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } ) 0 ) ⊆ ( ◡ { ⟨ ∅ , 𝑐 ⟩ } “ { 𝑑 } ) → ( ♯ ‘ 𝑧 ) < ( 𝐹 ‘ 𝑑 ) ) )
133 1 80 81 82 84 97 132 ramlb ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑐 ) − 1 ) < ( 0 Ramsey 𝐹 ) )
134 ramubcl ⊢ ( ( ( 0 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( sup ( ran 𝐹 , ℝ , < ) ∈ ℕ0 ∧ ( 0 Ramsey 𝐹 ) ≤ sup ( ran 𝐹 , ℝ , < ) ) ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )
135 3 4 5 18 75 134 syl32anc ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )
136 135 adantr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )
137 nn0lem1lt ⊢ ( ( ( 𝐹 ‘ 𝑐 ) ∈ ℕ0 ∧ ( 0 Ramsey 𝐹 ) ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑐 ) ≤ ( 0 Ramsey 𝐹 ) ↔ ( ( 𝐹 ‘ 𝑐 ) − 1 ) < ( 0 Ramsey 𝐹 ) ) )
138 116 136 137 syl2anc ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑐 ) ≤ ( 0 Ramsey 𝐹 ) ↔ ( ( 𝐹 ‘ 𝑐 ) − 1 ) < ( 0 Ramsey 𝐹 ) ) )
139 133 138 mpbird ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ ( 𝑐 ∈ 𝑅 ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℕ ) ) → ( 𝐹 ‘ 𝑐 ) ≤ ( 0 Ramsey 𝐹 ) )
140 139 expr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ 𝑐 ∈ 𝑅 ) → ( ( 𝐹 ‘ 𝑐 ) ∈ ℕ → ( 𝐹 ‘ 𝑐 ) ≤ ( 0 Ramsey 𝐹 ) ) )
141 135 adantr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ 𝑐 ∈ 𝑅 ) → ( 0 Ramsey 𝐹 ) ∈ ℕ0 )
142 141 nn0ge0d ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ 𝑐 ∈ 𝑅 ) → 0 ≤ ( 0 Ramsey 𝐹 ) )
143 breq1 ⊢ ( ( 𝐹 ‘ 𝑐 ) = 0 → ( ( 𝐹 ‘ 𝑐 ) ≤ ( 0 Ramsey 𝐹 ) ↔ 0 ≤ ( 0 Ramsey 𝐹 ) ) )
144 142 143 syl5ibrcom ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ 𝑐 ∈ 𝑅 ) → ( ( 𝐹 ‘ 𝑐 ) = 0 → ( 𝐹 ‘ 𝑐 ) ≤ ( 0 Ramsey 𝐹 ) ) )
145 elnn0 ⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ℕ0 ↔ ( ( 𝐹 ‘ 𝑐 ) ∈ ℕ ∨ ( 𝐹 ‘ 𝑐 ) = 0 ) )
146 115 145 sylib ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ 𝑐 ∈ 𝑅 ) → ( ( 𝐹 ‘ 𝑐 ) ∈ ℕ ∨ ( 𝐹 ‘ 𝑐 ) = 0 ) )
147 140 144 146 mpjaod ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ 𝑐 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑐 ) ≤ ( 0 Ramsey 𝐹 ) )
148 breq1 ⊢ ( ( 𝐹 ‘ 𝑐 ) = sup ( ran 𝐹 , ℝ , < ) → ( ( 𝐹 ‘ 𝑐 ) ≤ ( 0 Ramsey 𝐹 ) ↔ sup ( ran 𝐹 , ℝ , < ) ≤ ( 0 Ramsey 𝐹 ) ) )
149 147 148 syl5ibcom ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) ∧ 𝑐 ∈ 𝑅 ) → ( ( 𝐹 ‘ 𝑐 ) = sup ( ran 𝐹 , ℝ , < ) → sup ( ran 𝐹 , ℝ , < ) ≤ ( 0 Ramsey 𝐹 ) ) )
150 149 rexlimdva ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ( ∃ 𝑐 ∈ 𝑅 ( 𝐹 ‘ 𝑐 ) = sup ( ran 𝐹 , ℝ , < ) → sup ( ran 𝐹 , ℝ , < ) ≤ ( 0 Ramsey 𝐹 ) ) )
151 79 150 mpd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → sup ( ran 𝐹 , ℝ , < ) ≤ ( 0 Ramsey 𝐹 ) )
152 135 nn0red ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ( 0 Ramsey 𝐹 ) ∈ ℝ )
153 152 35 letri3d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ( ( 0 Ramsey 𝐹 ) = sup ( ran 𝐹 , ℝ , < ) ↔ ( ( 0 Ramsey 𝐹 ) ≤ sup ( ran 𝐹 , ℝ , < ) ∧ sup ( ran 𝐹 , ℝ , < ) ≤ ( 0 Ramsey 𝐹 ) ) ) )
154 75 151 153 mpbir2and ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ∃ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥 ) → ( 0 Ramsey 𝐹 ) = sup ( ran 𝐹 , ℝ , < ) )