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 ( 𝑇 , ℝ* , < ) ) |