MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ramval Structured version   Visualization version   GIF version

Theorem ramval 16948
Description: The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by AV, 14-Sep-2020.)
Hypotheses
Ref Expression
ramval.c 𝐢 = (π‘Ž ∈ V, 𝑖 ∈ β„•0 ↦ {𝑏 ∈ 𝒫 π‘Ž ∣ (β™―β€˜π‘) = 𝑖})
ramval.t 𝑇 = {𝑛 ∈ β„•0 ∣ βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (𝑅 ↑m (𝑠𝐢𝑀))βˆƒπ‘ ∈ 𝑅 βˆƒπ‘₯ ∈ 𝒫 𝑠((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐})))}
Assertion
Ref Expression
ramval ((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) β†’ (𝑀 Ramsey 𝐹) = inf(𝑇, ℝ*, < ))
Distinct variable groups:   𝑓,𝑐,π‘₯,𝐢   𝑛,𝑐,𝑠,𝐹,𝑓,π‘₯   π‘Ž,𝑏,𝑐,𝑓,𝑖,𝑛,𝑠,π‘₯,𝑀   𝑅,𝑐,𝑓,𝑛,𝑠,π‘₯   𝑉,𝑐,𝑓,𝑛,𝑠,π‘₯
Allowed substitution hints:   𝐢(𝑖,𝑛,𝑠,π‘Ž,𝑏)   𝑅(𝑖,π‘Ž,𝑏)   𝑇(π‘₯,𝑓,𝑖,𝑛,𝑠,π‘Ž,𝑏,𝑐)   𝐹(𝑖,π‘Ž,𝑏)   𝑉(𝑖,π‘Ž,𝑏)

Proof of Theorem ramval
Dummy variables 𝑦 π‘š π‘Ÿ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ram 16941 . . 3 Ramsey = (π‘š ∈ β„•0, π‘Ÿ ∈ V ↦ inf({𝑛 ∈ β„•0 ∣ βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š})βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)))}, ℝ*, < ))
21a1i 11 . 2 ((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) β†’ Ramsey = (π‘š ∈ β„•0, π‘Ÿ ∈ V ↦ inf({𝑛 ∈ β„•0 ∣ βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š})βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)))}, ℝ*, < )))
3 simplrr 775 . . . . . . . . . . . 12 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ π‘Ÿ = 𝐹)
43dmeqd 5898 . . . . . . . . . . 11 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ dom π‘Ÿ = dom 𝐹)
5 simpll3 1211 . . . . . . . . . . . 12 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ 𝐹:π‘…βŸΆβ„•0)
65fdmd 6721 . . . . . . . . . . 11 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ dom 𝐹 = 𝑅)
74, 6eqtrd 2766 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ dom π‘Ÿ = 𝑅)
8 simplrl 774 . . . . . . . . . . . . 13 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ π‘š = 𝑀)
98eqeq2d 2737 . . . . . . . . . . . 12 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ ((β™―β€˜π‘¦) = π‘š ↔ (β™―β€˜π‘¦) = 𝑀))
109rabbidv 3434 . . . . . . . . . . 11 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š} = {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = 𝑀})
11 vex 3472 . . . . . . . . . . . 12 𝑠 ∈ V
12 simpll1 1209 . . . . . . . . . . . 12 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ 𝑀 ∈ β„•0)
13 ramval.c . . . . . . . . . . . . 13 𝐢 = (π‘Ž ∈ V, 𝑖 ∈ β„•0 ↦ {𝑏 ∈ 𝒫 π‘Ž ∣ (β™―β€˜π‘) = 𝑖})
1413hashbcval 16942 . . . . . . . . . . . 12 ((𝑠 ∈ V ∧ 𝑀 ∈ β„•0) β†’ (𝑠𝐢𝑀) = {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = 𝑀})
1511, 12, 14sylancr 586 . . . . . . . . . . 11 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ (𝑠𝐢𝑀) = {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = 𝑀})
1610, 15eqtr4d 2769 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š} = (𝑠𝐢𝑀))
177, 16oveq12d 7422 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š}) = (𝑅 ↑m (𝑠𝐢𝑀)))
1817raleqdv 3319 . . . . . . . 8 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ (βˆ€π‘“ ∈ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š})βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)) ↔ βˆ€π‘“ ∈ (𝑅 ↑m (𝑠𝐢𝑀))βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐))))
19 simpr 484 . . . . . . . . . . . . 13 ((π‘š = 𝑀 ∧ π‘Ÿ = 𝐹) β†’ π‘Ÿ = 𝐹)
2019dmeqd 5898 . . . . . . . . . . . 12 ((π‘š = 𝑀 ∧ π‘Ÿ = 𝐹) β†’ dom π‘Ÿ = dom 𝐹)
21 fdm 6719 . . . . . . . . . . . . 13 (𝐹:π‘…βŸΆβ„•0 β†’ dom 𝐹 = 𝑅)
22213ad2ant3 1132 . . . . . . . . . . . 12 ((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) β†’ dom 𝐹 = 𝑅)
2320, 22sylan9eqr 2788 . . . . . . . . . . 11 (((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) β†’ dom π‘Ÿ = 𝑅)
2423ad2antrr 723 . . . . . . . . . 10 (((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) β†’ dom π‘Ÿ = 𝑅)
253ad2antrr 723 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ π‘Ÿ = 𝐹)
2625fveq1d 6886 . . . . . . . . . . . . 13 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (π‘Ÿβ€˜π‘) = (πΉβ€˜π‘))
2726breq1d 5151 . . . . . . . . . . . 12 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ ((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ↔ (πΉβ€˜π‘) ≀ (β™―β€˜π‘₯)))
288ad2antrr 723 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ π‘š = 𝑀)
2928oveq2d 7420 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (π‘₯πΆπ‘š) = (π‘₯𝐢𝑀))
30 vex 3472 . . . . . . . . . . . . . . . 16 π‘₯ ∈ V
3112ad2antrr 723 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ 𝑀 ∈ β„•0)
3228, 31eqeltrd 2827 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ π‘š ∈ β„•0)
3313hashbcval 16942 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ V ∧ π‘š ∈ β„•0) β†’ (π‘₯πΆπ‘š) = {𝑦 ∈ 𝒫 π‘₯ ∣ (β™―β€˜π‘¦) = π‘š})
3430, 32, 33sylancr 586 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (π‘₯πΆπ‘š) = {𝑦 ∈ 𝒫 π‘₯ ∣ (β™―β€˜π‘¦) = π‘š})
3529, 34eqtr3d 2768 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (π‘₯𝐢𝑀) = {𝑦 ∈ 𝒫 π‘₯ ∣ (β™―β€˜π‘¦) = π‘š})
3635sseq1d 4008 . . . . . . . . . . . . 13 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ ((π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐}) ↔ {𝑦 ∈ 𝒫 π‘₯ ∣ (β™―β€˜π‘¦) = π‘š} βŠ† (◑𝑓 β€œ {𝑐})))
37 rabss 4064 . . . . . . . . . . . . . 14 ({𝑦 ∈ 𝒫 π‘₯ ∣ (β™―β€˜π‘¦) = π‘š} βŠ† (◑𝑓 β€œ {𝑐}) ↔ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ 𝑦 ∈ (◑𝑓 β€œ {𝑐})))
3835eleq2d 2813 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (𝑦 ∈ (π‘₯𝐢𝑀) ↔ 𝑦 ∈ {𝑦 ∈ 𝒫 π‘₯ ∣ (β™―β€˜π‘¦) = π‘š}))
39 rabid 3446 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ {𝑦 ∈ 𝒫 π‘₯ ∣ (β™―β€˜π‘¦) = π‘š} ↔ (𝑦 ∈ 𝒫 π‘₯ ∧ (β™―β€˜π‘¦) = π‘š))
4038, 39bitrdi 287 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (𝑦 ∈ (π‘₯𝐢𝑀) ↔ (𝑦 ∈ 𝒫 π‘₯ ∧ (β™―β€˜π‘¦) = π‘š)))
4140biimpar 477 . . . . . . . . . . . . . . . . . . 19 (((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 π‘₯ ∧ (β™―β€˜π‘¦) = π‘š)) β†’ 𝑦 ∈ (π‘₯𝐢𝑀))
42 elpwi 4604 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ 𝒫 𝑠 β†’ π‘₯ βŠ† 𝑠)
4342adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ π‘₯ βŠ† 𝑠)
4413hashbcss 16944 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ V ∧ π‘₯ βŠ† 𝑠 ∧ 𝑀 ∈ β„•0) β†’ (π‘₯𝐢𝑀) βŠ† (𝑠𝐢𝑀))
4511, 43, 31, 44mp3an2i 1462 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (π‘₯𝐢𝑀) βŠ† (𝑠𝐢𝑀))
4645sselda 3977 . . . . . . . . . . . . . . . . . . 19 (((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) ∧ 𝑦 ∈ (π‘₯𝐢𝑀)) β†’ 𝑦 ∈ (𝑠𝐢𝑀))
4741, 46syldan 590 . . . . . . . . . . . . . . . . . 18 (((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 π‘₯ ∧ (β™―β€˜π‘¦) = π‘š)) β†’ 𝑦 ∈ (𝑠𝐢𝑀))
48 elmapi 8842 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀)) β†’ 𝑓:(𝑠𝐢𝑀)βŸΆπ‘…)
4948ad3antlr 728 . . . . . . . . . . . . . . . . . . 19 (((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 π‘₯ ∧ (β™―β€˜π‘¦) = π‘š)) β†’ 𝑓:(𝑠𝐢𝑀)βŸΆπ‘…)
50 ffn 6710 . . . . . . . . . . . . . . . . . . 19 (𝑓:(𝑠𝐢𝑀)βŸΆπ‘… β†’ 𝑓 Fn (𝑠𝐢𝑀))
51 fniniseg 7054 . . . . . . . . . . . . . . . . . . 19 (𝑓 Fn (𝑠𝐢𝑀) β†’ (𝑦 ∈ (◑𝑓 β€œ {𝑐}) ↔ (𝑦 ∈ (𝑠𝐢𝑀) ∧ (π‘“β€˜π‘¦) = 𝑐)))
5249, 50, 513syl 18 . . . . . . . . . . . . . . . . . 18 (((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 π‘₯ ∧ (β™―β€˜π‘¦) = π‘š)) β†’ (𝑦 ∈ (◑𝑓 β€œ {𝑐}) ↔ (𝑦 ∈ (𝑠𝐢𝑀) ∧ (π‘“β€˜π‘¦) = 𝑐)))
5347, 52mpbirand 704 . . . . . . . . . . . . . . . . 17 (((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) ∧ (𝑦 ∈ 𝒫 π‘₯ ∧ (β™―β€˜π‘¦) = π‘š)) β†’ (𝑦 ∈ (◑𝑓 β€œ {𝑐}) ↔ (π‘“β€˜π‘¦) = 𝑐))
5453anassrs 467 . . . . . . . . . . . . . . . 16 ((((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) ∧ 𝑦 ∈ 𝒫 π‘₯) ∧ (β™―β€˜π‘¦) = π‘š) β†’ (𝑦 ∈ (◑𝑓 β€œ {𝑐}) ↔ (π‘“β€˜π‘¦) = 𝑐))
5554pm5.74da 801 . . . . . . . . . . . . . . 15 (((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) ∧ 𝑦 ∈ 𝒫 π‘₯) β†’ (((β™―β€˜π‘¦) = π‘š β†’ 𝑦 ∈ (◑𝑓 β€œ {𝑐})) ↔ ((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)))
5655ralbidva 3169 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ 𝑦 ∈ (◑𝑓 β€œ {𝑐})) ↔ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)))
5737, 56bitrid 283 . . . . . . . . . . . . 13 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ ({𝑦 ∈ 𝒫 π‘₯ ∣ (β™―β€˜π‘¦) = π‘š} βŠ† (◑𝑓 β€œ {𝑐}) ↔ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)))
5836, 57bitr2d 280 . . . . . . . . . . . 12 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐) ↔ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐})))
5927, 58anbi12d 630 . . . . . . . . . . 11 ((((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)) ↔ ((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐}))))
6059rexbidva 3170 . . . . . . . . . 10 (((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) β†’ (βˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)) ↔ βˆƒπ‘₯ ∈ 𝒫 𝑠((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐}))))
6124, 60rexeqbidv 3337 . . . . . . . . 9 (((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) ∧ 𝑓 ∈ (𝑅 ↑m (𝑠𝐢𝑀))) β†’ (βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)) ↔ βˆƒπ‘ ∈ 𝑅 βˆƒπ‘₯ ∈ 𝒫 𝑠((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐}))))
6261ralbidva 3169 . . . . . . . 8 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ (βˆ€π‘“ ∈ (𝑅 ↑m (𝑠𝐢𝑀))βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)) ↔ βˆ€π‘“ ∈ (𝑅 ↑m (𝑠𝐢𝑀))βˆƒπ‘ ∈ 𝑅 βˆƒπ‘₯ ∈ 𝒫 𝑠((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐}))))
6318, 62bitrd 279 . . . . . . 7 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ (βˆ€π‘“ ∈ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š})βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)) ↔ βˆ€π‘“ ∈ (𝑅 ↑m (𝑠𝐢𝑀))βˆƒπ‘ ∈ 𝑅 βˆƒπ‘₯ ∈ 𝒫 𝑠((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐}))))
6463imbi2d 340 . . . . . 6 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ ((𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š})βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐))) ↔ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (𝑅 ↑m (𝑠𝐢𝑀))βˆƒπ‘ ∈ 𝑅 βˆƒπ‘₯ ∈ 𝒫 𝑠((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐})))))
6564albidv 1915 . . . . 5 ((((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) ∧ 𝑛 ∈ β„•0) β†’ (βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š})βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐))) ↔ βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (𝑅 ↑m (𝑠𝐢𝑀))βˆƒπ‘ ∈ 𝑅 βˆƒπ‘₯ ∈ 𝒫 𝑠((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐})))))
6665rabbidva 3433 . . . 4 (((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) β†’ {𝑛 ∈ β„•0 ∣ βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š})βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)))} = {𝑛 ∈ β„•0 ∣ βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (𝑅 ↑m (𝑠𝐢𝑀))βˆƒπ‘ ∈ 𝑅 βˆƒπ‘₯ ∈ 𝒫 𝑠((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐})))})
67 ramval.t . . . 4 𝑇 = {𝑛 ∈ β„•0 ∣ βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (𝑅 ↑m (𝑠𝐢𝑀))βˆƒπ‘ ∈ 𝑅 βˆƒπ‘₯ ∈ 𝒫 𝑠((πΉβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ (π‘₯𝐢𝑀) βŠ† (◑𝑓 β€œ {𝑐})))}
6866, 67eqtr4di 2784 . . 3 (((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) β†’ {𝑛 ∈ β„•0 ∣ βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š})βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)))} = 𝑇)
6968infeq1d 9471 . 2 (((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) ∧ (π‘š = 𝑀 ∧ π‘Ÿ = 𝐹)) β†’ inf({𝑛 ∈ β„•0 ∣ βˆ€π‘ (𝑛 ≀ (β™―β€˜π‘ ) β†’ βˆ€π‘“ ∈ (dom π‘Ÿ ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (β™―β€˜π‘¦) = π‘š})βˆƒπ‘ ∈ dom π‘Ÿβˆƒπ‘₯ ∈ 𝒫 𝑠((π‘Ÿβ€˜π‘) ≀ (β™―β€˜π‘₯) ∧ βˆ€π‘¦ ∈ 𝒫 π‘₯((β™―β€˜π‘¦) = π‘š β†’ (π‘“β€˜π‘¦) = 𝑐)))}, ℝ*, < ) = inf(𝑇, ℝ*, < ))
70 simp1 1133 . 2 ((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) β†’ 𝑀 ∈ β„•0)
71 simp3 1135 . . 3 ((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) β†’ 𝐹:π‘…βŸΆβ„•0)
72 simp2 1134 . . 3 ((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) β†’ 𝑅 ∈ 𝑉)
7371, 72fexd 7223 . 2 ((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) β†’ 𝐹 ∈ V)
74 xrltso 13123 . . . 4 < Or ℝ*
7574infex 9487 . . 3 inf(𝑇, ℝ*, < ) ∈ V
7675a1i 11 . 2 ((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) β†’ inf(𝑇, ℝ*, < ) ∈ V)
772, 69, 70, 73, 76ovmpod 7555 1 ((𝑀 ∈ β„•0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:π‘…βŸΆβ„•0) β†’ (𝑀 Ramsey 𝐹) = inf(𝑇, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084  βˆ€wal 1531   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  βˆƒwrex 3064  {crab 3426  Vcvv 3468   βŠ† wss 3943  π’« cpw 4597  {csn 4623   class class class wbr 5141  β—‘ccnv 5668  dom cdm 5669   β€œ cima 5672   Fn wfn 6531  βŸΆwf 6532  β€˜cfv 6536  (class class class)co 7404   ∈ cmpo 7406   ↑m cmap 8819  infcinf 9435  β„*cxr 11248   < clt 11249   ≀ cle 11250  β„•0cn0 12473  β™―chash 14293   Ramsey cram 16939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-cnex 11165  ax-resscn 11166  ax-pre-lttri 11183  ax-pre-lttrn 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-po 5581  df-so 5582  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7971  df-2nd 7972  df-er 8702  df-map 8821  df-en 8939  df-dom 8940  df-sdom 8941  df-sup 9436  df-inf 9437  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-ram 16941
This theorem is referenced by:  ramcl2lem  16949
  Copyright terms: Public domain W3C validator