Metamath Proof Explorer

Theorem ramval

Description: The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses ramval.c ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
ramval.t ⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) }
Assertion ramval ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 ramval.c ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2 ramval.t ⊢ 𝑇 = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) }
3 df-ram ⊢ Ramsey = ( 𝑚 ∈ ℕ0 , 𝑟 ∈ V ↦ inf ( { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ) } , ℝ* , < ) )
4 3 a1i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → Ramsey = ( 𝑚 ∈ ℕ0 , 𝑟 ∈ V ↦ inf ( { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ) } , ℝ* , < ) ) )
5 simplrr ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑟 = 𝐹 )
6 5 dmeqd ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → dom 𝑟 = dom 𝐹 )
7 simpll3 ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝐹 : 𝑅 ⟶ ℕ0 )
8 7 fdmd ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → dom 𝐹 = 𝑅 )
9 6 8 eqtrd ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → dom 𝑟 = 𝑅 )
10 simplrl ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑚 = 𝑀 )
11 10 eqeq2d ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑦 ) = 𝑚 ↔ ( ♯ ‘ 𝑦 ) = 𝑀 ) )
12 11 rabbidv ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } = { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑀 } )
13 vex ⊢ 𝑠 ∈ V
14 simpll1 ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
15 1 hashbcval ⊢ ( ( 𝑠 ∈ V ∧ 𝑀 ∈ ℕ0 ) → ( 𝑠 𝐶 𝑀 ) = { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑀 } )
16 13 14 15 sylancr ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑠 𝐶 𝑀 ) = { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑀 } )
17 12 16 eqtr4d ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } = ( 𝑠 𝐶 𝑀 ) )
18 9 17 oveq12d ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) = ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) )
19 18 raleqdv ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ) )
20 simpr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) → 𝑟 = 𝐹 )
21 20 dmeqd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) → dom 𝑟 = dom 𝐹 )
22 fdm ⊢ ( 𝐹 : 𝑅 ⟶ ℕ0 → dom 𝐹 = 𝑅 )
23 22 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → dom 𝐹 = 𝑅 )
24 21 23 sylan9eqr ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) → dom 𝑟 = 𝑅 )
25 24 ad2antrr ⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) → dom 𝑟 = 𝑅 )
26 5 ad2antrr ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → 𝑟 = 𝐹 )
27 26 fveq1d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( 𝑟 ‘ 𝑐 ) = ( 𝐹 ‘ 𝑐 ) )
28 27 breq1d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ) )
29 10 ad2antrr ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → 𝑚 = 𝑀 )
30 29 oveq2d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( 𝑥 𝐶 𝑚 ) = ( 𝑥 𝐶 𝑀 ) )
31 vex ⊢ 𝑥 ∈ V
32 14 ad2antrr ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → 𝑀 ∈ ℕ0 )
33 29 32 eqeltrd ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → 𝑚 ∈ ℕ0 )
34 1 hashbcval ⊢ ( ( 𝑥 ∈ V ∧ 𝑚 ∈ ℕ0 ) → ( 𝑥 𝐶 𝑚 ) = { 𝑦 ∈ 𝒫 𝑥 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } )
35 31 33 34 sylancr ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( 𝑥 𝐶 𝑚 ) = { 𝑦 ∈ 𝒫 𝑥 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } )
36 30 35 eqtr3d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( 𝑥 𝐶 𝑀 ) = { 𝑦 ∈ 𝒫 𝑥 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } )
37 36 sseq1d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ { 𝑦 ∈ 𝒫 𝑥 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
38 rabss ⊢ ( { 𝑦 ∈ 𝒫 𝑥 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝑦 ∈ ( ◡ 𝑓 “ { 𝑐 } ) ) )
39 36 eleq2d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( 𝑦 ∈ ( 𝑥 𝐶 𝑀 ) ↔ 𝑦 ∈ { 𝑦 ∈ 𝒫 𝑥 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) )
40 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝒫 𝑥 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ↔ ( 𝑦 ∈ 𝒫 𝑥 ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) )
41 39 40 bitrdi ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( 𝑦 ∈ ( 𝑥 𝐶 𝑀 ) ↔ ( 𝑦 ∈ 𝒫 𝑥 ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) )
42 41 biimpar ⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) ∧ ( 𝑦 ∈ 𝒫 𝑥 ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) → 𝑦 ∈ ( 𝑥 𝐶 𝑀 ) )
43 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑠 → 𝑥 ⊆ 𝑠 )
44 43 adantl ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → 𝑥 ⊆ 𝑠 )
45 1 hashbcss ⊢ ( ( 𝑠 ∈ V ∧ 𝑥 ⊆ 𝑠 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑥 𝐶 𝑀 ) ⊆ ( 𝑠 𝐶 𝑀 ) )
46 13 44 32 45 mp3an2i ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( 𝑥 𝐶 𝑀 ) ⊆ ( 𝑠 𝐶 𝑀 ) )
47 46 sselda ⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) ∧ 𝑦 ∈ ( 𝑥 𝐶 𝑀 ) ) → 𝑦 ∈ ( 𝑠 𝐶 𝑀 ) )
48 42 47 syldan ⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) ∧ ( 𝑦 ∈ 𝒫 𝑥 ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) → 𝑦 ∈ ( 𝑠 𝐶 𝑀 ) )
49 elmapi ⊢ ( 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) → 𝑓 : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 )
50 49 ad3antlr ⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) ∧ ( 𝑦 ∈ 𝒫 𝑥 ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) → 𝑓 : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 )
51 ffn ⊢ ( 𝑓 : ( 𝑠 𝐶 𝑀 ) ⟶ 𝑅 → 𝑓 Fn ( 𝑠 𝐶 𝑀 ) )
52 fniniseg ⊢ ( 𝑓 Fn ( 𝑠 𝐶 𝑀 ) → ( 𝑦 ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ( 𝑦 ∈ ( 𝑠 𝐶 𝑀 ) ∧ ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) )
53 50 51 52 3syl ⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) ∧ ( 𝑦 ∈ 𝒫 𝑥 ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) → ( 𝑦 ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ( 𝑦 ∈ ( 𝑠 𝐶 𝑀 ) ∧ ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) )
54 48 53 mpbirand ⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) ∧ ( 𝑦 ∈ 𝒫 𝑥 ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) ) → ( 𝑦 ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ( 𝑓 ‘ 𝑦 ) = 𝑐 ) )
55 54 anassrs ⊢ ( ( ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) ∧ 𝑦 ∈ 𝒫 𝑥 ) ∧ ( ♯ ‘ 𝑦 ) = 𝑚 ) → ( 𝑦 ∈ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ( 𝑓 ‘ 𝑦 ) = 𝑐 ) )
56 55 pm5.74da ⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) ∧ 𝑦 ∈ 𝒫 𝑥 ) → ( ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝑦 ∈ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) )
57 56 ralbidva ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → 𝑦 ∈ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) )
58 38 57 syl5bb ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( { 𝑦 ∈ 𝒫 𝑥 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) )
59 37 58 bitr2d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ↔ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
60 28 59 anbi12d ⊢ ( ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
61 60 rexbidva ⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) → ( ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ↔ ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
62 25 61 rexeqbidv ⊢ ( ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ) → ( ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
63 62 ralbidva ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
64 19 63 bitrd ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑓 ∈ ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
65 64 imbi2d ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ) ↔ ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ) )
66 65 albidv ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ) ↔ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ) )
67 66 rabbidva ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) → { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ) } = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } )
68 67 2 eqtr4di ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) → { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ) } = 𝑇 )
69 68 infeq1d ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) ∧ ( 𝑚 = 𝑀 ∧ 𝑟 = 𝐹 ) ) → inf ( { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( dom 𝑟 ↑m { 𝑦 ∈ 𝒫 𝑠 ∣ ( ♯ ‘ 𝑦 ) = 𝑚 } ) ∃ 𝑐 ∈ dom 𝑟 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑟 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝒫 𝑥 ( ( ♯ ‘ 𝑦 ) = 𝑚 → ( 𝑓 ‘ 𝑦 ) = 𝑐 ) ) ) } , ℝ* , < ) = inf ( 𝑇 , ℝ* , < ) )
70 simp1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝑀 ∈ ℕ0 )
71 simp3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝐹 : 𝑅 ⟶ ℕ0 )
72 simp2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝑅 ∈ 𝑉 )
73 fex ⊢ ( ( 𝐹 : 𝑅 ⟶ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → 𝐹 ∈ V )
74 71 72 73 syl2anc ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → 𝐹 ∈ V )
75 xrltso ⊢ < Or ℝ*
76 75 infex ⊢ inf ( 𝑇 , ℝ* , < ) ∈ V
77 76 a1i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → inf ( 𝑇 , ℝ* , < ) ∈ V )
78 4 69 70 74 77 ovmpod ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( 𝑀 Ramsey 𝐹 ) = inf ( 𝑇 , ℝ* , < ) )