Metamath Proof Explorer

Theorem rami

Description: The defining property of a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Hypotheses rami.c ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
rami.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
rami.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
rami.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ0 )
rami.x ⊢ ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )
rami.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
rami.l ⊢ ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑆 ) )
rami.g ⊢ ( 𝜑 → 𝐺 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 )
Assertion rami ( 𝜑 → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) )

Proof

Step Hyp Ref Expression
1 rami.c ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
2 rami.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3 rami.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4 rami.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ0 )
5 rami.x ⊢ ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 )
6 rami.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
7 rami.l ⊢ ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑆 ) )
8 rami.g ⊢ ( 𝜑 → 𝐺 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 )
9 cnveq ⊢ ( 𝑓 = 𝐺 → ◡ 𝑓 = ◡ 𝐺 )
10 9 imaeq1d ⊢ ( 𝑓 = 𝐺 → ( ◡ 𝑓 “ { 𝑐 } ) = ( ◡ 𝐺 “ { 𝑐 } ) )
11 10 sseq2d ⊢ ( 𝑓 = 𝐺 → ( ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) )
12 11 anbi2d ⊢ ( 𝑓 = 𝐺 → ( ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) )
13 12 2rexbidv ⊢ ( 𝑓 = 𝐺 → ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) ) )
14 eqid ⊢ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } = { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) }
15 1 14 ramtcl2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ↔ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } ≠ ∅ ) )
16 1 14 ramtcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } ↔ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } ≠ ∅ ) )
17 15 16 bitr4d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹 : 𝑅 ⟶ ℕ0 ) → ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ↔ ( 𝑀 Ramsey 𝐹 ) ∈ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } ) )
18 2 3 4 17 syl3anc ⊢ ( 𝜑 → ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ↔ ( 𝑀 Ramsey 𝐹 ) ∈ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } ) )
19 5 18 mpbid ⊢ ( 𝜑 → ( 𝑀 Ramsey 𝐹 ) ∈ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } )
20 breq1 ⊢ ( 𝑛 = ( 𝑀 Ramsey 𝐹 ) → ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) ↔ ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑠 ) ) )
21 20 imbi1d ⊢ ( 𝑛 = ( 𝑀 Ramsey 𝐹 ) → ( ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ↔ ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ) )
22 21 albidv ⊢ ( 𝑛 = ( 𝑀 Ramsey 𝐹 ) → ( ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ↔ ∀ 𝑠 ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ) )
23 22 elrab ⊢ ( ( 𝑀 Ramsey 𝐹 ) ∈ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } ↔ ( ( 𝑀 Ramsey 𝐹 ) ∈ ℕ0 ∧ ∀ 𝑠 ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ) )
24 23 simprbi ⊢ ( ( 𝑀 Ramsey 𝐹 ) ∈ { 𝑛 ∈ ℕ0 ∣ ∀ 𝑠 ( 𝑛 ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) } → ∀ 𝑠 ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
25 19 24 syl ⊢ ( 𝜑 → ∀ 𝑠 ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
26 fveq2 ⊢ ( 𝑠 = 𝑆 → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 𝑆 ) )
27 26 breq2d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑠 ) ↔ ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑆 ) ) )
28 oveq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 𝐶 𝑀 ) = ( 𝑆 𝐶 𝑀 ) )
29 28 oveq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) = ( 𝑅 ↑m ( 𝑆 𝐶 𝑀 ) ) )
30 pweq ⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
31 30 rexeqdv ⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
32 31 rexbidv ⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
33 29 32 raleqbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑆 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) )
34 27 33 imbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ↔ ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑆 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑆 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ) )
35 34 spcgv ⊢ ( 𝑆 ∈ 𝑊 → ( ∀ 𝑠 ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑠 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑠 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑠 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) → ( ( 𝑀 Ramsey 𝐹 ) ≤ ( ♯ ‘ 𝑆 ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑆 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) ) ) )
36 6 25 7 35 syl3c ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 𝑆 𝐶 𝑀 ) ) ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
37 ovex ⊢ ( 𝑆 𝐶 𝑀 ) ∈ V
38 elmapg ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑆 𝐶 𝑀 ) ∈ V ) → ( 𝐺 ∈ ( 𝑅 ↑m ( 𝑆 𝐶 𝑀 ) ) ↔ 𝐺 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 ) )
39 3 37 38 sylancl ⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑅 ↑m ( 𝑆 𝐶 𝑀 ) ) ↔ 𝐺 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 ) )
40 8 39 mpbird ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑅 ↑m ( 𝑆 𝐶 𝑀 ) ) )
41 13 36 40 rspcdva ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑅 ∃ 𝑥 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝑐 ) ≤ ( ♯ ‘ 𝑥 ) ∧ ( 𝑥 𝐶 𝑀 ) ⊆ ( ◡ 𝐺 “ { 𝑐 } ) ) )